RISC JKU

Prove:

(Proposition (commutativity of addition):  + = ) [Graphics:Images/index_gr_1.gif] ,

under the assumptions:

(Proposition (20): 20) [Graphics:Images/index_gr_2.gif] ,

(Definition (addition): 1) [Graphics:Images/index_gr_3.gif] ,

(Definition (addition): 2) [Graphics:Images/index_gr_4.gif] .

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 ([Graphics:Images/index_gr_5.gif])fails. (The prover "Simplifier" was unable to transform the proof situation.)

Alternative proof 2: failed

We try to prove ([Graphics:Images/index_gr_6.gif]) by induction on [Graphics:Images/index_gr_7.gif].

Induction Base:

(1) [Graphics:Images/index_gr_8.gif] .

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 ([Graphics:Images/index_gr_9.gif]) all variables arbitrary but fixed and prove:

(4) [Graphics:Images/index_gr_10.gif] .

A proof by simplification of ([Graphics:Images/index_gr_11.gif]) works.

Simplification of the lhs term:

[Graphics:Images/index_gr_12.gif] = by ([Graphics:Images/index_gr_13.gif])

[Graphics:Images/index_gr_14.gif]

Simplification of the rhs term:

[Graphics:Images/index_gr_15.gif] = by ([Graphics:Images/index_gr_16.gif])

[Graphics:Images/index_gr_17.gif]

Alternative proof 2: pending

Pending proof of ([Graphics:Images/index_gr_18.gif]).

Induction Step:

Induction Hypothesis:

(2) [Graphics:Images/index_gr_19.gif]

Induction Conclusion:

(3) [Graphics:Images/index_gr_20.gif] .

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 ([Graphics:Images/index_gr_21.gif]) all variables arbitrary but fixed:

(5) [Graphics:Images/index_gr_22.gif]

and simplify it.

Simplification of the lhs term:

[Graphics:Images/index_gr_23.gif]

Simplification of the rhs term:

[Graphics:Images/index_gr_24.gif] = by ([Graphics:Images/index_gr_25.gif])

[Graphics:Images/index_gr_26.gif]

Hence, it is sufficient to prove:

(6) [Graphics:Images/index_gr_27.gif] .

We try to prove ([Graphics:Images/index_gr_28.gif]) by induction on [Graphics:Images/index_gr_29.gif].

Induction Base:

(7) [Graphics:Images/index_gr_30.gif] .

A proof by simplification of ([Graphics:Images/index_gr_31.gif]) works.

Simplification of the lhs term:

[Graphics:Images/index_gr_32.gif] = by ([Graphics:Images/index_gr_33.gif])

[Graphics:Images/index_gr_34.gif]

Simplification of the rhs term:

[Graphics:Images/index_gr_35.gif] = by ([Graphics:Images/index_gr_36.gif])

[Graphics:Images/index_gr_37.gif]

Induction Step:

Induction Hypothesis:

(8) [Graphics:Images/index_gr_38.gif]

Induction Conclusion:

(9) [Graphics:Images/index_gr_39.gif] .

We simplify ([Graphics:Images/index_gr_40.gif]).

Simplification of the lhs term:

[Graphics:Images/index_gr_41.gif] = by ([Graphics:Images/index_gr_42.gif])

[Graphics:Images/index_gr_43.gif] = by ([Graphics:Images/index_gr_44.gif])

[Graphics:Images/index_gr_45.gif]

Simplification of the rhs term:

[Graphics:Images/index_gr_46.gif]

Hence, it is sufficient to prove:

(10) [Graphics:Images/index_gr_47.gif] .

The proof of ([Graphics:Images/index_gr_48.gif]) fails. (No applicable inference rule was found.)

Alternative proof 2: failed

We try to prove ([Graphics:Images/index_gr_49.gif]) by induction on [Graphics:Images/index_gr_50.gif].

Induction Base:

(11) [Graphics:Images/index_gr_51.gif] .

A proof by simplification of ([Graphics:Images/index_gr_52.gif]) works.

Simplification of the lhs term:

[Graphics:Images/index_gr_53.gif] = by ([Graphics:Images/index_gr_54.gif])

[Graphics:Images/index_gr_55.gif]

Simplification of the rhs term:

[Graphics:Images/index_gr_56.gif] = by ([Graphics:Images/index_gr_57.gif])

[Graphics:Images/index_gr_58.gif]

Induction Step:

Induction Hypothesis:

(12) [Graphics:Images/index_gr_59.gif]

Induction Conclusion:

(13) [Graphics:Images/index_gr_60.gif] .

We simplify ([Graphics:Images/index_gr_61.gif]).

Simplification of the lhs term:

[Graphics:Images/index_gr_62.gif] = by ([Graphics:Images/index_gr_63.gif])

[Graphics:Images/index_gr_64.gif] = by ([Graphics:Images/index_gr_65.gif])

[Graphics:Images/index_gr_66.gif] = by ([Graphics:Images/index_gr_67.gif])

[Graphics:Images/index_gr_68.gif]

Simplification of the rhs term:

[Graphics:Images/index_gr_69.gif] = by ([Graphics:Images/index_gr_70.gif])

[Graphics:Images/index_gr_71.gif]

Hence, it is sufficient to prove:

(14) [Graphics:Images/index_gr_72.gif] .

The proof of ([Graphics:Images/index_gr_73.gif]) fails. (No applicable inference rule was found.)

Additional Proof Generation Information


Converted by Mathematica      June 17, 2002