Prove:

(Proposition (15): 15) ,

under the assumptions:

(Proposition (20): 20) ,

(Definition (addition): 1) ,

(Definition (addition): 2) .

We prove () by induction on .

Induction Base:

(1) .

We take in () all variables arbitrary but fixed:

(4)

and simplify it.

Simplification of the lhs term:

⌋

Simplification of the rhs term:

= by ()

⌋

Hence, it is sufficient to prove:

(5) .

We prove () by induction on .

Induction Base:

(6) .

A proof by simplification of () works.

Simplification of the lhs term:

= by ()

⌋

Simplification of the rhs term:

⌋

Induction Step:

Induction Hypothesis:

(7)

Induction Conclusion:

(8) .

A proof by simplification of () works.

Simplification of the lhs term:

= by ()

= by ()

⌋

Simplification of the rhs term:

⌋

Induction Step:

Induction Hypothesis:

(2)

Induction Conclusion:

(3) .

We take in () all variables arbitrary but fixed:

(9)

and simplify it.

Simplification of the lhs term:

⌋

Simplification of the rhs term:

= by ()

⌋

Hence, it is sufficient to prove:

(10) .

We prove () by induction on .

Induction Base:

(11) .

A proof by simplification of () works.

Simplification of the lhs term:

= by ()

⌋

Simplification of the rhs term:

= by ()

⌋

Induction Step:

Induction Hypothesis:

(12)

Induction Conclusion:

(13) .

A proof by simplification of () works.

Simplification of the lhs term:

= by ()

= by ()

⌋

Simplification of the rhs term:

= by ()

⌋

•

Additional Proof Generation Information

---

Converted by Mathematica      June 17, 2002