From 302ce999a2a1590825510d9d488371ab590f2dfe Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 13:54:35 -0800
Subject: [PATCH 01/67] Autoformat

---
 src/Logic/Prover.ts | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index ac80fed..100cb00 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -29,9 +29,9 @@ export type Derivation<TheoremId = Id, PropertyId = Id> = {
 }
 type Result<TheoremId = Id, PropertyId = Id> =
   | {
-      kind: 'contradiction'
-      contradiction: Contradiction<TheoremId, PropertyId>
-    }
+    kind: 'contradiction'
+    contradiction: Contradiction<TheoremId, PropertyId>
+  }
   | { kind: 'derivations'; derivations: Derivation<TheoremId, PropertyId>[] }
 
 // Given a collection of implications and a collection of traits for an object,
@@ -116,7 +116,7 @@ class Prover<
     TheoremId,
     PropertyId
   >
-> {
+  > {
   private traits: Map<PropertyId, boolean>
 
   private given: Set<PropertyId>
@@ -288,9 +288,9 @@ class Prover<
       (
         acc:
           | {
-              falses: Formula<PropertyId>[]
-              unknown: Formula<PropertyId> | undefined
-            }
+            falses: Formula<PropertyId>[]
+            unknown: Formula<PropertyId> | undefined
+          }
           | undefined,
         sf: Formula<PropertyId>
       ) => {

From 8a0af8f9a273dfbbd125365ce4020c6cbdfebac3 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 13:52:42 -0800
Subject: [PATCH 02/67] Introduce problem

---
 src/Logic/Prover.ts | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 100cb00..12e10e1 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -146,6 +146,21 @@ class Prover<
       }
     }
 
+    // Problem: we have recorded proofs of the form
+    //
+    //   Property P holds by theorem T and supporting properties [P1, P2, ...]
+    //
+    // where the supporting properties _may_ also be properties we've dervied,
+    // which have their own proofs. We're currently expanding those out to
+    // proofs "from first principles" of the form
+    //
+    //   ... by theorems [T1, T2, ...] and supporting properties [P1, P2, ...]
+    //
+    // where each supporting property is in our list of initial assumptions.
+    //
+    // Instead of always unconditionally expanding proofs, we want to introduce
+    // an object that holds on to all of the supporting proof metadata, and can
+    // expand that out to full proofs on demand.
     const derivations: Derivation<TheoremId, PropertyId>[] = []
     this.traits.forEach((value: boolean, property: PropertyId) => {
       const proof = this.proof(property)

From 8d49233706a541279e93d6cbb3f6524af885c8fc Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 13:54:52 -0800
Subject: [PATCH 03/67] Introduce class

This class will end up holding on to our derivation list
---
 src/Logic/Prover.ts | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 12e10e1..83dcf94 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -109,6 +109,10 @@ export function proveTheorem<TheoremId = Id, PropertyId = Id>(
   }
 }
 
+class Derivations {
+
+}
+
 class Prover<
   TheoremId = Id,
   PropertyId = Id,

From aba8719b51b8b252437d881826186d1dad198e59 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 13:56:58 -0800
Subject: [PATCH 04/67] Add inner Derivations instance

that the Prover can start to collaborate with. We'll start moving _some_ of the existing prover state over to this object over the next several commits.
---
 src/Logic/Prover.ts | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 83dcf94..ca34a53 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -122,6 +122,7 @@ class Prover<
   >
   > {
   private traits: Map<PropertyId, boolean>
+  private derivations: Derivations
 
   private given: Set<PropertyId>
   private evidence: Map<PropertyId, Evidence<TheoremId, PropertyId>>
@@ -132,6 +133,7 @@ class Prover<
     traits: Map<PropertyId, boolean> = new Map()
   ) {
     this.traits = traits
+    this.derivations = new Derivations()
     this.given = new Set([...traits.keys()])
     this.evidence = new Map()
     this.queue = new Queue(implications)

From 1e47df421240e87b7763e275dc22a612240a5f05 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 13:58:49 -0800
Subject: [PATCH 05/67] Indicate next target statement

We want to replace this line with a call to the new derivations object. This is the API we'll need it to implement.
---
 src/Logic/Prover.ts | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index ca34a53..ce51e19 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -174,6 +174,7 @@ class Prover<
         return
       }
 
+      // this.derivations.add({ property, value, proof })
       derivations.push({ property, value, proof })
     })
 

From 49be1ea843f56327523308f312f1fcee33100a27 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:00:52 -0800
Subject: [PATCH 06/67] Introduce Derivations#add method

currently a no-op, just to ensure that we can get the intended signature to typecheck.
---
 src/Logic/Prover.ts | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index ce51e19..b218112 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -109,8 +109,14 @@ export function proveTheorem<TheoremId = Id, PropertyId = Id>(
   }
 }
 
-class Derivations {
+class Derivations<TheoremId, PropertyId> {
+  add(_: {
+    property: PropertyId,
+    value: boolean,
+    proof: Proof<TheoremId, PropertyId>
+  }) {
 
+  }
 }
 
 class Prover<
@@ -122,7 +128,7 @@ class Prover<
   >
   > {
   private traits: Map<PropertyId, boolean>
-  private derivations: Derivations
+  private derivations: Derivations<TheoremId, PropertyId>
 
   private given: Set<PropertyId>
   private evidence: Map<PropertyId, Evidence<TheoremId, PropertyId>>

From bd7e49ebf50b05d4652022cb7845547c5240fb06 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:01:59 -0800
Subject: [PATCH 07/67] Call the new method

Still no-ops, but ensures the call site typechecks.
---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index b218112..c6afd1b 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -180,7 +180,7 @@ class Prover<
         return
       }
 
-      // this.derivations.add({ property, value, proof })
+      this.derivations.add({ property, value, proof })
       derivations.push({ property, value, proof })
     })
 

From 0cedf3930c6830cf80bfe9cf7610b805bd56002c Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:04:12 -0800
Subject: [PATCH 08/67] Add constructor

