let p be preProgram of SCM+FSA; :: thesis: for l being Nat

for ic being Instruction of SCM+FSA st ex pc being Instruction of SCM+FSA st

( pc = p . l & UsedIntLoc pc = UsedIntLoc ic ) holds

UsedILoc p = UsedILoc (p +* (l,ic))

let l be Nat; :: thesis: for ic being Instruction of SCM+FSA st ex pc being Instruction of SCM+FSA st

( pc = p . l & UsedIntLoc pc = UsedIntLoc ic ) holds

UsedILoc p = UsedILoc (p +* (l,ic))

let ic be Instruction of SCM+FSA; :: thesis: ( ex pc being Instruction of SCM+FSA st

( pc = p . l & UsedIntLoc pc = UsedIntLoc ic ) implies UsedILoc p = UsedILoc (p +* (l,ic)) )

given pc being Instruction of SCM+FSA such that A1: pc = p . l and

A2: UsedIntLoc pc = UsedIntLoc ic ; :: thesis: UsedILoc p = UsedILoc (p +* (l,ic))

{ (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng p } = { (UsedIntLoc j) where j is Instruction of SCM+FSA : j in rng (p +* (l,ic)) } from FUNCT_7:sch 7(A2, A1);

hence UsedILoc p = UsedILoc (p +* (l,ic)) ; :: thesis: verum

for ic being Instruction of SCM+FSA st ex pc being Instruction of SCM+FSA st

( pc = p . l & UsedIntLoc pc = UsedIntLoc ic ) holds

UsedILoc p = UsedILoc (p +* (l,ic))

let l be Nat; :: thesis: for ic being Instruction of SCM+FSA st ex pc being Instruction of SCM+FSA st

( pc = p . l & UsedIntLoc pc = UsedIntLoc ic ) holds

UsedILoc p = UsedILoc (p +* (l,ic))

let ic be Instruction of SCM+FSA; :: thesis: ( ex pc being Instruction of SCM+FSA st

( pc = p . l & UsedIntLoc pc = UsedIntLoc ic ) implies UsedILoc p = UsedILoc (p +* (l,ic)) )

given pc being Instruction of SCM+FSA such that A1: pc = p . l and

A2: UsedIntLoc pc = UsedIntLoc ic ; :: thesis: UsedILoc p = UsedILoc (p +* (l,ic))

{ (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng p } = { (UsedIntLoc j) where j is Instruction of SCM+FSA : j in rng (p +* (l,ic)) } from FUNCT_7:sch 7(A2, A1);

hence UsedILoc p = UsedILoc (p +* (l,ic)) ; :: thesis: verum