let I, J be Program of ; :: 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 1;
A2: InsCode (goto (insloc (((card I) + (card J)) + 3))) = 6 by SCMFSA_2:47;
A3: 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 ;
then ((card J) + 2) -' (card ((a =0_goto (insloc ((card J) + 3))) ';' J)) = 0 by 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 A3, 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 A3, A4, Th13
.= goto (insloc (((card I) + 1) + ((card J) + 2))) by A3, SCMFSA_4:14
.= goto (insloc (((card I) + (card J)) + (1 + 2))) ;
card (Goto (insloc ((card I) + 1))) = 1 by SCMFSA8A:29;
then card (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) = ((card J) + 2) + 1 by A3, SCMFSA6A:61
.= (card J) + (2 + 1) ;
then card (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) = ((card J) + 2) + 1 ;
then (card J) + 2 < card (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) by NAT_1:13;
then A6: 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, A2, A6, SCMFSA8A:30, SCMFSA_2:124 ;
hence (if=0 a,I,J) . (insloc ((card J) + 2)) = goto (insloc (((card I) + (card J)) + 3)) by A1, SCMFSA6A:67; :: thesis: verum