let I be Instruction of S; :: thesis: ( I is halting implies I is IC-good )
assume A1: I is halting ; :: thesis: I is IC-good
let k be natural number ; :: according to AMISTD_2:def 18 :: thesis: for s1 being State of S holds (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),(IncrIC s1,k))
let s1 be State of S; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),(IncrIC s1,k))
set s2 = IncrIC s1,k;
dom ((IC S) .--> ((IC s1) + k)) = {(IC S)} by FUNCOP_1:19;
then A3: IC S in dom ((IC S) .--> ((IC s1) + k)) by TARSKI:def 1;
thus (IC (Exec I,s1)) + k = (IC s1) + k by A1, AMI_1:def 8
.= ((IC S) .--> ((IC s1) + k)) . (IC S) by FUNCOP_1:87
.= IC (IncrIC s1,k) by A3, FUNCT_4:14
.= IC (Exec I,(IncrIC s1,k)) by A1, AMI_1:def 8
.= IC (Exec (IncAddr I,k),(IncrIC s1,k)) by A1, Th29 ; :: thesis: verum