let i be Instruction of SCM ; :: thesis: for I being Instruction of SCM+FSA st i = I & i is halting holds
I is halting
let I be Instruction of SCM+FSA ; :: 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 SCM+FSA ; :: according to AMI_1:def 8 :: thesis: Exec I,S = S
reconsider s = (S | SCM-Memory ) +* (NAT --> i) as State of SCM by Th73;
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