set J = Stop SCM+FSA ;
let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds
( (while=0 a,I) . 0 = a =0_goto 4 & (while=0 a,I) . 1 = goto 2 & (while>0 a,I) . 0 = a >0_goto 4 & (while>0 a,I) . 1 = goto 2 )
let I be Program of SCM+FSA ; :: thesis: ( (while=0 a,I) . 0 = a =0_goto 4 & (while=0 a,I) . 1 = goto 2 & (while>0 a,I) . 0 = a >0_goto 4 & (while>0 a,I) . 1 = goto 2 )
set I1 = I ';' (Goto 0 );
set f = ((card I) + 4) .--> (goto 0 );
set i = a =0_goto ((card (Stop SCM+FSA )) + 3);
A1: a =0_goto ((card (Stop SCM+FSA )) + 3) <> halt SCM+FSA by SCMFSA_2:48, SCMFSA_2:124;
A2: 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;
A3: dom (((card I) + 4) .--> (goto 0 )) = {((card I) + 4)} by FUNCOP_1:19;
then A4: not 0 in dom (((card I) + 4) .--> (goto 0 )) ;
A5: dom (Macro (a =0_goto ((card (Stop SCM+FSA )) + 3))) = {0 ,1} by SCMFSA7B:4;
then A6: 0 in dom (Macro (a =0_goto ((card (Stop SCM+FSA )) + 3))) by TARSKI:def 2;
A7: 1 in dom (Macro (a =0_goto ((card (Stop SCM+FSA )) + 3))) by A5, TARSKI:def 2;
A8: 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 )))) ;
1 <> (card I) + 4 by NAT_1:11;
then A9: not 1 in dom (((card I) + 4) .--> (goto 0 )) by A3, TARSKI:def 1;
0 in dom (while=0 a,I) by Th10;
hence (while=0 a,I) . 0 = (if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) . 0 by A4, A2, FUNCT_4:def 1
.= (Directed (Macro (a =0_goto ((card (Stop SCM+FSA )) + 3)))) . 0 by A8, A6, SCMFSA8A:28
.= a =0_goto 4 by A1, SCMFSA7B:7, LL ;
:: thesis: ( (while=0 a,I) . 1 = goto 2 & (while>0 a,I) . 0 = a >0_goto 4 & (while>0 a,I) . 1 = goto 2 )
A10: 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;
1 in dom (while=0 a,I) by Th10;
hence (while=0 a,I) . 1 = (if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) . 1 by A2, A9, FUNCT_4:def 1
.= (Directed (Macro (a =0_goto ((card (Stop SCM+FSA )) + 3)))) . 1 by A8, A7, SCMFSA8A:28
.= goto 2 by SCMFSA7B:8 ;
:: thesis: ( (while>0 a,I) . 0 = a >0_goto 4 & (while>0 a,I) . 1 = goto 2 )
set i = a >0_goto ((card (Stop SCM+FSA )) + 3);
A11: a >0_goto ((card (Stop SCM+FSA )) + 3) <> halt SCM+FSA by SCMFSA_2:49, SCMFSA_2:124;
A12: 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 )))) ;
A13: dom (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3))) = {0 ,1} by SCMFSA7B:4;
then A14: 0 in dom (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3))) by TARSKI:def 2;
A15: 1 in dom (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3))) by A13, TARSKI:def 2;
0 in dom (while>0 a,I) by Th10;
hence (while>0 a,I) . 0 = (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) . 0 by A4, A10, FUNCT_4:def 1
.= (Directed (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3)))) . 0 by A12, A14, SCMFSA8A:28
.= a >0_goto 4 by A11, SCMFSA7B:7, LL ;
:: thesis: (while>0 a,I) . 1 = goto 2
1 in dom (while>0 a,I) by Th10;
hence (while>0 a,I) . 1 = (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) . 1 by A9, A10, FUNCT_4:def 1
.= (Directed (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3)))) . 1 by A12, A15, SCMFSA8A:28
.= goto 2 by SCMFSA7B:8 ;
:: thesis: verum