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 & UsedInt*Loc pc = UsedInt*Loc ic ) holds
UsedI*Loc p = UsedI*Loc (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 & UsedInt*Loc pc = UsedInt*Loc ic ) holds
UsedI*Loc p = UsedI*Loc (p +* (l,ic))
let ic be Instruction of SCM+FSA; :: thesis: ( ex pc being Instruction of SCM+FSA st
( pc = p . l & UsedInt*Loc pc = UsedInt*Loc ic ) implies UsedI*Loc p = UsedI*Loc (p +* (l,ic)) )
given pc being Instruction of SCM+FSA such that A1: pc = p . l and
A2: UsedInt*Loc pc = UsedInt*Loc ic ; :: thesis: UsedI*Loc p = UsedI*Loc (p +* (l,ic))
{ (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng p } = { (UsedInt*Loc j) where j is Instruction of SCM+FSA : j in rng (p +* (l,ic)) } from FUNCT_7:sch 7(A2, A1);
hence UsedI*Loc p = UsedI*Loc (p +* (l,ic)) ; :: thesis: verum