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