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