set J = Stop SCM+FSA;
let a be Int-Location; for I being MacroInstruction of SCM+FSA holds (while>0 (a,I)) . 2 = goto ((card I) + 4)
let I be MacroInstruction of SCM+FSA ; (while>0 (a,I)) . 2 = goto ((card I) + 4)
set I1 = I ';' (goto 0);
set i = a >0_goto 3;
set Mi = Macro (a >0_goto 3);
set G = Goto ((card (I ';' (goto 0))) + 1);
set J2 = (I ';' (goto 0)) ";" (Stop SCM+FSA);
set J1 = (Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA));
A1:
0 in dom (Goto ((card (I ';' (goto 0))) + 1))
by SCMFSA8A:31;
A2:
(Goto ((card (I ';' (goto 0))) + 1)) . 0 = goto ((card (I ';' (goto 0))) + 1)
;
dom ((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA))) = (dom (Goto ((card (I ';' (goto 0))) + 1))) \/ (dom (Reloc (((I ';' (goto 0)) ";" (Stop SCM+FSA)),(card (Goto ((card (I ';' (goto 0))) + 1))))))
by SCMFSA6A:39;
then A3:
0 in dom ((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA)))
by A1, XBOOLE_0:def 3;
then
0 + 2 in { (il + 2) where il is Nat : il in dom ((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA))) }
;
then A4:
2 in dom (Shift (((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA))),2))
by VALUED_1:def 12;
then A5: (Shift (((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA))),2)) /. 2 =
(Shift (((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA))),2)) . (0 + 2)
by PARTFUN1:def 6
.=
((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA))) . 0
by A3, VALUED_1:def 12
.=
(Directed (Goto ((card (I ';' (goto 0))) + 1))) . 0
by A1, SCMFSA8A:14
.=
goto ((card (I ';' (goto 0))) + 1)
by A1, A2, SCMFSA8A:16
;
A6:
card (Macro (a >0_goto 3)) = 2
by COMPOS_1:56;
then A7:
not 2 in dom (Macro (a >0_goto 3))
;
A8:
( 2 in dom (while>0 (a,I)) & dom (while>0 (a,I)) = dom (if>0 (a,(I ';' (goto 0)))) )
by Th7, FUNCT_7:30;
A9: if>0 (a,(I ';' (goto 0))) =
((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA))
by SCMFSA6A:25
.=
(Macro (a >0_goto 3)) ";" ((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA)))
by SCMFSA6A:25
;
then
dom (if>0 (a,(I ';' (goto 0)))) = (dom (Macro (a >0_goto 3))) \/ (dom (Reloc (((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA))),2)))
by SCMFSA6A:39, A6;
then A10:
2 in dom (Reloc (((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA))),2))
by A8, A7, XBOOLE_0:def 3;
A11:
Reloc (((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA))),2) = IncAddr ((Shift (((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA))),2)),2)
by COMPOS_1:34;
0 + 2 <> (card I) + 2
;
hence (while>0 (a,I)) . 2 =
((Macro (a >0_goto 3)) ";" ((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA)))) . 2
by A9, FUNCT_7:32
.=
(Reloc (((Goto ((card (I ';' (goto 0))) + 1)) ";" ((I ';' (goto 0)) ";" (Stop SCM+FSA))),2)) . 2
by A10, SCMFSA6A:40, A6
.=
IncAddr ((goto ((card (I ';' (goto 0))) + 1)),2)
by A4, A5, A11, COMPOS_1:def 21
.=
goto (((card (I ';' (goto 0))) + 1) + 2)
by SCMFSA_4:1
.=
goto ((((card I) + 1) + 1) + 2)
by COMPOS_2:11
.=
goto ((card I) + 4)
;
verum