let a be Int-Location; :: thesis: for I, J being MacroInstruction 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 MacroInstruction 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;
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 11; :: thesis: verum