Returning players! Wiki accounts were reset in late 2014. If you haven't played since then and wish to edit the wiki, you'll need a fresh account.

# Axioms

1. For all a and b, (a,b) is an ordered pair.
2. For all a, b, c and d, (a,b) = (c,d) if and only if a = c and b = d.
3. There exists exactly one a such that a is an empty list.
4. For all a and b, if b is a list, then {a}:b is a non-empty list.
5. For all a, if a is a non-empty list, then there exist b and c such that a = {b}:c and c is a list.
6. For all a, b, c, and d, if b and d are lists, then [{a}:b = {c}:d if and only if [a = c and b = d]].
7. For all a and b, if b is a list, then [the head of {a}:b is a, and the tail of {a}:b is b].
8. For all a, b and c, if c is a list, then [a is an element of {b}:c if and only if [a = b or a is an element of c]]
9. For all a, a is not an element of the empty list.
10. For all a, b and c, if b and c are lists, then ({a}:b) ++ c = {a}:(b ++ c).
11. For all c, if c is a list, then {} ++ c = c (where {} is the empty list).
12. For all Atoms X and Y, X * Y is an Atom.
13. E is an Atom. For all Atoms X, E * X = X and X * E = X.
14. For all Atoms X, [X’ is an Atom, and X * X’ = E and X’ * X = E].

# Theorems

1. {A}:::{B}&&{B}:::{C}&&{C}:::{A} = 0