let I be good Program of SCM+FSA ; :: thesis: for a being read-write Int-Location holds if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is good
let a be read-write Int-Location ; :: thesis: if=0 a,(Goto (insloc 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 (insloc ((card I1) + 3))) as good Program of SCM+FSA by Th99, SCMFSA7B:18;
if=0 a,(Goto (insloc 2)),I1 = ((((a =0_goto (insloc ((card I1) + 3))) ';' I1) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2))) ';' (Stop SCM+FSA ) by SCMFSA8B:def 1
.= (((J1 ';' I1) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2))) ';' (Stop SCM+FSA ) ;
hence if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is good ; :: thesis: verum