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