set i = a =0_goto (insloc ((card J) + 3));
reconsider Mi = Macro (a =0_goto (insloc ((card J) + 3))) as good Program of SCM+FSA by Th36, SCMFSA7B:18;
if=0 a,I,J = ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) by SCMFSA8B:def 1
.= (((Mi ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) ;
hence if=0 a,I,J is good ; :: thesis: verum