Prove:

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

under the assumptions:

(Definition (addition): 1) ,

(Definition (addition): 2) .

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

The proof of ()fails. (The prover "Simplifier" was unable to transform the proof situation.)

Alternative proof 2: failed

We try to prove () by induction on .

Induction Base:

(1) .

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

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:

⌋

Alternative proof 2: pending

Pending proof of ().

Induction Step:

Induction Hypothesis:

(2)

Induction Conclusion:

(3) .

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

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 try to prove () by induction on .

Induction Base:

(11) .

We simplify ().

Simplification of the lhs term:

= by ()

⌋

Simplification of the rhs term:

⌋

Hence, it is sufficient to prove:

(14) .

The proof of () fails. (No applicable inference rule was found.)

Induction Step:

Induction Hypothesis:

(12)

Induction Conclusion:

(13) .

We simplify ().

Simplification of the lhs term:

= by ()

= by ()

⌋

Simplification of the rhs term:

⌋

Hence, it is sufficient to prove:

(15) .

The proof of () fails. (No applicable inference rule was found.)

Alternative proof 2: failed

We try to prove () by induction on .

Induction Base:

(16) .

We simplify ().

Simplification of the lhs term:

= by ()

⌋

Simplification of the rhs term:

= by ()

⌋

Hence, it is sufficient to prove:

(19) .

The proof of () fails. (No applicable inference rule was found.)

Induction Step:

Induction Hypothesis:

(17)

Induction Conclusion:

(18) .

Pending proof of ().

•

Additional Proof Generation Information

---

Converted by Mathematica      June 17, 2002