as we'll need to start holding state in this class
---
 src/Logic/Prover.ts | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index c6afd1b..e0788cf 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -110,6 +110,9 @@ export function proveTheorem<TheoremId = Id, PropertyId = Id>(
 }
 
 class Derivations<TheoremId, PropertyId> {
+  constructor() {
+  }
+
   add(_: {
     property: PropertyId,
     value: boolean,

From a2d30d84679789a06c82af7c5146ed654f4e2186 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:05:11 -0800
Subject: [PATCH 09/67] Add initial state

---
 src/Logic/Prover.ts | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index e0788cf..f6214f0 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -110,7 +110,10 @@ export function proveTheorem<TheoremId = Id, PropertyId = Id>(
 }
 
 class Derivations<TheoremId, PropertyId> {
+  private derivations: Map<PropertyId, [boolean, Proof<TheoremId, PropertyId>]>
+
   constructor() {
+    this.derivations = new Map()
   }
 
   add(_: {

From 58d6499646e9051896da634d288ab423cdd413e9 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:05:40 -0800
Subject: [PATCH 10/67] Begin storing added state

---
 src/Logic/Prover.ts | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index f6214f0..2249f73 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -116,12 +116,12 @@ class Derivations<TheoremId, PropertyId> {
     this.derivations = new Map()
   }
 
-  add(_: {
+  add({ property, value, proof }: {
     property: PropertyId,
     value: boolean,
     proof: Proof<TheoremId, PropertyId>
   }) {
-
+    this.derivations.set(property, [value, proof])
   }
 }
 

From a6ad118f008e908c08180a81c26b80371d9102f3 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:06:34 -0800
Subject: [PATCH 11/67] Add next target statement

We want to remove the intermediate `derivations` array, so will need to return it from our new class.
---
 src/Logic/Prover.ts | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 2249f73..9483740 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -190,6 +190,7 @@ class Prover<
       derivations.push({ property, value, proof })
     })
 
+    // return { kind: 'derivations', derivations: this.derivations.all() }
     return { kind: 'derivations', derivations }
   }
 

From dbc8e12dd3bf5992f7cecb518765cd5afa1f0cd9 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:07:36 -0800
Subject: [PATCH 12/67] Add no-op, typechecking implementation

---
 src/Logic/Prover.ts | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 9483740..99614e3 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -123,6 +123,10 @@ class Derivations<TheoremId, PropertyId> {
   }) {
     this.derivations.set(property, [value, proof])
   }
+
+  all(): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {
+    return []
+  }
 }
 
 class Prover<

From 0819c5d745e1e4bb0760398568dd2cf5b297e747 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:08:51 -0800
Subject: [PATCH 13/67] Implement `all` method

---
 src/Logic/Prover.ts | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 99614e3..061b98a 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -125,7 +125,9 @@ class Derivations<TheoremId, PropertyId> {
   }
 
   all(): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {
-    return []
+    return [...this.derivations.entries()].map(
+      ([property, [value, proof]]) => ({ property, value, proof })
+    )
   }
 }
 

From 2c2703798543e24c836909c2f983f4a43649edc5 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:09:22 -0800
Subject: [PATCH 14/67] Replace derivations list

---
 src/Logic/Prover.ts | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 061b98a..e0b20e3 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -196,8 +196,7 @@ class Prover<
       derivations.push({ property, value, proof })
     })
 
-    // return { kind: 'derivations', derivations: this.derivations.all() }
-    return { kind: 'derivations', derivations }
+    return { kind: 'derivations', derivations: this.derivations.all() }
   }
 
   proof(

From 57cca95a0d7aaf87428a1af276ab062550905c7b Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:10:25 -0800
Subject: [PATCH 15/67] Remove write to unread variable

---
 src/Logic/Prover.ts | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index e0b20e3..6a3689a 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -193,7 +193,6 @@ class Prover<
       }
 
       this.derivations.add({ property, value, proof })
-      derivations.push({ property, value, proof })
     })
 
     return { kind: 'derivations', derivations: this.derivations.all() }

From f7857b08b96465c31636cc600279c072000587a5 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:10:36 -0800
Subject: [PATCH 16/67] Remove unused variable

---
 src/Logic/Prover.ts | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 6a3689a..0b973be 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -185,7 +185,6 @@ class Prover<
     // Instead of always unconditionally expanding proofs, we want to introduce
     // an object that holds on to all of the supporting proof metadata, and can
     // expand that out to full proofs on demand.
