RISC JKU

Prove:

(Proposition (equal classes)) [Graphics:Images/index_gr_1.gif] ,

under the assumptions:

We assume

(1) [Graphics:Images/index_gr_6.gif] ,

and show

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

We prove ([Graphics:Images/index_gr_8.gif]) by the deduction rule.

We assume

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

and show

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

Formula ([Graphics:Images/index_gr_11.gif]), using ([Graphics:Images/index_gr_12.gif]), is implied by:

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

We show ([Graphics:Images/index_gr_14.gif]) by mutual inclusion:

⊆: We assume

⊇: Now we assume

•

Additional Proof Generation Information

Converted by Mathematica      June 17, 2002