let I, J be Program of SCM+FSA ; :: thesis: for a being Int-Location holds (if=0 a,I,J) . (insloc (((card I) + (card J)) + 3)) = halt SCM+FSA
let a be Int-Location ; :: thesis: (if=0 a,I,J) . (insloc (((card I) + (card J)) + 3)) = halt SCM+FSA
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;
set II = (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I;
A2: card ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) = (card (((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J) ';' (Goto (insloc ((card I) + 1))))) + (card I) by SCMFSA6A:61
.= ((card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + (card (Goto (insloc ((card I) + 1))))) + (card I) by SCMFSA6A:61
.= ((card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + 1) + (card I) by SCMFSA8A:29
.= (((card (Macro (a =0_goto (insloc ((card J) + 3))))) + (card J)) + 1) + (card I) by SCMFSA6A:61
.= ((2 + (card J)) + 1) + (card I) by SCMFSA7B:6
.= ((card I) + (card J)) + 3 ;
then A3: ((card I) + (card J)) + 3 < (card ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) + (card (Stop SCM+FSA )) by NAT_1:13, SCMFSA8A:17;
(((card I) + (card J)) + 3) -' (card ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) = 0 by A2, XREAL_1:234;
hence (if=0 a,I,J) . (insloc (((card I) + (card J)) + 3)) = IncAddr (halt SCM+FSA ),(card ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) by A1, A2, A3, Th13, SCMFSA8A:16
.= halt SCM+FSA by SCMFSA_4:8 ;
:: thesis: verum