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