SimonForest

record MyS
  (State : Set)
  (Operation : (f g : State) → Set)
  (Change : {f g : State} (O : Operation f g) → Set)
  :
  Set
  where

data Left-state : Set where
  Left-notdone : Left-state

SimonForest

record MyS
  (State : Set)
  (Operation : (f g : State) → Set)
  (Change : {f g : State} (O : Operation f g) → Set)
  :
  Set
  where
  field
    comp : {f f' f'' : State} (F : Operation f f') (G : Operation f' f'') → Operation f f''

SimonForest

(set-option :global-decls false)
(set-option :smt.mbqi false)
(declare-sort Ref)
(declare-fun Ref_constr_id (Ref) Int)

(declare-sort String)
(declare-fun String_constr_id (String) Int)

(declare-sort Kind)
(declare-fun Kind_constr_id (Kind) Int)

SimonForest

(set-option :global-decls false)
(set-option :smt.mbqi false)
(declare-sort Ref)
(declare-fun Ref_constr_id (Ref) Int)

(declare-sort String)
(declare-fun String_constr_id (String) Int)

(declare-sort Kind)
(declare-fun Kind_constr_id (Kind) Int)