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 EXTPRO_1:def 3 :: 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, EXTPRO_1:def 3
.= S by Th76 ; :: thesis: verum