wip theory

diff --git a/THEORY b/THEORY
index e908c6838a22c471af7d2a794739ea3a4de7254f..f5518b0e848d64b4eb95a948bed7fb83bb8498be 100644 (file)
--- a/THEORY
+++ b/THEORY
@@ -3,54 +3,85 @@ relations
                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
+               C has D <=> D isin C
+       C has D => C > D
+
+define convenience function
+       cont(C) := { Cx | Cx isin C }
 
 patches
-       patch P is two subset of commits, Ptip and Pbase
+       patch P is two sets Px of commits, Ptip and Pbase
        each subset has a single ur-ancestor C0_Ptip resp C0_Pbase
-       these subsets mutually exclusive
+       all these subsets Ptip,Qbase,Rtip,Sbase mutually exclusive
        P(C) is either Ptip, Pbase, or nil (recorded in commit)
 
 commits fall into three categories wrt P
- how(P,C) = included
+ inpatch(P,C) = included
        P included in C
-               \forall D \elem Ptip,  C ] D <=> C > D
- how(P,C) = absent
+               \forall D \elem Ptip,  C has D <=> C > D
+ inpatch(P,C) = absent
        P absent from C
-               \forall D \elem Ptip, !(C ] D)
- how(P,C) = removed
+               \forall D \elem Ptip, !(C has D)
+ inpatch(P,C) = removed
        P removed from C
-               \exists E s.t.
-                       \forall D \elem Ptip,
-                               something
+               cont(C) \intersection Ptip = { }
+               but maybe \exists Cx \elem Ptip s.t. Cx < C
 
 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
+       every maximal Ce < C in Px
+       ie every Ce for which
+               C > Ce   and   !\exists C s.t. C > Ce
+
+existence of corresponding base B for every tip commit C
+       \forall C s.t. P(C) = Ptip
+               \exists B s.t. E(C,Pbase) = { B }
+ resulting function B(C)
+
+contents of tip commits
+       \forall C s.t. P(c) = Ptip
+               cont(C) = cont(B(C)) \union { Cp s.t. P(Cp) = Ptip and Cp < C }
 
-cleanness of patch
-       if P(C) = Ptip
-          B \elem E(C,Pbase)
-       then
-          C ] Cx  ^  B !] Cx  =>  P
+non-circularity
+       \forall B s.t. P(c) = Pbase
+               cont(B) \notintersect Ptip
 
 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)
+       Cx isin C  <=>  Cx = D  v  Cx isin D
+       inpatch(P,C) = inpatch(P,D)
 
-anticommit
- make C from D, P, A-, A+ 
+anticommit for removing a patch P from D to make C
+ make C from D, A-
  where
-       A+ < A- < D
+       P(C) = Qbase
+       P(A-) = Ptip
+       inpatch(P,C) = included
        E(D,Ptip) = { A- }
+ then let
+       A+ = B(A-)
+ hence
+       A+ < A- < D
        E(D,Pbase) = { A+ }
  result
-       C < { D }
+       C >1 { D }
        P(C) = P(D)
-       
+       inpatch(P,C) = removed
+
+single patch dependency application
+ make C from D, A+
+ where
+       P(C) = Qbase
+       P(A+) = Ptip
+       inpatch(P,C) != included
+ then let
+       A- = B(A+)
+ hence
+       A- < A+
+ result
+       C >1 { D, A+ } => C > D, C > A+ > A-
+       P(C) = P(D)
+       inpatch(P,C) = included
+