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