namespace http://cds.omdoc.org/examples❚

theory Magma : ?FOLEQNatDed =
  op : term ⟶ term ⟶ term ❘# 1 ∘ 2 prec 50❙
❚

theory Semigroup : ?FOLEQNatDed =
  include ?Magma❙
  assoc: {x,y,z} ⊦ (x∘y)∘z ≐ x∘(y∘z)❙
  
  assocR: {x,y,z} ⊦ x∘(y∘z) ≐ (x∘y)∘z❘
        = [x,y,z] sym assoc❙

  assoc4:  {w,x,y,z} ⊦ ((w∘x)∘y)∘z ≐ w∘(x∘(y∘z))❘
        =  [w,x,y,z] trans3 (congT assoc [u]u∘z) assoc (congT assoc [u]w∘u)❙
  assoc4R: {w,x,y,z} ⊦ w∘(x∘(y∘z)) ≐ ((w∘x)∘y)∘z❘
        = [w,x,y,z] sym assoc4❙
  assoc5: {v,w,x,y,z} ⊦ (((v∘w)∘x)∘y)∘z ≐ v∘(w∘(x∘(y∘z)))❘
        = [v,w,x,y,z] trans4 (congT assoc4 [u]u∘z) assoc
                              (congT assoc [u]v∘u) (congT assoc [u]v∘(w∘u))❙
❚

theory Commutative : ?FOLEQNatDed =
  include ?Magma❙
  comm: {x,y} ⊦ x∘y ≐ y∘x❙
❚

theory Neutral : ?FOLEQNatDed =
  include ?Magma❙
  e  : term ❙  
  neutLeft: {x} ⊦ x∘e ≐ x❙
  neutRight: {x} ⊦ x∘e ≐ x❙
❚

theory Idempotent : ?FOLEQNatDed =
  include ?Magma❙
  idempotent: {x} ⊦ x∘x ≐ x❙
❚

theory Monoid : ?FOLEQNatDed =
  include ?Semigroup❙
  include ?Neutral❙
❚

theory Band : ?FOLEQNatDed =
  include ?Semigroup❙
  include ?Idempotent❙
❚

theory Semilattice : ?FOLEQNatDed =
  include ?Band❙
  include ?Commutative❙
❚