let p be preProgram of SCM+FSA; :: thesis: for k being Nat holds UsedI*Loc p = UsedI*Loc (IncAddr (p,k))
let k be Nat; :: thesis: UsedI*Loc p = UsedI*Loc (IncAddr (p,k))
set A = { () where i is Instruction of SCM+FSA : i in rng p } ;
set B = { () 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= { () where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) }
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { () where i is Instruction of SCM+FSA : i in rng p } or e in { () where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } )
assume e in { () where i is Instruction of SCM+FSA : i in rng p } ; :: thesis: e in { () 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 ;
A6: x in dom (IncAddr (p,k)) by ;
e = UsedInt*Loc (IncAddr (i,k)) by ;
hence e in { () where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } by A7; :: thesis: verum
end;
{ (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } c= { () where i is Instruction of SCM+FSA : i in rng p }
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { () where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } or e in { () where i is Instruction of SCM+FSA : i in rng p } )
assume e in { () where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } ; :: thesis: e in { () 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 ;
A12: x in dom p by ;
p /. x = p . x by ;
then A13: p /. x in rng p by ;
i = IncAddr ((p /. x),k) by ;
then e = UsedInt*Loc (p /. x) by ;
hence e in { () where i is Instruction of SCM+FSA : i in rng p } by A13; :: thesis: verum
end;
hence UsedI*Loc p = UsedI*Loc (IncAddr (p,k)) by ; :: thesis: verum