let I, J be Program of ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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 (insloc ((card I) + 1)) does_not_destroy c by Th86;
assume A3: J does_not_destroy c ; :: thesis: ( if=0 a,I,J does_not_destroy c & if>0 a,I,J does_not_destroy c )
then (a =0_goto (insloc ((card J) + 3))) ';' J does_not_destroy c by Th82, SCMFSA7B:18;
then ((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1))) does_not_destroy c by A2, Th81;
then A4: (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I does_not_destroy c by A1, Th81;
A5: Goto (insloc ((card I) + 1)) does_not_destroy c by Th86;
(a >0_goto (insloc ((card J) + 3))) ';' J does_not_destroy c by A3, Th82, SCMFSA7B:19;
then ((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1))) does_not_destroy c by A5, Th81;
then A6: (((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I does_not_destroy c by A1, Th81;
A7: if=0 a,I,J = ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((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; :: thesis: if>0 a,I,J does_not_destroy c
A8: if>0 a,I,J = ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((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; :: thesis: verum