let p be preProgram of SCM+FSA; :: thesis: for k being Nat holds UsedILoc p = UsedILoc (IncAddr (p,k))

let k be Nat; :: thesis: UsedILoc p = UsedILoc (IncAddr (p,k))

set A = { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng p } ;

set B = { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } ;

A1: { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng p } c= { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) }

let k be Nat; :: thesis: UsedILoc p = UsedILoc (IncAddr (p,k))

set A = { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng p } ;

set B = { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } ;

A1: { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng p } c= { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) }

proof

{ (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } c= { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng p }
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng p } or e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } )

assume e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng p } ; :: thesis: e in { (UsedIntLoc 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 = UsedIntLoc 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 = UsedIntLoc (IncAddr (i,k)) by A2, Th23;

hence e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } by A7; :: thesis: verum

end;assume e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng p } ; :: thesis: e in { (UsedIntLoc 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 = UsedIntLoc 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 = UsedIntLoc (IncAddr (i,k)) by A2, Th23;

hence e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } by A7; :: thesis: verum

proof

hence
UsedILoc p = UsedILoc (IncAddr (p,k))
by A1, XBOOLE_0:def 10; :: thesis: verum
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } or e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng p } )

assume e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } ; :: thesis: e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng p }

then consider i being Instruction of SCM+FSA such that

A8: e = UsedIntLoc 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 = UsedIntLoc (p /. x) by A8, Th23;

hence e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng p } by A13; :: thesis: verum

end;assume e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (IncAddr (p,k)) } ; :: thesis: e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng p }

then consider i being Instruction of SCM+FSA such that

A8: e = UsedIntLoc 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 = UsedIntLoc (p /. x) by A8, Th23;

hence e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng p } by A13; :: thesis: verum