RISC JKU

Direction from right to left:

We assume

(DA.RA) [Graphics:indexgr135.gif]

and show

(DA.LC) [Graphics:indexgr136.gif].

We prove (DA.LC) by the deduction rule.

We assume

(DA.LC.H) [Graphics:indexgr137.gif]

and show

(DA.LC.C) [Graphics:indexgr138.gif].

We prove (DA.LC.C) by case distinction using (DA.RA).

Case (DA.RA.1) [Graphics:indexgr141.gif]:

Case (DA.RA.2) [Graphics:indexgr144.gif]: