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 ) )
set J1 = (((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I;
A1: card ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) = (card (((Macro (a >0_goto ((card J) + 3))) ';' J) ';' (Goto ((card I) + 1)))) + (card I) by SCMFSA6A:61
.= ((card ((Macro (a >0_goto ((card J) + 3))) ';' J)) + (card (Goto ((card I) + 1)))) + (card I) by SCMFSA6A:61
.= ((card ((Macro (a >0_goto ((card J) + 3))) ';' J)) + 1) + (card I) by SCMFSA8A:29
.= (((card (Macro (a >0_goto ((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 ;
assume n < ((card I) + (card J)) + 3 ; :: thesis: ( n in dom (if>0 a,I,J) & (if>0 a,I,J) . n <> halt SCM+FSA )
then n in dom ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) by A1, SCMFSA6A:15;
then A2: n in dom (Directed ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) by FUNCT_4:105;
then A3: (Directed ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) . n in rng (Directed ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) by FUNCT_1:def 5;
if>0 a,I,J = ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ) by SCMFSA8B:def 2;
then A4: Directed ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) c= if>0 a,I,J by SCMFSA6A:55;
then dom (Directed ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) c= dom (if>0 a,I,J) by GRFUNC_1:8;
hence n in dom (if>0 a,I,J) by A2; :: thesis: (if>0 a,I,J) . n <> halt SCM+FSA
(if>0 a,I,J) . n = (Directed ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) . n by A2, A4, GRFUNC_1:8;
hence (if>0 a,I,J) . n <> halt SCM+FSA by A3, AMI_1:def 53; :: thesis: verum