let I be Instruction of ; :: thesis: for S being State of
for s being State of st S = (s | SCM-Memory ) +* (NAT --> I) holds
IC s = IC S
let S be State of ; :: thesis: for s being State of st S = (s | SCM-Memory ) +* (NAT --> I) holds
IC s = IC S
let s be State of ; :: 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