1 files changed, 36 insertions, 1 deletions
diff --git a/README.md b/README.md
index ee7b099..9441dd4 100644
--- a/README.md
+++ b/README.md
@@ -1,2 +1,37 @@
 # Theorem prover in ts types
-Experiment to use typescript's type system for theorem proving
+Experiment to use typescript's type system to make a shitty theorem prover.
+
+
+### Commutativity of addition in ts types or something?
+
+```typescript
+export type Commutativity<A extends Op, B extends Op> = Rewrite<Add<A, B>, Add<B, A>>;
+
+export interface Comm_Base_Proof<B extends Op> {
+  type: 'rewrite',
+  left: Equation<Add<_0, B>, Add<B, _0>>; // 0 + b = b + 0
+  right: ChainRewrites<[
+    IdentityR<B>,         // b = b + 0
+    Sym<Identity<B>>,     // b + 0 = b + 0
+    Refl<Add<B, _0>>,     // true
+  ], this['left']>;
+};
+
+export interface Comm_Inductive_Proof<A extends Op, B extends Op> {
+  type: 'rewrite',
+  left: Equation<Add<Succ<A>, B>, Add<B, Succ<A>>>;  // succ(a) + b = b + succ(a)
+  right: ChainRewrites<[
+    SumSucc<A, B>,          // succ(a + b) = b + succ(a)
+    Commutativity<A, B>,    // succ(b + a) = b + succ(a)
+    SumSuccR<B, A>,         // succ(b + a) = succ(b + a)
+    Refl<Succ<Add<B, A>>>,  // true
+  ], this['left']>;
+};
+
+export namespace spec {
+  export type commutativity = [
+    assert<VerifyEquation<Comm_Base_Proof<'B'>>>,
+    assert<VerifyEquation<Comm_Inductive_Proof<'A', 'B'>>>,
+  ]
+}
+```