let I be Instruction of S; :: thesis: ( I is sequential implies I is IC-good )
assume A1: I is sequential ; :: 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 IC S in dom ((IC S) .--> ((IC s1) + k)) by TARSKI:def 1;
then A3: IC (IncrIC (s1,k)) = ((IC S) .--> ((IC s1) + k)) . (IC S) by FUNCT_4:14
.= (IC s1) + k by FUNCOP_1:87 ;
A4: IC (Exec (I,(IncrIC (s1,k)))) = succ (IC (IncrIC (s1,k))) by A1, AMISTD_1:def 16
.= ((IC s1) + 1) + k by A3 ;
IC (Exec (I,s1)) = succ (IC s1) by A1, AMISTD_1:def 16
.= (IC s1) + 1 ;
hence (IC (Exec (I,s1))) + k = IC (Exec ((IncAddr (I,k)),(IncrIC (s1,k)))) by A1, A4, COMPOS_1:92; :: thesis: verum