#!python
module NIL
{
  signature
  {
    [Nil]
    op nil : -> Nil
  }
}

#!python
module PROP
{
  signature
  {
    [ Bool < Prop ]
    op _/\_ : Prop Prop -> Prop { assoc comm prec: 55 }
    op _\/_ : Prop Prop -> Prop { assoc comm prec: 59 }
    op neg_ : Prop -> Prop { prec: 53 }
    op _=>_ : Prop Prop -> Prop
    op _<=>_ : Prop Prop -> Prop
  }
  axioms
  {
    vars P Q R : Prop
    eq false /\ P = false .
    eq true /\ P = P .
    eq P /\ P = P .
    eq true \/ P = true .
    eq false \/ P = P .
    eq P \/ P = P .
    eq neg true = false .
    eq neg false = true .
    eq neg neg P = P .
    eq P => true = true .
    eq P => false = neg(P) .
    eq true => P = P .
    eq false => P = true .
    eq P => P = true .
    eq P <=> Q = (P => Q) /\ (Q => P) .
  }
}

#!python
module NUMBER
{
  signature
  {
    [ Number ]
    op 0 : -> Number
    op s_ : Number -> Number
  }
}

#!python
module SET
(
  X :: TRIV
)
{
  imports
  {
    pr(NIL)
    ex(PROP)
    pr(NUMBER)
  }
  signature
  {
    [ Nil Elt < Set ]
    op _,_ : Set Set -> Set { assoc comm idem id: nil }
    op _@_ : Elt Set -> Prop
    op _\_ : Set Set -> Set
    op # : Set -> Number
  }
  axioms {
    vars X Y : Elt
    vars S T : Set
    eq (S,X = nil) = false .
    eq X @ nil = false .
    cq X @ (Y,S) = true
       if (X = Y) .
    cq X @ (Y,S) = X @ S
       if neg(X = Y) .
    eq nil \ S = nil .
    eq S \ nil = S .
    eq S \ (X,T) = (S \ X) \ T .
    eq (S,X) \ X = S .
    cq (S,Y) \ X = S \ X
       if (neg X = Y) .
    eq #(nil) = 0 .
    cq #(X,S) = s(#(S))
       if neg(X @ S) .
    cq #(X,S) = #(S)
       if (X @ S) .
  }
}

#!python
module LIST
(
  X :: TRIV
)
{
  imports
  {
    pr(NIL)
    pr(PROP)
    ex(NUMBER)
  }
  signature
  {
    [ Nil Elt < List ]
    op _;_ : List List -> List { assoc id: nil }
    op _@_ : Elt Nil -> Prop
    op _@_ : Elt Elt -> Prop
    op _@_ : Elt List -> Prop
    op _-_ : List Elt -> List
    op # : Nil -> Number
    op # : Elt -> Number
    op # : List -> Number
    op occur : List Elt -> Number
    op position : List Elt -> Number
  }
  axioms
  {
    vars X Y : Elt
    vars L F : List
    eq X @ nil =  false .
    cq X @ (Y;L) =  true
       if X = Y .
    cq X @ (Y;L) =  X @ L
       if neg(X = Y) .
    eq nil - X = nil .
    eq (X;L) - X = L .
    cq (Y;L) - X = Y;(L - X)
       if neg(X = Y) .
    eq #(nil) = 0 .
    eq #(L;X) = s(#(L)) .
    eq occur(nil,X) = 0 .
    eq occur((X;L),X) = s(occur(L,X)) .
    cq occur((Y;L),X) = occur(L,X)
       if neg(X = Y) .
    eq position((X;L),X) = 0 .
    cq position((X;L),Y) = s(position(L,X))
       if neg(X = Y) .
  }
}

#!python
module BAG
(
  X :: TRIV
)
{
  imports
  {
    pr(NIL)
    ex(PROP)
    pr(NUMBER)
  }
  signature
  {
    [ Nil Elt < Bag ]
    op _|_ : Bag Bag -> Bag { assoc comm id: nil }
    op _@_ : Elt Nil -> Prop
    op _@_ : Elt Elt -> Prop
    op _@_ : Elt Bag -> Prop
    op _sub_ : Bag Bag -> Bag
    op # : Nil -> Number
    op # : Elt -> Number
    op # : Bag -> Number
    op bag : Bag Elt -> Number
  }
  axioms {
    vars X Y : Elt
    vars S T : Bag
    eq (S | X = nil) = false .
    eq X @ nil = false .
    cq X @ (Y | S) = true
       if (X = Y) .
    cq X @ (Y | S) = X @ S
       if neg(X = Y) .
    eq nil sub S = nil .
    eq S sub nil = S .
    eq S sub (X | T) = (S sub X) sub T .
    eq (S | X) sub X = S .
    cq (S | Y) sub X = S sub X
       if (neg X = Y) .
    eq #(nil) = 0 .
    eq #(X | S) = s(#(S)) .
    eq bag(nil,X) = 0 .
    cq bag((Y | S),X) = bag(S,X)
       if (neg X = Y) .
    cq bag((Y | S),X) = s(bag(S,X))
       if (X = Y) .
  }
}