let a be Int-Location ; :: thesis: for I, J being Program of SCM+FSA
for n being Element of NAT st n < ((card I) + (card J)) + 3 holds
( n in dom (if>0 a,I,J) & (if>0 a,I,J) . n <> halt SCM+FSA )
let I, J be Program of SCM+FSA ; :: thesis: for n being Element of NAT st n < ((card I) + (card J)) + 3 holds
( n in dom (if>0 a,I,J) & (if>0 a,I,J) . n <> halt SCM+FSA )
let n be Element of NAT ; :: thesis: ( n < ((card I) + (card J)) + 3 implies ( n in dom (if>0 a,I,J) & (if>0 a,I,J) . n <> halt SCM+FSA ) )
assume A1: n < ((card I) + (card J)) + 3 ; :: thesis: ( n in dom (if>0 a,I,J) & (if>0 a,I,J) . n <> halt SCM+FSA )
A2: 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 2;
set J1 = (((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I;
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 insloc n in dom ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) by A1, SCMFSA6A:15;
then A3: insloc n in dom (Directed ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) by FUNCT_4:105;
Directed ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) c= if>0 a,I,J by A2, SCMFSA6A:55;
then A4: ( dom (Directed ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) c= dom (if>0 a,I,J) & (if>0 a,I,J) . (insloc n) = (Directed ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) . (insloc n) ) by A3, GRFUNC_1:8;
hence n in dom (if>0 a,I,J) by A3; :: thesis: (if>0 a,I,J) . n <> halt SCM+FSA
(Directed ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) . (insloc n) in rng (Directed ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) by A3, FUNCT_1:def 5;
hence (if>0 a,I,J) . n <> halt SCM+FSA by A4, AMI_1:def 52; :: thesis: verum