Prove:

(Proposition (20): 20) ,

under the assumptions:

(Definition (addition): 1) ,

(Definition (addition): 2) .

We prove () by induction on .

Induction Base:

(1) .

A proof by simplification of () works.

Simplification of the lhs term:

= by ()

⌋

Simplification of the rhs term:

⌋

Induction Step:

Induction Hypothesis:

(2)

Induction Conclusion:

(3) .

A proof by simplification of () works.

Simplification of the lhs term:

= by ()

= by ()

⌋

Simplification of the rhs term:

⌋

•

Additional Proof Generation Information

---

Converted by Mathematica      June 17, 2002