let I be Instruction of SCM; :: thesis: for S being State of SCM
for s being State of SCM+FSA st S = (s | SCM-Memory) +* (NAT --> I) holds
IC s = IC S
let S be State of SCM; :: thesis: for s being State of SCM+FSA st S = (s | SCM-Memory) +* (NAT --> I) holds
IC s = IC S
let s be State of SCM+FSA; :: thesis: ( S = (s | SCM-Memory) +* (NAT --> I) implies IC s = IC S )
assume S = (s | SCM-Memory) +* (NAT --> I) ; :: thesis: IC s = IC S
then s = (s +* S) +* (s | NAT) by Th76;
hence IC s = IC S by Th78; :: thesis: verum