(def-language csm-0-language
    (base-types channel message))

(def-theory csm-0-theory 
    (language csm-0-language)
    (component-theories h-o-real-arithmetic the-kernel-theory))

(def-cartesian-product action
    (port message)
    (accessors channel message)
    (constructor build%action)
    (theory port-theory))

(def-language port-language
    (embedded-language csm-0-language)
    (sorts (port channel)))

(def-theory port-theory 
    (language port-language)
    (component-theories csm-0-theory))

(def-imported-rewrite-rules port-theory
    (source-theories pairs sequences))

(def-language csm-language
    (embedded-language port-theory)
    (base-types state)
    (constants 
      (next (state action state))
      (initial (state prop))))

(def-theory csm-theory 
    (component-theories h-o-real-arithmetic)
    (language csm-language))

(def-theory-ensemble-instances det-hoare-machines
    (target-theories csm-theory)
    (sorts 
      (state state)
      (action action))
    (constants
      (next  next)
      (initial initial))
    (multiples 1))

(def-theory-ensemble csm-theory
    (fixed-theories csm-0-theory))

(def-theory-ensemble-multiple csm-theory 3 (fixed-theories csm-0-theory))

(def-theory-ensemble-overloadings csm-theory (1) (fixed-theories csm-0-theory))

(def-cartesian-product composite%state
    (state_0 state_1 state_2)
    (constructor build%composite%state)
    (accessors component_0 component_1 component_2)
    (theory csm-theory-3-tuples))