let I be MacroInstruction of SCM+FSA ; :: thesis: for a being Int-Location holds if=0 (a,(I ';' (goto 0))) = ((((a =0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) ';' (goto 0)) ";" (Stop SCM+FSA)
let a be Int-Location; :: thesis: if=0 (a,(I ';' (goto 0))) = ((((a =0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) ';' (goto 0)) ";" (Stop SCM+FSA)
set I1 = I ';' (goto 0);
thus if=0 (a,(I ';' (goto 0))) = (((a =0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" (I ';' (goto 0))) ";" (Stop SCM+FSA)
.= ((stop (Directed ((a =0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))))) ';' (I ';' (goto 0))) ";" (Stop SCM+FSA)
.= (((stop (Directed ((a =0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))))) ';' I) ';' (goto 0)) ";" (Stop SCM+FSA) by COMPOS_1:29
.= ((((a =0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) ';' (goto 0)) ";" (Stop SCM+FSA) ; :: thesis: verum