set J = Stop SCM+FSA;
let a be Int-Location ; :: thesis: for I being Program of 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 ; :: 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:25
.= ((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:25
.= (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:29
.= (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:17;
dom (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) = {0,1} by COMPOS_1:61;
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:25
.= ((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:25
.= (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:29
.= (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:17;
dom (Macro (a >0_goto ((card (Stop SCM+FSA)) + 3))) = {0,1} by COMPOS_1:61;
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