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:14;
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:18;
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