let j, i be Nat; :: according to AMISTD_2:def 3 :: thesis: for b₁ being set holds (IC (Exec ((IncAddr ((IncAddr (I,k)),j)),b₁))) + i = IC (Exec ((IncAddr ((IncAddr (I,k)),(j + i))),(IncIC (b₁,i))))
let s be State of S; :: thesis: (IC (Exec ((IncAddr ((IncAddr (I,k)),j)),s))) + i = IC (Exec ((IncAddr ((IncAddr (I,k)),(j + i))),(IncIC (s,i))))
thus (IC (Exec ((IncAddr ((IncAddr (I,k)),j)),s))) + i = (IC (Exec ((IncAddr (I,(k + j))),s))) + i by COMPOS_0:7
.= IC (Exec ((IncAddr (I,((k + j) + i))),(IncIC (s,i)))) by AMISTD_2:def 3
.= IC (Exec ((IncAddr (I,(k + (j + i)))),(IncIC (s,i))))
.= IC (Exec ((IncAddr ((IncAddr (I,k)),(j + i))),(IncIC (s,i)))) by COMPOS_0:7 ; :: thesis: verum