let a be Int-Location; 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 ; 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 ; ( 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
; ( 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; (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; verum