let I, J be MacroInstruction of SCM+FSA ; for a, c being Int-Location st not I destroys c & not J destroys c holds
( not if=0 (a,I,J) destroys c & not if>0 (a,I,J) destroys c )
let a, c be Int-Location; ( not I destroys c & not J destroys c implies ( not if=0 (a,I,J) destroys c & not if>0 (a,I,J) destroys c ) )
assume A1:
not I destroys c
; ( J destroys c or ( not if=0 (a,I,J) destroys c & not if>0 (a,I,J) destroys c ) )
A2:
not Goto ((card I) + 1) destroys c
by Th48;
assume A3:
not J destroys c
; ( not if=0 (a,I,J) destroys c & not if>0 (a,I,J) destroys c )
then
not (a =0_goto ((card J) + 3)) ";" J destroys c
by Th44, SCMFSA7B:12;
then
not ((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1)) destroys c
by A2, Th43;
then A4:
not (((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I destroys c
by A1, Th43;
A5:
not Goto ((card I) + 1) destroys c
by Th48;
not (a >0_goto ((card J) + 3)) ";" J destroys c
by A3, Th44, SCMFSA7B:13;
then
not ((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1)) destroys c
by A5, Th43;
then A6:
not (((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I destroys c
by A1, Th43;
not Stop SCM+FSA destroys c
by Th47;
hence
not if=0 (a,I,J) destroys c
by A4, Th43; not if>0 (a,I,J) destroys c
not Stop SCM+FSA destroys c
by Th47;
hence
not if>0 (a,I,J) destroys c
by A6, Th43; verum