let F be NAT -defined the InstructionsF of SCM -valued total Function; :: thesis: 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; :: 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:3

.= Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) ; :: thesis: verum

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; :: 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:3

.= Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) ; :: thesis: verum