-    const derivations: Derivation<TheoremId, PropertyId>[] = []
     this.traits.forEach((value: boolean, property: PropertyId) => {
       const proof = this.proof(property)
       if (!proof || proof === 'given') {

From 6b8f2d0aa1808965927c343059c2e6348fb0f92c Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:15:05 -0800
Subject: [PATCH 17/67] Add next target statement

We want to move towards the Derivations class managing this evidence, so will need to ensure it has a copy.
---
 src/Logic/Prover.ts | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 0b973be..f4dac8a 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -300,6 +300,7 @@ class Prover<
     }
 
     this.traits.set(property, formula.value)
+    // this.derivations.addEvidence(property, theorem, support)
     this.evidence.set(property, [theorem, support])
     this.queue.mark(property)
   }

From 90727267d168118c24758f1cb48ec85733e97bcf Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:15:56 -0800
Subject: [PATCH 18/67] Add no-op implementation

---
 src/Logic/Prover.ts | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index f4dac8a..1e68795 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -124,6 +124,10 @@ class Derivations<TheoremId, PropertyId> {
     this.derivations.set(property, [value, proof])
   }
 
+  addEvidence(property: PropertyId, theorem: TheoremId, support: PropertyId[]) {
+
+  }
+
   all(): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {
     return [...this.derivations.entries()].map(
       ([property, [value, proof]]) => ({ property, value, proof })

From 652892f88aaa86162917409a83510695942e6271 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:16:24 -0800
Subject: [PATCH 19/67] Call no-op implementation

---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 1e68795..7aab08e 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -304,7 +304,7 @@ class Prover<
     }
 
     this.traits.set(property, formula.value)
-    // this.derivations.addEvidence(property, theorem, support)
+    this.derivations.addEvidence(property, theorem, support)
     this.evidence.set(property, [theorem, support])
     this.queue.mark(property)
   }

From 03e8b639a063cfb49520cb01ad33dc720d514631 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:16:34 -0800
Subject: [PATCH 20/67] Add inner state for evidence tracking

---
 src/Logic/Prover.ts | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 7aab08e..3f8e3dd 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -111,9 +111,11 @@ export function proveTheorem<TheoremId = Id, PropertyId = Id>(
 
 class Derivations<TheoremId, PropertyId> {
   private derivations: Map<PropertyId, [boolean, Proof<TheoremId, PropertyId>]>
+  private evidence: Map<PropertyId, Evidence<TheoremId, PropertyId>>
 
   constructor() {
     this.derivations = new Map()
+    this.evidence = new Map()
   }
 
   add({ property, value, proof }: {

From dd177afea9ec545f532f92702e3721683409d8c7 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:17:06 -0800
Subject: [PATCH 21/67] Store evidence in derivations state

---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 3f8e3dd..db365d6 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -127,7 +127,7 @@ class Derivations<TheoremId, PropertyId> {
   }
 
   addEvidence(property: PropertyId, theorem: TheoremId, support: PropertyId[]) {
-
+    this.evidence.set(property, [theorem, support])
   }
 
   all(): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {

From ae38e3364fe5496764abd61314693121132f3b00 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:18:37 -0800
Subject: [PATCH 22/67] Add next target

---
 src/Logic/Prover.ts | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index db365d6..d3dcc97 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -210,6 +210,7 @@ class Prover<
       return 'given'
     }
 
+    // const evidence = this.derivations.getEvidence(property)
     const evidence = this.evidence.get(property)
     return evidence ? this.expand(evidence) : undefined
   }

From 56c40cd875c0c3fec2131b86c9820ee030a13ca7 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:19:27 -0800
Subject: [PATCH 23/67] Add no-op implementation

---
 src/Logic/Prover.ts | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index d3dcc97..887ec52 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -130,6 +130,10 @@ class Derivations<TheoremId, PropertyId> {
     this.evidence.set(property, [theorem, support])
   }
 
+  getEvidence(property: PropertyId): Evidence<TheoremId, PropertyId> | undefined {
+    return undefined
+  }
+
   all(): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {
     return [...this.derivations.entries()].map(
       ([property, [value, proof]]) => ({ property, value, proof })

From 4a0a4f6142367616db9e4deb528cf454f1dc8728 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:20:11 -0800
Subject: [PATCH 24/67] Introduce call to no-op implementation

to ensure it typechecks
---
 src/Logic/Prover.ts | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 887ec52..31780ce 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -214,8 +214,7 @@ class Prover<
       return 'given'
     }
 
-    // const evidence = this.derivations.getEvidence(property)
-    const evidence = this.evidence.get(property)
+    const evidence = this.derivations.getEvidence(property) || this.evidence.get(property)
     return evidence ? this.expand(evidence) : undefined
   }
 

From a3b7eeaf73eaf1070e18fb3a4ed7b24e02c79583 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:21:32 -0800
Subject: [PATCH 25/67] Implement `getEvidence`

---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 31780ce..665a1f8 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -131,7 +131,7 @@ class Derivations<TheoremId, PropertyId> {
   }
 
   getEvidence(property: PropertyId): Evidence<TheoremId, PropertyId> | undefined {
-    return undefined
+    return this.evidence.get(property)
   }
 
   all(): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {

From 128ca08c9f1d276784dd1f79bf85c41bb14ac47d Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:22:28 -0800
Subject: [PATCH 26/67] Remove unused call

---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 665a1f8..2d0601a 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -214,7 +214,7 @@ class Prover<
       return 'given'
     }
 
-    const evidence = this.derivations.getEvidence(property) || this.evidence.get(property)
+    const evidence = this.derivations.getEvidence(property)
     return evidence ? this.expand(evidence) : undefined
   }
 

From 9f93df6f231a1a688d5d864322d70e56e84361d5 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:22:56 -0800
Subject: [PATCH 27/67] Replace reimplemented method

This is the same call we replaced with our extracted method earlier
---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 2d0601a..a39bbab 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -264,7 +264,7 @@ class Prover<
         assumptions.add(property)
         expanded.add(property)
       } else {
-        const evidence = this.evidence.get(property)
+        const evidence = this.derivations.getEvidence(property)
         if (evidence) {
           theoremByProperty.set(property, evidence[0])
           queue = queue.concat(evidence[1])

From 58a1ab3449ef7cacb13ff543ddd39ed56efd8e87 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:23:29 -0800
Subject: [PATCH 28/67] Stop setting `evidence` directly

All reads now factor through `this.derivations` instead.
---
 src/Logic/Prover.ts | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index a39bbab..1d139ec 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -311,7 +311,6 @@ class Prover<
 
     this.traits.set(property, formula.value)
     this.derivations.addEvidence(property, theorem, support)
-    this.evidence.set(property, [theorem, support])
     this.queue.mark(property)
   }
 

From 7ad1cbb33b0633cce7b2cce6c5a38c7a548f6c94 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:24:00 -0800
Subject: [PATCH 29/67] Remove unused variable

---
 src/Logic/Prover.ts | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 1d139ec..a2a690b 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -153,7 +153,6 @@ class Prover<
   private derivations: Derivations<TheoremId, PropertyId>
 
   private given: Set<PropertyId>
-  private evidence: Map<PropertyId, Evidence<TheoremId, PropertyId>>
   private queue: Queue<TheoremId, PropertyId, Theorem>
 
   constructor(
@@ -163,7 +162,6 @@ class Prover<
     this.traits = traits
     this.derivations = new Derivations()
     this.given = new Set([...traits.keys()])
-    this.evidence = new Map()
     this.queue = new Queue(implications)
 
     traits.forEach((_: boolean, id: PropertyId) => {

From 057067644efc082fad0c1837269aa7a150eb3175 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:25:50 -0800
Subject: [PATCH 30/67] Describe next goal

---
 src/Logic/Prover.ts | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index a2a690b..68da422 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -243,6 +243,8 @@ class Prover<
     return this.expand([theorem, properties])
   }
 
+  // This seems to be a concern of the Derivations class, and we'd really like
+  // to move it. We can't quite though, because of
   private expand([theorem, properties]: Evidence<TheoremId, PropertyId>): Proof<
     TheoremId,
     PropertyId
@@ -258,7 +260,7 @@ class Prover<
         continue
       }
 
-      if (this.given.has(property)) {
+      if (this.given.has(property)) { // <-- this reference to other state
         assumptions.add(property)
         expanded.add(property)
       } else {

From 37014259f41da480631a54801a53260937a8cf18 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:26:14 -0800
Subject: [PATCH 31/67] Begin tracking `given` property ids in `Derivations`

since we'll need these to move the `expand` method
---
 src/Logic/Prover.ts | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 68da422..b73b8c4 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -112,10 +112,12 @@ export function proveTheorem<TheoremId = Id, PropertyId = Id>(
 class Derivations<TheoremId, PropertyId> {
   private derivations: Map<PropertyId, [boolean, Proof<TheoremId, PropertyId>]>
   private evidence: Map<PropertyId, Evidence<TheoremId, PropertyId>>
+  private given: Set<PropertyId>
 
   constructor() {
     this.derivations = new Map()
     this.evidence = new Map()
+    this.given = new Set()
   }
 
   add({ property, value, proof }: {

From 84e709da6e0487126e32a29894467474278cee87 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:28:33 -0800
Subject: [PATCH 32/67] Introduce optional constructor argument

---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index b73b8c4..f0c1403 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -114,7 +114,7 @@ class Derivations<TheoremId, PropertyId> {
   private evidence: Map<PropertyId, Evidence<TheoremId, PropertyId>>
   private given: Set<PropertyId>
 
-  constructor() {
+  constructor(assumptions: PropertyId[] = []) {
     this.derivations = new Map()
     this.evidence = new Map()
     this.given = new Set()

From 70b91458384ba6761639b7ca352ccbcf27c34fad Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:28:54 -0800
Subject: [PATCH 33/67] Store given assumptions

---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index f0c1403..f23c620 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -117,7 +117,7 @@ class Derivations<TheoremId, PropertyId> {
   constructor(assumptions: PropertyId[] = []) {
     this.derivations = new Map()
     this.evidence = new Map()
-    this.given = new Set()
+    this.given = new Set(assumptions)
   }
 
   add({ property, value, proof }: {

From 5dff416cbf0e541f697696a5bd01058c13599643 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:29:24 -0800
Subject: [PATCH 34/67] Pass initially assumed trait ids to Derivations

---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index f23c620..fc05986 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -162,7 +162,7 @@ class Prover<
     traits: Map<PropertyId, boolean> = new Map()
   ) {
     this.traits = traits
-    this.derivations = new Derivations()
+    this.derivations = new Derivations([...traits.keys()])
     this.given = new Set([...traits.keys()])
     this.queue = new Queue(implications)
 

From 6facfd3a64fbe5f2c7c30f976f81c9088cfb1500 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:29:51 -0800
Subject: [PATCH 35/67] Remove unused default argument

---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index fc05986..2b29d41 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -114,7 +114,7 @@ class Derivations<TheoremId, PropertyId> {
   private evidence: Map<PropertyId, Evidence<TheoremId, PropertyId>>
   private given: Set<PropertyId>
 
-  constructor(assumptions: PropertyId[] = []) {
+  constructor(assumptions: PropertyId[]) {
     this.derivations = new Map()
     this.evidence = new Map()
     this.given = new Set(assumptions)

From af7bb825aa9132d8cb083a0cbbb7bfb05befc496 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:30:49 -0800
Subject: [PATCH 36/67] Copy `expand` method to `Derivations`

This looks like a large change, but is an exact copy-paste except that `this.derivation.getEvidence` is now `this.getEvidence`. We aren't currently calling this method, but the fact that it type-checks gives us some good confidence.
---
 src/Logic/Prover.ts | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 2b29d41..38e04d3 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -141,6 +141,40 @@ class Derivations<TheoremId, PropertyId> {
       ([property, [value, proof]]) => ({ property, value, proof })
     )
   }
+
+  expand([theorem, properties]: Evidence<TheoremId, PropertyId>): Proof<
+    TheoremId,
+    PropertyId
+  > {
+    const theoremByProperty = new Map<PropertyId, TheoremId>()
+    const assumptions = new Set<PropertyId>()
+    const expanded = new Set<PropertyId>()
+
+    let queue = [...properties]
+    let property
+    while ((property = queue.shift())) {
+      if (expanded.has(property)) {
+        continue
+      }
+
+      if (this.given.has(property)) {
+        assumptions.add(property)
+        expanded.add(property)
+      } else {
+        const evidence = this.getEvidence(property)
+        if (evidence) {
+          theoremByProperty.set(property, evidence[0])
+          queue = queue.concat(evidence[1])
+          expanded.add(property)
+        }
+      }
+    }
+
+    return {
+      theorems: [theorem, ...theoremByProperty.values()],
+      properties: [...assumptions],
+    }
+  }
 }
 
 class Prover<

From 32410c0aa55b976c1393059892b2586595045d58 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:32:47 -0800
Subject: [PATCH 37/67] Delegate `expand` call to `Derivations`

Since it is an exact copy-paste, and since the tests pass, this gives us good confidence.
---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 38e04d3..eca59e2 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -249,7 +249,7 @@ class Prover<
     }
 
     const evidence = this.derivations.getEvidence(property)
-    return evidence ? this.expand(evidence) : undefined
+    return evidence ? this.derivations.expand(evidence) : undefined
   }
 
   private apply(

From f650304915164f9ab09015c312fb9d8923059a19 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:33:30 -0800
Subject: [PATCH 38/67] Delegate another call to `expand`

---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index eca59e2..8584645 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -276,7 +276,7 @@ class Prover<
     theorem: TheoremId,
     properties: PropertyId[]
   ): Contradiction<TheoremId, PropertyId> {
-    return this.expand([theorem, properties])
+    return this.derivations.expand([theorem, properties])
   }
 
   // This seems to be a concern of the Derivations class, and we'd really like

From 22bafea1a37c25388eb9e214cf380eb1655535d8 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:33:53 -0800
Subject: [PATCH 39/67] Remove unused method

We've basically ended up moving this to the `Derivations` class
---
 src/Logic/Prover.ts | 36 ------------------------------------
 1 file changed, 36 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 8584645..d596c61 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -279,42 +279,6 @@ class Prover<
     return this.derivations.expand([theorem, properties])
   }
 
-  // This seems to be a concern of the Derivations class, and we'd really like
-  // to move it. We can't quite though, because of
-  private expand([theorem, properties]: Evidence<TheoremId, PropertyId>): Proof<
-    TheoremId,
-    PropertyId
-  > {
-    const theoremByProperty = new Map<PropertyId, TheoremId>()
-    const assumptions = new Set<PropertyId>()
-    const expanded = new Set<PropertyId>()
-
-    let queue = [...properties]
-    let property
-    while ((property = queue.shift())) {
-      if (expanded.has(property)) {
-        continue
-      }
-
-      if (this.given.has(property)) { // <-- this reference to other state
-        assumptions.add(property)
-        expanded.add(property)
-      } else {
-        const evidence = this.derivations.getEvidence(property)
-        if (evidence) {
-          theoremByProperty.set(property, evidence[0])
-          queue = queue.concat(evidence[1])
-          expanded.add(property)
-        }
-      }
-    }
-
-    return {
-      theorems: [theorem, ...theoremByProperty.values()],
-      properties: [...assumptions],
-    }
-  }
-
   force(
     theorem: TheoremId,
     formula: Formula<PropertyId>,

From aa7a6bed632aa719846700777b01dcf27f1ddb7a Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:35:27 -0800
Subject: [PATCH 40/67] Copy `proof` method to `Derivations`

Similarly, this is an exact copy-paste, except for `this.derivations.` becoming `this.`.
---
 src/Logic/Prover.ts | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index d596c61..0190d3f 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -175,6 +175,17 @@ class Derivations<TheoremId, PropertyId> {
       properties: [...assumptions],
     }
   }
+
+  proof(
+    property: PropertyId
+  ): Proof<TheoremId, PropertyId> | 'given' | undefined {
+    if (this.given.has(property)) {
+      return 'given'
+    }
+
+    const evidence = this.getEvidence(property)
+    return evidence ? this.expand(evidence) : undefined
+  }
 }
 
 class Prover<

From ae59931697fda899d05a14fcbe786376d2b75126 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:37:11 -0800
Subject: [PATCH 41/67] Delegate `proof` to `Derivations`

---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 0190d3f..66814fb 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -241,7 +241,7 @@ class Prover<
     // an object that holds on to all of the supporting proof metadata, and can
     // expand that out to full proofs on demand.
     this.traits.forEach((value: boolean, property: PropertyId) => {
-      const proof = this.proof(property)
+      const proof = this.derivations.proof(property)
       if (!proof || proof === 'given') {
         return
       }

From 9c9c0bb4028c27cf112e451e02905618d5d23a0e Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:37:28 -0800
Subject: [PATCH 42/67] Remove unused method

---
 src/Logic/Prover.ts | 11 -----------
 1 file changed, 11 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 66814fb..eeed14c 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -252,17 +252,6 @@ class Prover<
     return { kind: 'derivations', derivations: this.derivations.all() }
   }
 
-  proof(
-    property: PropertyId
-  ): Proof<TheoremId, PropertyId> | 'given' | undefined {
-    if (this.given.has(property)) {
-      return 'given'
-    }
-
-    const evidence = this.derivations.getEvidence(property)
-    return evidence ? this.derivations.expand(evidence) : undefined
-  }
-
   private apply(
     implication: Theorem
   ): Contradiction<TheoremId, PropertyId> | undefined {

From 863127e4a29b67bc6db4cc536bf6c34c63319d34 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:38:16 -0800
Subject: [PATCH 43/67] Privatize `getEvidence` method

Calls to this are now entirely contained in the `Derivations` class, so we can begin encapsulating them better.
---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index eeed14c..d801aab 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -132,7 +132,7 @@ class Derivations<TheoremId, PropertyId> {
     this.evidence.set(property, [theorem, support])
   }
 
-  getEvidence(property: PropertyId): Evidence<TheoremId, PropertyId> | undefined {
+  private getEvidence(property: PropertyId): Evidence<TheoremId, PropertyId> | undefined {
     return this.evidence.get(property)
   }
 

From 84553322421084a38edb7e7b6effe4a9420c63dd Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:45:12 -0800
Subject: [PATCH 44/67] Add comment on next goal

---
 src/Logic/Prover.ts | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index d801aab..e3c1a01 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -137,6 +137,20 @@ class Derivations<TheoremId, PropertyId> {
   }
 
   all(): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {
+    // We should now have enough information stored that we can populate this
+    // list directly from `evidence` rather than relying on something external
+    // populating `derivations`.
+    //
+    // Our next goal is to adapt this existing logic from `Prover#run`:
+    //
+    //   this.traits.forEach((value: boolean, property: PropertyId) => {
+    //     const proof = this.derivations.proof(property)
+    //     if (!proof || proof === 'given') {
+    //       return
+    //     }
+
+    //     this.derivations.add({ property, value, proof })
+    //   })
     return [...this.derivations.entries()].map(
       ([property, [value, proof]]) => ({ property, value, proof })
     )

From 5d5d6100d94d6e2f0470b2ade007014a31cd0e64 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:53:20 -0800
Subject: [PATCH 45/67] Add unused default argument

---
 src/Logic/Prover.ts | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index e3c1a01..85a379b 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -136,7 +136,9 @@ class Derivations<TheoremId, PropertyId> {
     return this.evidence.get(property)
   }
 
-  all(): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {
+  all(
+    traits: Map<PropertyId, boolean> = new Map()
+  ): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {
     // We should now have enough information stored that we can populate this
     // list directly from `evidence` rather than relying on something external
     // populating `derivations`.

From 15b5dd66bc6d2546e934ad1804f2d58faf6c8abc Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:54:04 -0800
Subject: [PATCH 46/67] Add unused accumulator value

that we will eventually return
---
 src/Logic/Prover.ts | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 85a379b..d29a707 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -153,6 +153,8 @@ class Derivations<TheoremId, PropertyId> {
 
     //     this.derivations.add({ property, value, proof })
     //   })
+    const result: { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] = []
+
     return [...this.derivations.entries()].map(
       ([property, [value, proof]]) => ({ property, value, proof })
     )

From 6d5c5939e39ab354bcd1bb7899b8ae4b66434d96 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:55:04 -0800
Subject: [PATCH 47/67] Copy existing iteration block

again with the natural tweaks for changing context
---
 src/Logic/Prover.ts | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index d29a707..cf395d2 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -154,6 +154,14 @@ class Derivations<TheoremId, PropertyId> {
     //     this.derivations.add({ property, value, proof })
     //   })
     const result: { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] = []
+    traits.forEach((value: boolean, property: PropertyId) => {
+      const proof = this.proof(property)
+      if (!proof || proof === 'given') {
+        return
+      }
+
+      result.push({ property, value, proof })
+    })
 
     return [...this.derivations.entries()].map(
       ([property, [value, proof]]) => ({ property, value, proof })

From 7a13a6359da1786973926248a3d663bb7c2881a5 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:56:20 -0800
Subject: [PATCH 48/67] Supply optional `traits` argument

---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index cf395d2..d98ffd8 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -275,7 +275,7 @@ class Prover<
       this.derivations.add({ property, value, proof })
     })
 
-    return { kind: 'derivations', derivations: this.derivations.all() }
+    return { kind: 'derivations', derivations: this.derivations.all(this.traits) }
   }
 
   private apply(

From 89f9546adb3da6a1c7c4ea2008d6c9329f420fa5 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:56:50 -0800
Subject: [PATCH 49/67] Use updated `all` implementation

---
 src/Logic/Prover.ts | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index d98ffd8..f2a5753 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -163,9 +163,7 @@ class Derivations<TheoremId, PropertyId> {
       result.push({ property, value, proof })
     })
 
-    return [...this.derivations.entries()].map(
-      ([property, [value, proof]]) => ({ property, value, proof })
-    )
+    return result
   }
 
   expand([theorem, properties]: Evidence<TheoremId, PropertyId>): Proof<

From 44d18d65db6a9130cb327c2d12e110702eba32d3 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 15:01:49 -0800
Subject: [PATCH 50/67] Remove comment

---
 src/Logic/Prover.ts | 14 --------------
 1 file changed, 14 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index f2a5753..6e9035d 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -139,20 +139,6 @@ class Derivations<TheoremId, PropertyId> {
   all(
     traits: Map<PropertyId, boolean> = new Map()
   ): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {
-    // We should now have enough information stored that we can populate this
-    // list directly from `evidence` rather than relying on something external
-    // populating `derivations`.
-    //
-    // Our next goal is to adapt this existing logic from `Prover#run`:
-    //
-    //   this.traits.forEach((value: boolean, property: PropertyId) => {
-    //     const proof = this.derivations.proof(property)
-    //     if (!proof || proof === 'given') {
-    //       return
-    //     }
-
-    //     this.derivations.add({ property, value, proof })
-    //   })
     const result: { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] = []
     traits.forEach((value: boolean, property: PropertyId) => {
       const proof = this.proof(property)

From 2c9dc1f72bc605127d45b2d0eb296e63dad24f61 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:58:06 -0800
Subject: [PATCH 51/67] Remove unused block

---
 src/Logic/Prover.ts | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 6e9035d..38c2f09 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -250,15 +250,6 @@ class Prover<
     // Instead of always unconditionally expanding proofs, we want to introduce
     // an object that holds on to all of the supporting proof metadata, and can
     // expand that out to full proofs on demand.
-    this.traits.forEach((value: boolean, property: PropertyId) => {
-      const proof = this.derivations.proof(property)
-      if (!proof || proof === 'given') {
-        return
-      }
-
-      this.derivations.add({ property, value, proof })
-    })
-
     return { kind: 'derivations', derivations: this.derivations.all(this.traits) }
   }
 

From 50fe5122bc71bc1921b392fee6ae1d0bb0ac1eff Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 14:59:41 -0800
Subject: [PATCH 52/67] Remove unused method

---
 src/Logic/Prover.ts | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 38c2f09..ebae288 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -120,14 +120,6 @@ class Derivations<TheoremId, PropertyId> {
     this.given = new Set(assumptions)
   }
 
-  add({ property, value, proof }: {
-    property: PropertyId,
-    value: boolean,
-    proof: Proof<TheoremId, PropertyId>
-  }) {
-    this.derivations.set(property, [value, proof])
-  }
-
   addEvidence(property: PropertyId, theorem: TheoremId, support: PropertyId[]) {
     this.evidence.set(property, [theorem, support])
   }

From 9b638c6a816a7b7f6b793352a818544b210881ab Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 15:00:32 -0800
Subject: [PATCH 53/67] Remove unused field

---
 src/Logic/Prover.ts | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index ebae288..64bc9f3 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -201,7 +201,6 @@ class Prover<
   private traits: Map<PropertyId, boolean>
   private derivations: Derivations<TheoremId, PropertyId>
 
-  private given: Set<PropertyId>
   private queue: Queue<TheoremId, PropertyId, Theorem>
 
   constructor(
@@ -210,7 +209,6 @@ class Prover<
   ) {
     this.traits = traits
     this.derivations = new Derivations([...traits.keys()])
-    this.given = new Set([...traits.keys()])
     this.queue = new Queue(implications)
 
     traits.forEach((_: boolean, id: PropertyId) => {

From 05d583b7a7d7804e2edfea4e8109c5650ce3c6de Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 15:02:38 -0800
Subject: [PATCH 54/67] Remove unused field

---
 src/Logic/Prover.ts | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 64bc9f3..fcacd90 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -110,12 +110,10 @@ export function proveTheorem<TheoremId = Id, PropertyId = Id>(
 }
 
 class Derivations<TheoremId, PropertyId> {
-  private derivations: Map<PropertyId, [boolean, Proof<TheoremId, PropertyId>]>
   private evidence: Map<PropertyId, Evidence<TheoremId, PropertyId>>
   private given: Set<PropertyId>
 
   constructor(assumptions: PropertyId[]) {
-    this.derivations = new Map()
     this.evidence = new Map()
     this.given = new Set(assumptions)
   }

From b1c160066be87c0254adfef166acceab2e6ebf18 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 18:10:48 -0800
Subject: [PATCH 55/67] Add comment on next goal

---
 src/Logic/Prover.ts | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index fcacd90..faec1ab 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -238,6 +238,11 @@ class Prover<
     // Instead of always unconditionally expanding proofs, we want to introduce
     // an object that holds on to all of the supporting proof metadata, and can
     // expand that out to full proofs on demand.
+    //
+    // We want to eventually make the breaking API change
+    //   return { kind: 'derivations', derivations: this.derviations }
+    // The last blocker to doing that is the fact that `derivations` doesn't
+    // encapsulate the `traits` that we're currently passing in.
     return { kind: 'derivations', derivations: this.derivations.all(this.traits) }
   }
 

From 7c1c693ee9b41450571608cf02d33e0aa8d8ee99 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 18:12:17 -0800
Subject: [PATCH 56/67] Pass `value` to `Derivations`

---
 src/Logic/Prover.ts | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index faec1ab..9fa9937 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -118,7 +118,7 @@ class Derivations<TheoremId, PropertyId> {
     this.given = new Set(assumptions)
   }
 
-  addEvidence(property: PropertyId, theorem: TheoremId, support: PropertyId[]) {
+  addEvidence(property: PropertyId, value: boolean, theorem: TheoremId, support: PropertyId[]) {
     this.evidence.set(property, [theorem, support])
   }
 
@@ -304,7 +304,7 @@ class Prover<
     }
 
     this.traits.set(property, formula.value)
-    this.derivations.addEvidence(property, theorem, support)
+    this.derivations.addEvidence(property, formula.value, theorem, support)
     this.queue.mark(property)
   }
 

From 2848ef0d7e78d21ffb8467265db23b723f6f7941 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 18:15:39 -0800
Subject: [PATCH 57/67] Add `traits` field

---
 src/Logic/Prover.ts | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 9fa9937..77a5e99 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -112,10 +112,12 @@ export function proveTheorem<TheoremId = Id, PropertyId = Id>(
 class Derivations<TheoremId, PropertyId> {
   private evidence: Map<PropertyId, Evidence<TheoremId, PropertyId>>
   private given: Set<PropertyId>
+  private traits: Map<PropertyId, boolean>
 
   constructor(assumptions: PropertyId[]) {
     this.evidence = new Map()
     this.given = new Set(assumptions)
+    this.traits = new Map()
   }
 
   addEvidence(property: PropertyId, value: boolean, theorem: TheoremId, support: PropertyId[]) {

From a05ebb0a9d72cde8118daa66470313d44b2ce39b Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 18:16:13 -0800
Subject: [PATCH 58/67] Record trait value

---
 src/Logic/Prover.ts | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 77a5e99..38c04e7 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -122,6 +122,7 @@ class Derivations<TheoremId, PropertyId> {
 
   addEvidence(property: PropertyId, value: boolean, theorem: TheoremId, support: PropertyId[]) {
     this.evidence.set(property, [theorem, support])
+    this.traits.set(property, value)
   }
 
   private getEvidence(property: PropertyId): Evidence<TheoremId, PropertyId> | undefined {

From 703331a0d3556fa6ce162798cc1489fc88c85427 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 18:17:11 -0800
Subject: [PATCH 59/67] Use internally tracked `traits`

---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 38c04e7..68eedf3 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -133,7 +133,7 @@ class Derivations<TheoremId, PropertyId> {
     traits: Map<PropertyId, boolean> = new Map()
   ): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {
     const result: { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] = []
-    traits.forEach((value: boolean, property: PropertyId) => {
+    this.traits.forEach((value: boolean, property: PropertyId) => {
       const proof = this.proof(property)
       if (!proof || proof === 'given') {
         return

From ac6c6276a68aa31dc8e75099d9638c39ea4aa3f4 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 18:17:27 -0800
Subject: [PATCH 60/67] Don't pass unused `traits`

---
 src/Logic/Prover.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 68eedf3..8dc71c3 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -246,7 +246,7 @@ class Prover<
     //   return { kind: 'derivations', derivations: this.derviations }
     // The last blocker to doing that is the fact that `derivations` doesn't
     // encapsulate the `traits` that we're currently passing in.
-    return { kind: 'derivations', derivations: this.derivations.all(this.traits) }
+    return { kind: 'derivations', derivations: this.derivations.all() }
   }
 
   private apply(

From c7cd2364d047e9a5322645e8f2c855bd80deb9d3 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 18:17:45 -0800
Subject: [PATCH 61/67] Remove unused argument

---
 src/Logic/Prover.ts | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 8dc71c3..29dd28c 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -129,9 +129,7 @@ class Derivations<TheoremId, PropertyId> {
     return this.evidence.get(property)
   }
 
-  all(
-    traits: Map<PropertyId, boolean> = new Map()
-  ): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {
+  all(): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {
     const result: { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] = []
     this.traits.forEach((value: boolean, property: PropertyId) => {
       const proof = this.proof(property)

From 3cb482ac7149ee99b565897d0fee128b5f4c4cf1 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 18:21:03 -0800
Subject: [PATCH 62/67] Make the breaking API change

---
 src/Logic/Prover.test.ts | 2 +-
 src/Logic/Prover.ts      | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Logic/Prover.test.ts b/src/Logic/Prover.test.ts
index aff8d71..89f6417 100644
--- a/src/Logic/Prover.test.ts
+++ b/src/Logic/Prover.test.ts
@@ -20,7 +20,7 @@ describe('deduceTraits', () => {
     if (result.kind === 'contradiction') {
       contradiction = result.contradiction
     } else {
-      deductions = result.derivations
+      deductions = result.derivations.all()
     }
   }
 
diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 29dd28c..0a7582e 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -32,7 +32,7 @@ type Result<TheoremId = Id, PropertyId = Id> =
     kind: 'contradiction'
     contradiction: Contradiction<TheoremId, PropertyId>
   }
-  | { kind: 'derivations'; derivations: Derivation<TheoremId, PropertyId>[] }
+  | { kind: 'derivations'; derivations: Derivations<TheoremId, PropertyId> }
 
 // Given a collection of implications and a collection of traits for an object,
 // find either the collection of derivable traits, or a contradiction
@@ -244,7 +244,7 @@ class Prover<
     //   return { kind: 'derivations', derivations: this.derviations }
     // The last blocker to doing that is the fact that `derivations` doesn't
     // encapsulate the `traits` that we're currently passing in.
-    return { kind: 'derivations', derivations: this.derivations.all() }
+    return { kind: 'derivations', derivations: this.derivations }
   }
 
   private apply(

From b0a1f3fece4ab9bff09259663769faf4cca83035 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 18:21:45 -0800
Subject: [PATCH 63/67] Remove completed comment

---
 src/Logic/Prover.ts | 20 --------------------
 1 file changed, 20 deletions(-)

diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 0a7582e..12cd24d 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -224,26 +224,6 @@ class Prover<
       }
     }
 
-    // Problem: we have recorded proofs of the form
-    //
-    //   Property P holds by theorem T and supporting properties [P1, P2, ...]
-    //
-    // where the supporting properties _may_ also be properties we've dervied,
-    // which have their own proofs. We're currently expanding those out to
-    // proofs "from first principles" of the form
-    //
-    //   ... by theorems [T1, T2, ...] and supporting properties [P1, P2, ...]
-    //
-    // where each supporting property is in our list of initial assumptions.
-    //
-    // Instead of always unconditionally expanding proofs, we want to introduce
-    // an object that holds on to all of the supporting proof metadata, and can
-    // expand that out to full proofs on demand.
-    //
-    // We want to eventually make the breaking API change
-    //   return { kind: 'derivations', derivations: this.derviations }
-    // The last blocker to doing that is the fact that `derivations` doesn't
-    // encapsulate the `traits` that we're currently passing in.
     return { kind: 'derivations', derivations: this.derivations }
   }
 

From 0564933b9454a004f8bff736404baa6a8c535532 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 18:25:13 -0800
Subject: [PATCH 64/67] Move `Derivations` class to its own file

---
 src/Logic/Derivations.ts | 88 ++++++++++++++++++++++++++++++++++++++++
 src/Logic/Prover.ts      | 86 +--------------------------------------
 2 files changed, 89 insertions(+), 85 deletions(-)
 create mode 100644 src/Logic/Derivations.ts

diff --git a/src/Logic/Derivations.ts b/src/Logic/Derivations.ts
new file mode 100644
index 0000000..86b4fc4
--- /dev/null
+++ b/src/Logic/Derivations.ts
@@ -0,0 +1,88 @@
+import { Id } from './Types'
+
+type Evidence<TheoremId = Id, PropertyId = Id> = [TheoremId, PropertyId[]]
+
+export type Proof<TheoremId = Id, PropertyId = Id> = {
+  theorems: TheoremId[]
+  properties: PropertyId[]
+}
+
+export class Derivations<TheoremId, PropertyId> {
+  private evidence: Map<PropertyId, Evidence<TheoremId, PropertyId>>
+  private given: Set<PropertyId>
+  private traits: Map<PropertyId, boolean>
+
+  constructor(assumptions: PropertyId[]) {
+    this.evidence = new Map()
+    this.given = new Set(assumptions)
+    this.traits = new Map()
+  }
+
+  addEvidence(property: PropertyId, value: boolean, theorem: TheoremId, support: PropertyId[]) {
+    this.evidence.set(property, [theorem, support])
+    this.traits.set(property, value)
+  }
+
+  private getEvidence(property: PropertyId): Evidence<TheoremId, PropertyId> | undefined {
+    return this.evidence.get(property)
+  }
+
+  all(): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {
+    const result: { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] = []
+    this.traits.forEach((value: boolean, property: PropertyId) => {
+      const proof = this.proof(property)
+      if (!proof || proof === 'given') {
+        return
+      }
+
+      result.push({ property, value, proof })
+    })
+
+    return result
+  }
+
+  expand([theorem, properties]: Evidence<TheoremId, PropertyId>): Proof<
+    TheoremId,
+    PropertyId
+  > {
+    const theoremByProperty = new Map<PropertyId, TheoremId>()
+    const assumptions = new Set<PropertyId>()
+    const expanded = new Set<PropertyId>()
+
+    let queue = [...properties]
+    let property
+    while ((property = queue.shift())) {
+      if (expanded.has(property)) {
+        continue
+      }
+
+      if (this.given.has(property)) {
+        assumptions.add(property)
+        expanded.add(property)
+      } else {
+        const evidence = this.getEvidence(property)
+        if (evidence) {
+          theoremByProperty.set(property, evidence[0])
+          queue = queue.concat(evidence[1])
+          expanded.add(property)
+        }
+      }
+    }
+
+    return {
+      theorems: [theorem, ...theoremByProperty.values()],
+      properties: [...assumptions],
+    }
+  }
+
+  proof(
+    property: PropertyId
+  ): Proof<TheoremId, PropertyId> | 'given' | undefined {
+    if (this.given.has(property)) {
+      return 'given'
+    }
+
+    const evidence = this.getEvidence(property)
+    return evidence ? this.expand(evidence) : undefined
+  }
+}
\ No newline at end of file
diff --git a/src/Logic/Prover.ts b/src/Logic/Prover.ts
index 12cd24d..12a90f7 100644
--- a/src/Logic/Prover.ts
+++ b/src/Logic/Prover.ts
@@ -10,14 +10,10 @@ import {
 import ImplicationIndex from './ImplicationIndex'
 import Queue from './Queue'
 import { Id, Implication } from './Types'
+import { Derivations, Proof } from './Derivations'
 
 // TODO: is it deduction, or derivation
 
-type Evidence<TheoremId = Id, PropertyId = Id> = [TheoremId, PropertyId[]]
-type Proof<TheoremId = Id, PropertyId = Id> = {
-  theorems: TheoremId[]
-  properties: PropertyId[]
-}
 export type Contradiction<TheoremId = Id, PropertyId = Id> = Proof<
   TheoremId,
   PropertyId
@@ -109,86 +105,6 @@ export function proveTheorem<TheoremId = Id, PropertyId = Id>(
   }
 }
 
-class Derivations<TheoremId, PropertyId> {
-  private evidence: Map<PropertyId, Evidence<TheoremId, PropertyId>>
-  private given: Set<PropertyId>
-  private traits: Map<PropertyId, boolean>
-
-  constructor(assumptions: PropertyId[]) {
-    this.evidence = new Map()
-    this.given = new Set(assumptions)
-    this.traits = new Map()
-  }
-
-  addEvidence(property: PropertyId, value: boolean, theorem: TheoremId, support: PropertyId[]) {
-    this.evidence.set(property, [theorem, support])
-    this.traits.set(property, value)
-  }
-
-  private getEvidence(property: PropertyId): Evidence<TheoremId, PropertyId> | undefined {
-    return this.evidence.get(property)
-  }
-
-  all(): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {
-    const result: { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] = []
-    this.traits.forEach((value: boolean, property: PropertyId) => {
-      const proof = this.proof(property)
-      if (!proof || proof === 'given') {
-        return
-      }
-
-      result.push({ property, value, proof })
-    })
-
-    return result
-  }
-
-  expand([theorem, properties]: Evidence<TheoremId, PropertyId>): Proof<
-    TheoremId,
-    PropertyId
-  > {
-    const theoremByProperty = new Map<PropertyId, TheoremId>()
-    const assumptions = new Set<PropertyId>()
-    const expanded = new Set<PropertyId>()
-
-    let queue = [...properties]
-    let property
-    while ((property = queue.shift())) {
-      if (expanded.has(property)) {
-        continue
-      }
-
-      if (this.given.has(property)) {
-        assumptions.add(property)
-        expanded.add(property)
-      } else {
-        const evidence = this.getEvidence(property)
-        if (evidence) {
-          theoremByProperty.set(property, evidence[0])
-          queue = queue.concat(evidence[1])
-          expanded.add(property)
-        }
-      }
-    }
-
-    return {
-      theorems: [theorem, ...theoremByProperty.values()],
-      properties: [...assumptions],
-    }
-  }
-
-  proof(
-    property: PropertyId
-  ): Proof<TheoremId, PropertyId> | 'given' | undefined {
-    if (this.given.has(property)) {
-      return 'given'
-    }
-
-    const evidence = this.getEvidence(property)
-    return evidence ? this.expand(evidence) : undefined
-  }
-}
-
 class Prover<
   TheoremId = Id,
   PropertyId = Id,

From 382e5e06aeb87c70d007c366b1785f185afa27c7 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 18:26:52 -0800
Subject: [PATCH 65/67] Inline method

---
 src/Logic/Derivations.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Derivations.ts b/src/Logic/Derivations.ts
index 86b4fc4..068ca8f 100644
--- a/src/Logic/Derivations.ts
+++ b/src/Logic/Derivations.ts
@@ -60,7 +60,7 @@ export class Derivations<TheoremId, PropertyId> {
         assumptions.add(property)
         expanded.add(property)
       } else {
-        const evidence = this.getEvidence(property)
+        const evidence = this.evidence.get(property)
         if (evidence) {
           theoremByProperty.set(property, evidence[0])
           queue = queue.concat(evidence[1])

From c2ac8cff714d02a9b06150f101edf61bbadc4cc4 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 18:27:05 -0800
Subject: [PATCH 66/67] Inline method

---
 src/Logic/Derivations.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Logic/Derivations.ts b/src/Logic/Derivations.ts
index 068ca8f..7404959 100644
--- a/src/Logic/Derivations.ts
+++ b/src/Logic/Derivations.ts
@@ -82,7 +82,7 @@ export class Derivations<TheoremId, PropertyId> {
       return 'given'
     }
 
-    const evidence = this.getEvidence(property)
+    const evidence = this.evidence.get(property)
     return evidence ? this.expand(evidence) : undefined
   }
 }
\ No newline at end of file

From 34576cd1fe3d28cb347deadaa18956817b8c9fb4 Mon Sep 17 00:00:00 2001
From: James Dabbs <jamesdabbs@gmail.com>
Date: Sun, 29 Nov 2020 18:27:16 -0800
Subject: [PATCH 67/67] Remove unused method

---
 src/Logic/Derivations.ts | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/src/Logic/Derivations.ts b/src/Logic/Derivations.ts
index 7404959..0d27fe1 100644
--- a/src/Logic/Derivations.ts
+++ b/src/Logic/Derivations.ts
@@ -23,10 +23,6 @@ export class Derivations<TheoremId, PropertyId> {
     this.traits.set(property, value)
   }
 
-  private getEvidence(property: PropertyId): Evidence<TheoremId, PropertyId> | undefined {
-    return this.evidence.get(property)
-  }
-
   all(): { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] {
     const result: { property: PropertyId, value: boolean, proof: Proof<TheoremId, PropertyId> }[] = []
     this.traits.forEach((value: boolean, property: PropertyId) => {