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