let k be Nat; :: thesis: for s being State of SCM
for F being NAT -defined the InstructionsF of SCM -valued total Function holds Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k)))
let s be State of SCM; :: thesis: for F being NAT -defined the InstructionsF of SCM -valued total Function holds Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k)))
let F be NAT -defined the InstructionsF of SCM -valued total Function; :: thesis: 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))) ; :: thesis: verum