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));
card (Goto (insloc 2)) = 1 by SCMFSA8A:29;
then A1: 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;
A2: 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 A3: card (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc 2))) = ((card J) + 2) + 1 by A2, SCMFSA6A:61
.= (card J) + (2 + 1) ;
then A4: card ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc 2))) ';' (Goto (insloc 2))) = ((card J) + 3) + 1 by A2, SCMFSA6A:61
.= (card J) + (3 + 1) ;
((card J) + 3) -' (card (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc 2)))) = 0 by A3, XREAL_1:234;
then A5: 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 A3, NAT_1:13;
then A6: ((((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 A3, A5, Th13
.= goto (insloc (2 + ((card J) + 3))) by A3, SCMFSA_4:14
.= goto (insloc ((card J) + (2 + 3))) ;
A7: ( 6 <> 0 & InsCode (goto (insloc ((card J) + 5))) = 6 & InsCode (halt SCM+FSA ) = 0 ) by SCMFSA_2:47, SCMFSA_2:124;
card ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc 2))) ';' (Goto (insloc 2))) = ((card J) + 3) + 1 by A4;
then (card J) + 3 < card ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc 2))) ';' (Goto (insloc 2))) by NAT_1:13;
then A8: 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 A6, A7, A8, SCMFSA8A:30 ;
hence (if=0 a,(Goto (insloc 2)),J) . (insloc ((card J) + 3)) = goto (insloc ((card J) + 5)) by A1; :: thesis: verum