let a be Int-Location; for I being MacroInstruction of SCM+FSA holds UsedILoc (if=0 (a,(I ';' (goto 0)))) = UsedILoc ((if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)))
let I be MacroInstruction of SCM+FSA ; UsedILoc (if=0 (a,(I ';' (goto 0)))) = UsedILoc ((if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)))
set I1 = I ';' (goto 0);
set Lc4 = (card I) + 2;
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;
UsedIntLoc pc =
UsedIntLoc (goto (0 + ((card I) + 2)))
by Lm1, A1
.=
{}
by SF_MASTR:15
.=
UsedIntLoc (goto 0)
by SF_MASTR:15
;
hence
UsedILoc (if=0 (a,(I ';' (goto 0)))) = UsedILoc ((if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)))
by SCMFSA_9:49; verum