let I be good Program of SCM+FSA; :: thesis: for a being read-write Int-Location holds if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is good
let a be read-write Int-Location ; :: thesis: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is good
reconsider J3 = Macro (SubFrom (a,(intloc 0))) as good Program of SCM+FSA by Th99, SCMFSA7B:8;
I ';' (SubFrom (a,(intloc 0))) = I ';' J3 ;
then reconsider I1 = I ';' (SubFrom (a,(intloc 0))) as good Program of SCM+FSA ;
reconsider J1 = Macro (a =0_goto ((card I1) + 3)) as good Program of SCM+FSA by Th99, SCMFSA7B:12;
if=0 (a,(Goto 2),I1) = ((((a =0_goto ((card I1) + 3)) ';' I1) ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2)) ';' (Stop SCM+FSA) by SCMFSA8B:def 1
.= (((J1 ';' I1) ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2)) ';' (Stop SCM+FSA) ;
hence if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is good ; :: thesis: verum