let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard without_implicit_jumps regular AMI-Struct of N
for I being Instruction of S st I is sequential holds
I is IC-good
let S be non empty stored-program IC-Ins-separated definite standard-ins standard without_implicit_jumps regular AMI-Struct of N; :: thesis: for I being Instruction of S st I is sequential holds
I is IC-good
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 17 :: thesis: for s1, s2 being State of S st s2 = s1 +* ((IC S) .--> ((IC s1) + k,S)) holds
(IC (Exec I,s1)) + k,S = IC (Exec (IncAddr I,k),s2)
let s1, s2 be State of S; :: thesis: ( s2 = s1 +* ((IC S) .--> ((IC s1) + k,S)) implies (IC (Exec I,s1)) + k,S = IC (Exec (IncAddr I,k),s2) )
assume A2: s2 = s1 +* ((IC S) .--> ((IC s1) + k,S)) ; :: thesis: (IC (Exec I,s1)) + k,S = IC (Exec (IncAddr I,k),s2)
dom ((IC S) .--> ((IC s1) + k,S)) = {(IC S)} by FUNCOP_1:19;
then IC S in dom ((IC S) .--> ((IC s1) + k,S)) by TARSKI:def 1;
then A3: IC s2 = ((IC S) .--> ((IC s1) + k,S)) . (IC S) by A2, FUNCT_4:14
.= il. S,((locnum (IC s1),S) + k) by FUNCOP_1:87 ;
A4: IC (Exec I,s2) = NextLoc (IC s2),S by A1, AMISTD_1:def 16
.= il. S,(((locnum (IC s1),S) + k) + 1) by A3, AMISTD_1:def 13
.= il. S,(((locnum (IC s1),S) + 1) + k) ;
IC (Exec I,s1) = NextLoc (IC s1),S by A1, AMISTD_1:def 16
.= il. S,((locnum (IC s1),S) + 1) ;
hence (IC (Exec I,s1)) + k,S = IC (Exec I,s2) by A4, AMISTD_1:def 13
.= IC (Exec (IncAddr I,k),s2) by A1, Th29 ;
:: thesis: verum