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