set J = Stop SCM+FSA;
let a be Int-Location ; :: thesis: for I being Program of 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 ; :: 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: 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;
A2: dom (((card I) + 4) .--> (goto 0)) = {((card I) + 4)} by FUNCOP_1:13;
then A3: not 0 in dom (((card I) + 4) .--> (goto 0)) ;
A4: dom (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) = {0,1} by COMPOS_1:61;
then A5: 0 in dom (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) by TARSKI:def 2;
A6: 1 in dom (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) by A4, TARSKI:def 2;
A7: 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)))) ;
1 <> (card I) + 4 by NAT_1:11;
then A8: not 1 in dom (((card I) + 4) .--> (goto 0)) by A2, 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 A3, A1, FUNCT_4:def 1
.= (Directed (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3)))) . 0 by A7, A5, SCMFSA8A:14
.= a =0_goto 4 by Lm1, SCMFSA7B:1 ;
:: thesis: ( (while=0 (a,I)) . 1 = goto 2 & (while>0 (a,I)) . 0 = a >0_goto 4 & (while>0 (a,I)) . 1 = goto 2 )
A9: 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 A1, A8, FUNCT_4:def 1
.= (Directed (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3)))) . 1 by A7, A6, SCMFSA8A:14
.= goto 2 by SCMFSA7B:2 ;
:: 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);
A10: 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)))) ;
A11: dom (Macro (a >0_goto ((card (Stop SCM+FSA)) + 3))) = {0,1} by COMPOS_1:61;
then A12: 0 in dom (Macro (a >0_goto ((card (Stop SCM+FSA)) + 3))) by TARSKI:def 2;
A13: 1 in dom (Macro (a >0_goto ((card (Stop SCM+FSA)) + 3))) by A11, 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 A3, A9, FUNCT_4:def 1
.= (Directed (Macro (a >0_goto ((card (Stop SCM+FSA)) + 3)))) . 0 by A10, A12, SCMFSA8A:14
.= a >0_goto 4 by Lm1, SCMFSA7B:1 ;
:: 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 A8, A9, FUNCT_4:def 1
.= (Directed (Macro (a >0_goto ((card (Stop SCM+FSA)) + 3)))) . 1 by A10, A13, SCMFSA8A:14
.= goto 2 by SCMFSA7B:2 ;
:: thesis: verum