# example KB

```#one = two should not be provable
typeside EmptySortsCheck = literal {
types
Void
nat
constants
one two : nat
equations
forall x:Void. one = two
options
prover = completion
#		completion_precedence = "one two"
}

typeside Group = literal {
types
S
constants
e : S
functions
I : S -> S
o : S,S -> S
equations
forall x. (e o x) = x
forall x. (I(x) o x) = e
forall x, y, z. ((x o y) o z) = (x o (y o z))
options
prover = completion
#		completion_precedence = "e o I"
}

typeside LR = literal {
types
S
constants
e : S
functions
I : S -> S
o : S,S -> S
equations
forall x. o(e,x) = x
forall x. o(x,I(x)) = e
forall x y z. o(o(x,y),z)=o(x,o(y,z))
options
prover = completion
#		completion_precedence = "e o I"
}

typeside RL = literal {
types
S
constants
e : S
functions
I : S -> S
o : S,S -> S
equations
forall x. o(x,e) = x
forall x. o(I(x),x) = e
forall x, y, z. o(o(x,y),z)=o(x,o(y,z))
options
prover = completion
#		completion_precedence = "e o I"
}

typeside Arith = literal {
types
N
constants
zero : N
functions
succ : N -> N
plus : N,N -> N
times : N,N -> N
equations
forall x. plus(zero, x) = x
forall x, y. plus(succ(x),y) = succ(plus(x,y))
forall x. times(zero, x) = zero
forall x, y. times(succ(x),y) = plus(y,times(x,y))
options
prover = completion
#		completion_precedence = "zero succ plus times"
}

#try ((a o b) o (c o d)) = ((a o c) o (b o d)) and
#forall p q r s. ((p o q) o (r o s)) = ((p o r) o (q o s))
typeside Entropic = literal {
types
S
constants
a b c d : S
functions
o : S,S -> S
equations
forall x, y, z, w. o(o(x,y),o(z,w)) = o(o(x,z),o(y,w))
forall x, y. o(o(x,y),x) = x
options
prover = completion
completion_precedence = "o a b c d"
}

typeside ACUIN = literal {
types
S
constants
e : S
functions
n : S -> S
o : S,S -> S
equations
forall x, y, z. o(o(x,y),z) = o(x,o(y,z))
forall x, y. o(x,y) = o(y,x)
forall x. o(x, e) = x
#		forall x. o(x, x) = x
options
prover = completion
completion_precedence = "e n o"
#		completion_syntactic_ac = true
#		timeout = 10
}

typeside DistributiveLattice = literal {
types
DL
constants
t f : DL
functions
n : DL, DL -> DL
u : DL, DL -> DL
equations
forall x. (x n t)=x
forall x y. (y n x) = (x n y)
forall x y z. (x n (y n z)) = ((x n y) n z)
forall x. (x n f)=f
forall x. (x u f)=x
forall x y. (y u x) = (x u y)
forall x y z. (x u (y u z)) = ((x u y) u z)
forall x. (x u t) = t
#forall x y z. (x n (y u z)) = ((x n y) u (x n z))
options
prover=completion
completion_precedence = "t f n u"
}

# still too hard
#
#typeside BooleanRing = literal {
#	types
#		S
#	constants
#		zero one : S
#	functions
#		plus times : S,S -> S
#	equations
#		forall x y z.  plus(plus(x,y),z) = plus(x,plus(y,z))
#		forall x y z.  times(times(x,y),z) = times(x,times(y,z))
#		forall x y. plus(x,y) = plus(y,x)
#		forall x y. times(x,y) = times(y,x)
#		forall x y, z. plus(x,plus(y,z)) = plus(y,plus(x,z))
#		forall x y, z. times(x,times(y,z)) = times(y,times(x,z))
#		forall x y, z. times(x,plus(y,z)) = plus(times(x,y),times(x,z))
#		forall x y, z. times(plus(x,y),z) = plus(times(x,z),times(y,z))
#		forall x. plus(zero,x) = x
#		forall x. plus(x,zero) = x
#		forall x. times(one,x) = x
#		forall x. times(x,one) = x
#		forall x. times(zero,x) = zero
#		forall x. times(x,zero) = zero
#		forall x. plus(x,x) = zero
#		forall x. times(x,x) = x
#		forall x y. plus(x,plus(x,y)) = y
#		forall x y. times(x,times(x,y)) = times(x,y)
#	options
#		prover = completion
#		completion_precedence = "zero one plus times"
#}
```
Keywords:

typeside_literal

Options:

prover
completion_precedence