let F be NAT -defined the Instructions of SCM -valued total Function; :: thesis: for k being Element of 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 Element of NAT ; :: thesis: 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; :: 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:4
.= Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) ; :: thesis: verum