for N being with_zero set
for I being Instruction of (STC N)
for s being State of (STC N)
for k being Nat holds Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)