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:21
.= ((card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + (card (Goto ((card I) + 1)))) + (card I) by SCMFSA6A:21
.= ((card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + 1) + (card I) by SCMFSA8A:15
.= (((card (Macro (a =0_goto ((card J) + 3)))) + (card J)) + 1) + (card I) by SCMFSA6A:21
.= ((2 + (card J)) + 1) + (card I) by COMPOS_1:56
.= ((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, AFINSQ_1:66;
then A2: n in dom (Directed ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) by FUNCT_4:99;
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 3;
if=0 (a,I,J) = ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) by SCMFSA8B:def 1;
then A4: Directed ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) c= if=0 (a,I,J) by SCMFSA6A:16;
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:2;
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:2;
hence (if=0 (a,I,J)) . n <> halt SCM+FSA by A3, COMPOS_1:def 3; :: thesis: verum