(def-language language-op-semantics
    (base-types state value expr)
    (constants 
      (op%state (expr state state))
      (op%value (expr state value))))

(def-theory op-semantics 
    (language language-op-semantics)
    (component-theories h-o-real-arithmetic))
(load-section sequences)

(def-atomic-sort expr%seq 
    "lambda(f:[nn,expr], f_seq_q{f})"
    (theory op-semantics)
    (witness "lambda(x:nn, ?expr)"))

(def-atomic-sort state%seq 
    "lambda(f:[nn,state], f_seq_q{f})"
    (theory op-semantics)
    (witness "lambda(x:nn, ?state)"))

(def-recursive-constant opseq%state 
    "lambda(evs:[state, expr%seq, nn -> state], 
              lambda(env:state, f:expr%seq, n:nn, 
                                            if(n=0, op%state(f(0), env),
                                                  op%state(f(n), evs(env, f, n-1)))))"
    (theory op-semantics))