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