let p be preProgram of SCM+FSA; for k being Nat holds UsedI*Loc p = UsedI*Loc (IncAddr (p,k))
let k be Nat; UsedI*Loc p = UsedI*Loc (IncAddr (p,k))
set A = { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng p } ;
set B = { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } ;
A1:
{ (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng p } c= { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) }
proof
let e be
object ;
TARSKI:def 3 ( not e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng p } or e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } )
assume
e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng p }
;
e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) }
then consider i being
Instruction of
SCM+FSA such that A2:
e = UsedInt*Loc i
and A3:
i in rng p
;
consider x being
object such that A4:
x in dom p
and A5:
p . x = i
by A3, FUNCT_1:def 3;
A6:
x in dom (IncAddr (p,k))
by A4, COMPOS_1:def 21;
(IncAddr (p,k)) . x =
IncAddr (
(p /. x),
k)
by A4, COMPOS_1:def 21
.=
IncAddr (
i,
k)
by A4, A5, PARTFUN1:def 6
;
then A7:
IncAddr (
i,
k)
in rng (IncAddr (p,k))
by A6, FUNCT_1:3;
e = UsedInt*Loc (IncAddr (i,k))
by A2, Th39;
hence
e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) }
by A7;
verum
end;
{ (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } c= { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng p }
proof
let e be
object ;
TARSKI:def 3 ( not e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } or e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng p } )
assume
e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) }
;
e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng p }
then consider i being
Instruction of
SCM+FSA such that A8:
e = UsedInt*Loc i
and A9:
i in rng (IncAddr (p,k))
;
consider x being
object such that A10:
x in dom (IncAddr (p,k))
and A11:
(IncAddr (p,k)) . x = i
by A9, FUNCT_1:def 3;
A12:
x in dom p
by A10, COMPOS_1:def 21;
p /. x = p . x
by A12, PARTFUN1:def 6;
then A13:
p /. x in rng p
by A12, FUNCT_1:3;
i = IncAddr (
(p /. x),
k)
by A12, COMPOS_1:def 21, A11;
then
e = UsedInt*Loc (p /. x)
by A8, Th39;
hence
e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng p }
by A13;
verum
end;
hence
UsedI*Loc p = UsedI*Loc (IncAddr (p,k))
by A1, XBOOLE_0:def 10; verum