let I, J be Program of SCM+FSA ; for a, c being Int-Location st not I destroysdestroy c & not J destroysdestroy c holds
( not if=0 a,I,J destroysdestroy c & not if>0 a,I,J destroysdestroy c )
let a, c be Int-Location ; ( not I destroysdestroy c & not J destroysdestroy c implies ( not if=0 a,I,J destroysdestroy c & not if>0 a,I,J destroysdestroy c ) )
assume A1:
not I destroysdestroy c
; ( J destroysdestroy c or ( not if=0 a,I,J destroysdestroy c & not if>0 a,I,J destroysdestroy c ) )
A2:
not Goto ((card I) + 1) destroysdestroy c
by Th86;
assume A3:
not J destroysdestroy c
; ( not if=0 a,I,J destroysdestroy c & not if>0 a,I,J destroysdestroy c )
then
not (a =0_goto ((card J) + 3)) ';' J destroysdestroy c
by Th82, SCMFSA7B:18;
then
not ((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1)) destroysdestroy c
by A2, Th81;
then A4:
not (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I destroysdestroy c
by A1, Th81;
A5:
not Goto ((card I) + 1) destroysdestroy c
by Th86;
not (a >0_goto ((card J) + 3)) ';' J destroysdestroy c
by A3, Th82, SCMFSA7B:19;
then
not ((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1)) destroysdestroy c
by A5, Th81;
then A6:
not (((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I destroysdestroy 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 destroysdestroy c
by Th85;
hence
not if=0 a,I,J destroysdestroy c
by A4, A7, Th81; not if>0 a,I,J destroysdestroy 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 destroysdestroy c
by Th85;
hence
not if>0 a,I,J destroysdestroy c
by A6, A8, Th81; verum