let a be Int-Location ; :: thesis: for I, J being Program of SCM+FSA holds
( (if=0 a,I,J) . (insloc 0 ) = a =0_goto (insloc ((card J) + 3)) & (if=0 a,I,J) . (insloc 1) = goto (insloc 2) & (if>0 a,I,J) . (insloc 0 ) = a >0_goto (insloc ((card J) + 3)) & (if>0 a,I,J) . (insloc 1) = goto (insloc 2) )
let I, J be Program of SCM+FSA ; :: thesis: ( (if=0 a,I,J) . (insloc 0 ) = a =0_goto (insloc ((card J) + 3)) & (if=0 a,I,J) . (insloc 1) = goto (insloc 2) & (if>0 a,I,J) . (insloc 0 ) = a >0_goto (insloc ((card J) + 3)) & (if>0 a,I,J) . (insloc 1) = goto (insloc 2) )
set i = a =0_goto (insloc ((card J) + 3));
A1: a =0_goto (insloc ((card J) + 3)) <> halt SCM+FSA by SCMFSA_2:48, SCMFSA_2:124;
A2: if=0 a,I,J = ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) by SCMFSA8B:def 1
.= (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' (I ';' (Stop SCM+FSA )) by SCMFSA6A:67
.= ((a =0_goto (insloc ((card J) + 3))) ';' J) ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA ))) by SCMFSA6A:67
.= (a =0_goto (insloc ((card J) + 3))) ';' (J ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )))) by SCMFSA6A:71
.= (Macro (a =0_goto (insloc ((card J) + 3)))) ';' (J ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )))) ;
dom (Macro (a =0_goto (insloc ((card J) + 3)))) = {(insloc 0 ),(insloc 1)} by SCMFSA7B:4;
then A3: ( insloc 0 in dom (Macro (a =0_goto (insloc ((card J) + 3)))) & insloc 1 in dom (Macro (a =0_goto (insloc ((card J) + 3)))) ) by TARSKI:def 2;
hence (if=0 a,I,J) . (insloc 0 ) = (Directed (Macro (a =0_goto (insloc ((card J) + 3))))) . (insloc 0 ) by A2, SCMFSA8A:28
.= a =0_goto (insloc ((card J) + 3)) by A1, SCMFSA7B:7 ;
:: thesis: ( (if=0 a,I,J) . (insloc 1) = goto (insloc 2) & (if>0 a,I,J) . (insloc 0 ) = a >0_goto (insloc ((card J) + 3)) & (if>0 a,I,J) . (insloc 1) = goto (insloc 2) )
thus (if=0 a,I,J) . (insloc 1) = (Directed (Macro (a =0_goto (insloc ((card J) + 3))))) . (insloc 1) by A2, A3, SCMFSA8A:28
.= goto (insloc 2) by SCMFSA7B:8 ; :: thesis: ( (if>0 a,I,J) . (insloc 0 ) = a >0_goto (insloc ((card J) + 3)) & (if>0 a,I,J) . (insloc 1) = goto (insloc 2) )
set i = a >0_goto (insloc ((card J) + 3));
A4: a >0_goto (insloc ((card J) + 3)) <> halt SCM+FSA by SCMFSA_2:49, SCMFSA_2:124;
A5: if>0 a,I,J = ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) by SCMFSA8B:def 2
.= (((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' (I ';' (Stop SCM+FSA )) by SCMFSA6A:67
.= ((a >0_goto (insloc ((card J) + 3))) ';' J) ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA ))) by SCMFSA6A:67
.= (a >0_goto (insloc ((card J) + 3))) ';' (J ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )))) by SCMFSA6A:71
.= (Macro (a >0_goto (insloc ((card J) + 3)))) ';' (J ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )))) ;
dom (Macro (a >0_goto (insloc ((card J) + 3)))) = {(insloc 0 ),(insloc 1)} by SCMFSA7B:4;
then A6: ( insloc 0 in dom (Macro (a >0_goto (insloc ((card J) + 3)))) & insloc 1 in dom (Macro (a >0_goto (insloc ((card J) + 3)))) ) by TARSKI:def 2;
hence (if>0 a,I,J) . (insloc 0 ) = (Directed (Macro (a >0_goto (insloc ((card J) + 3))))) . (insloc 0 ) by A5, SCMFSA8A:28
.= a >0_goto (insloc ((card J) + 3)) by A4, SCMFSA7B:7 ;
:: thesis: (if>0 a,I,J) . (insloc 1) = goto (insloc 2)
thus (if>0 a,I,J) . (insloc 1) = (Directed (Macro (a >0_goto (insloc ((card J) + 3))))) . (insloc 1) by A5, A6, SCMFSA8A:28
.= goto (insloc 2) by SCMFSA7B:8 ; :: thesis: verum