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