let a be Int-Location; for I being MacroInstruction of SCM+FSA holds UsedI*Loc (if=0 (a,(I ';' (goto 0)))) = UsedI*Loc ((if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)))
let I be MacroInstruction of SCM+FSA ; UsedI*Loc (if=0 (a,(I ';' (goto 0)))) = UsedI*Loc ((if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)))
set Lc4 = (card I) + 2;
set IG = I ';' (goto 0);
set if0 = if=0 (a,(I ';' (goto 0)));
A1: (card I) + 2 =
((card I) + 1) + 1
.=
(card (I ';' (goto 0))) + 1
by COMPOS_2:11
;
A2:
card (if=0 (a,(I ';' (goto 0)))) = (card (I ';' (goto 0))) + 4
by SCMFSA_X:1;
(card I) + 2 < (card (I ';' (goto 0))) + 4
by XREAL_1:6, A1;
then A3:
(card I) + 2 in dom (if=0 (a,(I ';' (goto 0))))
by A2, AFINSQ_1:66;
A4:
(if=0 (a,(I ';' (goto 0)))) . ((card I) + 2) in rng (if=0 (a,(I ';' (goto 0))))
by A3, FUNCT_1:3;
rng (if=0 (a,(I ';' (goto 0)))) c= the InstructionsF of SCM+FSA
by RELAT_1:def 19;
then reconsider pc = (if=0 (a,(I ';' (goto 0)))) . ((card I) + 2) as Instruction of SCM+FSA by A4;
UsedInt*Loc pc =
UsedInt*Loc (goto (0 + ((card I) + 2)))
by Lm1, A1
.=
{}
by SF_MASTR:32
.=
UsedInt*Loc (goto 0)
by SF_MASTR:32
;
hence
UsedI*Loc (if=0 (a,(I ';' (goto 0)))) = UsedI*Loc ((if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)))
by SCMFSA_9:50; verum