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 Th70, 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 Th70, 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