let I, J be Program 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 Th86;
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 Th82, SCMFSA7B:12;
then
not ((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1)) destroys c
by A2, Th81;
then A4:
not (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I destroys c
by A1, Th81;
A5:
not Goto ((card I) + 1) destroys c
by Th86;
not (a >0_goto ((card J) + 3)) ';' J destroys c
by A3, Th82, SCMFSA7B:13;
then
not ((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1)) destroys c
by A5, Th81;
then A6:
not (((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I destroys c
by A1, Th81;
A7:
if=0 (a,I,J) = ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)
by SCMFSA8B:def 1;
not Stop SCM+FSA destroys c
by Th85;
hence
not if=0 (a,I,J) destroys c
by A4, A7, Th81; not if>0 (a,I,J) destroys c
A8:
if>0 (a,I,J) = ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)
by SCMFSA8B:def 2;
not Stop SCM+FSA destroys c
by Th85;
hence
not if>0 (a,I,J) destroys c
by A6, A8, Th81; verum