From f9ad769d9f0137aa79f1bf3ebc34f35d21814124 Mon Sep 17 00:00:00 2001
From: Branden J Brown <zephyrtronium@gmail.com>
Date: Mon, 19 Jan 2026 17:21:51 -0500
Subject: [PATCH] horse/prob: kfl addition

---
 horse/prob/kfl.kk | 49 +++++++++++++++++++++++++++++++++++------------
 1 file changed, 37 insertions(+), 12 deletions(-)

diff --git a/horse/prob/kfl.kk b/horse/prob/kfl.kk
index f62e662..90fad49 100644
--- a/horse/prob/kfl.kk
+++ b/horse/prob/kfl.kk
@@ -71,31 +71,56 @@ pub fun kfl/(*)(a: kfl, b: kfl): e kfl
     Gt -> (b, a)
     _ -> (a, b)
   match (l, h)
+    (r, Guaranteed) -> r // factor out Guaranteed cases
     (Impossible, _) -> Impossible
-    (Probably-Not, Guaranteed) -> Probably-Not
     (Probably-Not, _) -> Impossible
-    (Doubtful, Guaranteed) -> Doubtful
-    (Doubtful, Cry-If-Not) -> Doubtful
+    (r, Cry-If-Not) -> r // factor out further Cry-If-Not cases
     (Doubtful, Most-Likely) -> Probably-Not
     (Doubtful, _) -> Impossible
-    (Unlikely, Guaranteed) -> Unlikely
-    (Unlikely, Cry-If-Not) -> Unlikely
     (Unlikely, Most-Likely) -> Doubtful
     (Unlikely, Probably) -> Doubtful
     (Unlikely, Mayhapsibly) -> Probably-Not
     (Unlikely, _) -> Probably-Not // (Unlikely, Unlikely) because commutative
-    (Mayhapsibly, Guaranteed) -> Mayhapsibly
-    (Mayhapsibly, Cry-If-Not) -> Mayhapsibly
     (Mayhapsibly, Most-Likely) -> Unlikely
     (Mayhapsibly, Probably) -> Unlikely
     (Mayhapsibly, _) -> Unlikely
-    (Probably, Guaranteed) -> Probably
-    (Probably, Cry-If-Not) -> Probably
     (Probably, Most-Likely) -> Mayhapsibly
     (Probably, _) -> Unlikely
-    (Most-Likely, Guaranteed) -> Most-Likely
-    (Most-Likely, Cry-If-Not) -> Most-Likely
     (Most-Likely, _) -> Probably
-    (Cry-If-Not, Guaranteed) -> Guaranteed
+    // These two are only needed because the type system doesn't understand commutativity.
     (Cry-If-Not, _) -> Cry-If-Not
     (Guaranteed, _) -> Guaranteed
+
+// KFL addition, or the probability of occurrence of at least one of two independent events.
+pub fun kfl/(+)(a: kfl, b: kfl): e kfl
+  val (l, h) = match a.cmp(b) // this operation is commutative
+    Gt -> (b, a)
+    _ -> (a, b)
+  match (l, h)
+    // Cases with _ on the right are (a, a) due to commutativity.
+    // Cases with _ on the left simplify later cases that all absorb to the right.
+    (Guaranteed, _) -> Guaranteed
+    (_, Guaranteed) -> Guaranteed
+    (Cry-If-Not, _) -> Cry-If-Not
+    (Most-Likely, Cry-If-Not) -> Guaranteed
+    (Most-Likely, _) -> Cry-If-Not
+    (_, Cry-If-Not) -> Cry-If-Not
+    (Probably, Most-Likely) -> Cry-If-Not
+    (Probably, _) -> Most-Likely
+    (_, Most-Likely) -> Most-Likely
+    (Mayhapsibly, Probably) -> Most-Likely
+    (Mayhapsibly, _) -> Probably
+    (Unlikely, Probably) -> Most-Likely
+    (Unlikely, Mayhapsibly) -> Probably
+    (Unlikely, _) -> Mayhapsibly
+    (_, Probably) -> Probably
+    (Doubtful, Mayhapsibly) -> Probably
+    (Doubtful, Unlikely) -> Mayhapsibly
+    (Doubtful, _) -> Unlikely
+    (_, Mayhapsibly) -> Mayhapsibly
+    (_, Unlikely) -> Unlikely
+    (Probably-Not, Doubtful) -> Unlikely
+    (Probably-Not, _) -> Probably-Not
+    (_, Doubtful) -> Doubtful
+    (_, Probably-Not) -> Probably-Not
+    (_, Impossible) -> Impossible