wip theory

diff --git a/THEORY b/THEORY
new file mode 100644 (file)
index 0000000..e908c68
--- /dev/null
+++ b/THEORY
@@ -0,0 +1,56 @@
+relations
+       ancestry: of commits, a partial order
+               C > D           C is a descendant of D
+       inclusion: commit includes change made in another
+               a partial order, consistent with ancestry but more partial
+               C ] D
+       C ] D => C > D
+
+patches
+       patch P is two subset of commits, Ptip and Pbase
+       each subset has a single ur-ancestor C0_Ptip resp C0_Pbase
+       these subsets mutually exclusive
+       P(C) is either Ptip, Pbase, or nil (recorded in commit)
+
+commits fall into three categories wrt P
+ how(P,C) = included
+       P included in C
+               \forall D \elem Ptip,  C ] D <=> C > D
+ how(P,C) = absent
+       P absent from C
+               \forall D \elem Ptip, !(C ] D)
+ how(P,C) = removed
+       P removed from C
+               \exists E s.t.
+                       \forall D \elem Ptip,
+                               something
+
+the ends E(C,Px) of Px = Pbase or Ptip are
+       every maximal Ce < C in Px ie
+       every Ce for which
+               C > Ce   ^   !\exists C s.t. C > Ce
+
+cleanness of patch
+       if P(C) = Ptip
+          B \elem E(C,Pbase)
+       then
+          C ] Cx  ^  B !] Cx  =>  P
+
+normal commits
+ make C from D
+ result
+       C < { D }
+       P(C) = P(D)
+       Cx [ C  <=>  Cx = D  v  Cx [ D
+       how(P,C) = how(P,D)
+
+anticommit
+ make C from D, P, A-, A+ 
+ where
+       A+ < A- < D
+       E(D,Ptip) = { A- }
+       E(D,Pbase) = { A+ }
+ result
+       C < { D }
+       P(C) = P(D)
+