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