mark beta origins of pruned branches as unused

In the S5 proof for (□p↔◇q)→◇(p↔q) this caused a redundant node 21 (in step 31).
wo · Oct 13, 2019 · a9a2a62 · a9a2a62
1 parent ba6d9fa
commit a9a2a62
Showing 1 changed file with 7 additions and 2 deletions.
diff --git a/prover.js b/prover.js
@@ -626,8 +626,13 @@ Tree.prototype.pruneBranch = function(branch, complementary1, complementary2) {
                 }
                 else {
                     log("pruning branch "+obranches[j]+": unused expansion of "+branch.nodes[i].fromNodes[0]);
-                    if (obranches[j].closed) this.closedBranches.remove(obranches[j]);
-                    else this.openBranches.remove(obranches[j]);
+                    if (obranches[j].closed) {
+                        this.closedBranches.remove(obranches[j]);
+                        branch.nodes[i].fromNodes[0].used = false;
+                    }
+                    else {
+                        this.openBranches.remove(obranches[j]);
+                    }
                     // We don't remove the beta expansion result on this branch;
                     // it'll be removed in the displayed sentence tree because
                     // it has .used == false