let I, J be Program of SCM+FSA ; :: thesis: for a being Int-Location holds (if>0 a,I,J) . (insloc ((card J) + 2)) = goto (insloc (((card I) + (card J)) + 3))
let a be Int-Location ; :: thesis: (if>0 a,I,J) . (insloc ((card J) + 2)) = goto (insloc (((card I) + (card J)) + 3))
set JJ = (a >0_goto (insloc ((card J) + 3))) ';' J;
set J3 = ((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)));
A1: 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;
A2: card ((a >0_goto (insloc ((card J) + 3))) ';' J) = (card (Macro (a >0_goto (insloc ((card J) + 3))))) + (card J) by SCMFSA6A:61
.= 2 + (card J) by SCMFSA7B:6 ;
card (Goto (insloc ((card I) + 1))) = 1 by SCMFSA8A:29;
then A3: card (((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) = ((card J) + 2) + 1 by A2, SCMFSA6A:61
.= (card J) + (2 + 1) ;
((card J) + 2) -' (card ((a >0_goto (insloc ((card J) + 3))) ';' J)) = 0 by A2, XREAL_1:234;
then A4: goto (insloc ((card I) + 1)) = (Goto (insloc ((card I) + 1))) . (insloc (((card J) + 2) -' (card ((a >0_goto (insloc ((card J) + 3))) ';' J)))) by SCMFSA8A:47;
card (Goto (insloc ((card I) + 1))) = 1 by SCMFSA8A:29;
then (card J) + 2 < (card ((a >0_goto (insloc ((card J) + 3))) ';' J)) + (card (Goto (insloc ((card I) + 1)))) by A2, NAT_1:13;
then A5: (((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) . (insloc ((card J) + 2)) = IncAddr (goto (insloc ((card I) + 1))),(card ((a >0_goto (insloc ((card J) + 3))) ';' J)) by A2, A4, Th13
.= goto (insloc (((card I) + 1) + ((card J) + 2))) by A2, SCMFSA_4:14
.= goto (insloc (((card I) + (card J)) + (1 + 2))) ;
A6: ( 6 <> 0 & InsCode (goto (insloc (((card I) + (card J)) + 3))) = 6 & InsCode (halt SCM+FSA ) = 0 ) by SCMFSA_2:47, SCMFSA_2:124;
card (((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) = ((card J) + 2) + 1 by A3;
then (card J) + 2 < card (((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) by NAT_1:13;
then A7: insloc ((card J) + 2) in dom (((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) by SCMFSA6A:15;
then ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' (I ';' (Stop SCM+FSA ))) . (insloc ((card J) + 2)) = (Directed (((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1))))) . (insloc ((card J) + 2)) by SCMFSA8A:28
.= goto (insloc (((card I) + (card J)) + 3)) by A5, A6, A7, SCMFSA8A:30 ;
hence (if>0 a,I,J) . (insloc ((card J) + 2)) = goto (insloc (((card I) + (card J)) + 3)) by A1, SCMFSA6A:67; :: thesis: verum