set J = Stop SCM+FSA ;
let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds
( 0 in dom (while=0 a,I) & 1 in dom (while=0 a,I) & 0 in dom (while>0 a,I) & 1 in dom (while>0 a,I) )
let I be Program of SCM+FSA ; :: thesis: ( 0 in dom (while=0 a,I) & 1 in dom (while=0 a,I) & 0 in dom (while>0 a,I) & 1 in dom (while>0 a,I) )
set I1 = I ';' (Goto 0 );
set f = ((card I) + 4) .--> (goto 0 );
set i = a =0_goto ((card (Stop SCM+FSA )) + 3);
if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA ) = ((((a =0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))) ';' (I ';' (Goto 0 ))) ';' (Stop SCM+FSA ) by SCMFSA8B:def 1
.= (((a =0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )) by SCMFSA6A:67
.= ((a =0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA ))) by SCMFSA6A:67
.= (a =0_goto ((card (Stop SCM+FSA )) + 3)) ';' ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))) by SCMFSA6A:71
.= (Macro (a =0_goto ((card (Stop SCM+FSA )) + 3))) ';' ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))) ;
then A1: dom (Macro (a =0_goto ((card (Stop SCM+FSA )) + 3))) c= dom (if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) by SCMFSA6A:56;
dom (Macro (a =0_goto ((card (Stop SCM+FSA )) + 3))) = {0 ,1} by SCMFSA7B:4;
then A2: ( 0 in dom (Macro (a =0_goto ((card (Stop SCM+FSA )) + 3))) & 1 in dom (Macro (a =0_goto ((card (Stop SCM+FSA )) + 3))) ) by TARSKI:def 2;
dom (while=0 a,I) = (dom (if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA ))) \/ (dom (((card I) + 4) .--> (goto 0 ))) by FUNCT_4:def 1;
then dom (if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) c= dom (while=0 a,I) by XBOOLE_1:7;
then dom (Macro (a =0_goto ((card (Stop SCM+FSA )) + 3))) c= dom (while=0 a,I) by A1, XBOOLE_1:1;
hence ( 0 in dom (while=0 a,I) & 1 in dom (while=0 a,I) ) by A2; :: thesis: ( 0 in dom (while>0 a,I) & 1 in dom (while>0 a,I) )
set i = a >0_goto ((card (Stop SCM+FSA )) + 3);
if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA ) = ((((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))) ';' (I ';' (Goto 0 ))) ';' (Stop SCM+FSA ) by SCMFSA8B:def 2
.= (((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )) by SCMFSA6A:67
.= ((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA ))) by SCMFSA6A:67
.= (a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))) by SCMFSA6A:71
.= (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3))) ';' ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))) ;
then A3: dom (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3))) c= dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) by SCMFSA6A:56;
dom (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3))) = {0 ,1} by SCMFSA7B:4;
then A4: ( 0 in dom (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3))) & 1 in dom (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3))) ) by TARSKI:def 2;
dom (while>0 a,I) = (dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA ))) \/ (dom (((card I) + 4) .--> (goto 0 ))) by FUNCT_4:def 1;
then dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) c= dom (while>0 a,I) by XBOOLE_1:7;
then dom (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3))) c= dom (while>0 a,I) by A3, XBOOLE_1:1;
hence ( 0 in dom (while>0 a,I) & 1 in dom (while>0 a,I) ) by A4; :: thesis: verum