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 as State of SCM by Th42;
thus Exec (I,S) = S +* (Exec (i,s)) by A1, Th44
.= S +* s by A2
.= S by Th45 ; :: thesis: verum