let F be NAT -defined the InstructionsF of SCM -valued total Function; for k being Nat
for s being State of SCM holds Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k)))
let k be Nat; for s being State of SCM holds Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k)))
let s be State of SCM; Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k)))
thus Comput (F,s,(k + 1)) =
Following (F,(Comput (F,s,k)))
by EXTPRO_1:3
.=
Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k)))
; verum