Prove:
(Proposition (commutativity of addition): + = ) ,
under the assumptions:
(Proposition (20): 20) ,
(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 and prove:
(4) .
A proof by simplification of () works.
Simplification of the lhs term:
= by ()
⌋
Simplification of the rhs term:
= by ()
⌋
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:
(5)
and simplify it.
Simplification of the lhs term:
⌋
Simplification of the rhs term:
= by ()
⌋
Hence, it is sufficient to prove:
(6) .
We try to prove () by induction on .
Induction Base:
(7) .
A proof by simplification of () works.
Simplification of the lhs term:
= by ()
⌋
Simplification of the rhs term:
= by ()
⌋
Induction Step:
Induction Hypothesis:
(8)
Induction Conclusion:
(9) .
We simplify ().
Simplification of the lhs term:
= by ()
= by ()
⌋
Simplification of the rhs term:
⌋
Hence, it is sufficient to prove:
(10) .
The proof of () fails. (No applicable inference rule was found.)
Alternative proof 2: failed
We try to 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) .
We simplify ().
Simplification of the lhs term:
= by ()
= by ()
= by ()
⌋
Simplification of the rhs term:
= by ()
⌋
Hence, it is sufficient to prove:
(14) .
The proof of () fails. (No applicable inference rule was found.)
•