let i be Instruction of ; :: thesis: for I being Instruction of st i = I & i is halting holds
I is halting
let I be Instruction of ; :: thesis: ( i = I & i is halting implies I is halting )
assume A1: i = I ; :: thesis: ( not i is halting or I is halting )
assume A2: i is halting ; :: thesis: I is halting
let S be State of ; :: according to AMI_1:def 8 :: thesis: Exec I,S = S
reconsider s = (S | SCM-Memory ) +* (NAT --> i) as State of by SCMFSA_1:18;
thus Exec I,S = (S +* (Exec i,s)) +* (S | NAT ) by A1, Th75
.= (S +* s) +* (S | NAT ) by A2, AMI_1:def 8
.= S by Th76 ; :: thesis: verum