let I, J be Program of ; for a being Int-Location holds (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)) = goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 5))
let a be Int-Location ; (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)) = goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 5))
set I1 = I ';' (SubFrom a,(intloc 0 ));
set J3 = ((a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) ';' (I ';' (SubFrom a,(intloc 0 )))) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)));
set J4 = (((a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) ';' (I ';' (SubFrom a,(intloc 0 )))) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2));
A1:
card (Goto (insloc ((card (Goto (insloc 2))) + 1))) = 1
by SCMFSA8A:29;
card ((a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) ';' (I ';' (SubFrom a,(intloc 0 )))) =
(card (Macro (a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))))) + (card (I ';' (SubFrom a,(intloc 0 ))))
by SCMFSA6A:61
.=
2 + (card (I ';' (SubFrom a,(intloc 0 ))))
by SCMFSA7B:6
;
then A2: card (((a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) ';' (I ';' (SubFrom a,(intloc 0 )))) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) =
((card (I ';' (SubFrom a,(intloc 0 )))) + 2) + 1
by A1, SCMFSA6A:61
.=
(card (I ';' (SubFrom a,(intloc 0 )))) + (2 + 1)
;
then
((card (I ';' (SubFrom a,(intloc 0 )))) + (2 + 1)) -' (card (((a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) ';' (I ';' (SubFrom a,(intloc 0 )))) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1))))) = 0
by XREAL_1:234;
then A3:
goto (insloc 2) = (Goto (insloc 2)) . (insloc (((card (I ';' (SubFrom a,(intloc 0 )))) + (2 + 1)) -' (card (((a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) ';' (I ';' (SubFrom a,(intloc 0 )))) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))))))
by SCMFSA8A:47;
A4:
card (Goto (insloc 2)) = 1
by SCMFSA8A:29;
then
(card (I ';' (SubFrom a,(intloc 0 )))) + (2 + 1) < (card (((a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) ';' (I ';' (SubFrom a,(intloc 0 )))) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1))))) + (card (Goto (insloc 2)))
by A2, NAT_1:13;
then A5: ((((a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) ';' (I ';' (SubFrom a,(intloc 0 )))) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2))) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + (2 + 1))) =
IncAddr (goto (insloc 2)),(card (((a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) ';' (I ';' (SubFrom a,(intloc 0 )))) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))))
by A2, A3, Th13
.=
goto ((insloc 2) + ((card (I ';' (SubFrom a,(intloc 0 )))) + (2 + 1)))
by A2, SCMFSA_4:14
.=
goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + (2 + 3)))
;
A6:
InsCode (goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 5))) = 6
by SCMFSA_2:47;
card ((((a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) ';' (I ';' (SubFrom a,(intloc 0 )))) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2))) =
((card (I ';' (SubFrom a,(intloc 0 )))) + (2 + 1)) + 1
by A2, A4, SCMFSA6A:61
.=
(card (I ';' (SubFrom a,(intloc 0 )))) + ((2 + 1) + 1)
;
then
card ((((a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) ';' (I ';' (SubFrom a,(intloc 0 )))) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2))) = ((card (I ';' (SubFrom a,(intloc 0 )))) + 3) + 1
;
then
(card (I ';' (SubFrom a,(intloc 0 )))) + 3 < card ((((a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) ';' (I ';' (SubFrom a,(intloc 0 )))) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2)))
by NAT_1:13;
then A7:
insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3) in dom ((((a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) ';' (I ';' (SubFrom a,(intloc 0 )))) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2)))
by SCMFSA6A:15;
then (((((a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) ';' (I ';' (SubFrom a,(intloc 0 )))) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2))) ';' (Stop SCM+FSA )) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)) =
(Directed ((((a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) ';' (I ';' (SubFrom a,(intloc 0 )))) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2)))) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))
by SCMFSA8A:28
.=
goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 5))
by A5, A6, A7, SCMFSA8A:30, SCMFSA_2:124
;
hence
(if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)) = goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 5))
by SCMFSA8B:def 1; verum