Prove:

(Proposition (commutativity of addition):  + = ) ,

under the assumptions:

(Proposition (15): 15) ,

(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 and prove:

(4) .

A proof by simplification of () works.

Simplification of the lhs term:

= by ()

⌋

Simplification of the rhs term:

= by ()

⌋

Induction Step:

Induction Hypothesis:

(2)

Induction Conclusion:

(3) .

We take in () all variables arbitrary but fixed and prove:

(5) .

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