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 Th57;
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 Th53, SCMFSA7B:12;
then
not ((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1)) destroys c
by A2, Th52;
then A4:
not (((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I destroys c
by A1, Th52;
A5:
not Goto ((card I) + 1) destroys c
by Th57;
not (a >0_goto ((card J) + 3)) ";" J destroys c
by A3, Th53, SCMFSA7B:13;
then
not ((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1)) destroys c
by A5, Th52;
then A6:
not (((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I destroys c
by A1, Th52;
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 Th56;
hence
not if=0 (a,I,J) destroys c
by A4, A7, Th52; 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 Th56;
hence
not if>0 (a,I,J) destroys c
by A6, A8, Th52; verum