1 files changed, 28 insertions, 0 deletions
diff --git a/src/tests/theorem.spec.ts b/src/tests/theorem.spec.ts
new file mode 100644
index 0000000..4ab220a
--- /dev/null
+++ b/src/tests/theorem.spec.ts
@@ -0,0 +1,28 @@
+import { addition } from '../natural-numbers';
+import { Add, _0 } from '../utils/nat';
+import { ApplyRewrite, ChainRewrites, Sym, Eq, VerifyEquation, Equation, assert, Evaluate } from '../utils/theorem';
+
+export type specChainRewrites = [
+  assert<Eq<
+    ChainRewrites<
+      [
+        addition.Commutativity<_0, 'B'>,
+        addition.Identity<'B'>,
+      ],
+      Add<Add<_0, 'B'>, 'C'>
+    >,
+    Add<'B', 'C'>
+  >>,
+  assert<Eq<
+    ChainRewrites<
+      [
+        addition.Commutativity<_0, 'B'>,
+        addition.Identity<'B'>,
+        Sym<addition.Identity<Add<'B', 'C'>>>,
+        addition.Commutativity<Add<'B', 'C'>, _0>,
+      ],
+      Add<Add<_0, 'B'>, 'C'>
+    >,
+    Add<_0, Add<'B', 'C'>>
+  >>,
+]