THEORY

   1 relations
   2         ancestry: of commits, a partial order
   3                 C > D           C is a descendant of D
   4         inclusion: commit includes change made in another
   5                 a partial order, consistent with ancestry but more partial
   6                 C ] D
   7         C ] D => C > D
   8
   9 patches
  10         patch P is two subset of commits, Ptip and Pbase
  11         each subset has a single ur-ancestor C0_Ptip resp C0_Pbase
  12         these subsets mutually exclusive
  13         P(C) is either Ptip, Pbase, or nil (recorded in commit)
  14
  15 commits fall into three categories wrt P
  16  how(P,C) = included
  17         P included in C
  18                 \forall D \elem Ptip,  C ] D <=> C > D
  19  how(P,C) = absent
  20         P absent from C
  21                 \forall D \elem Ptip, !(C ] D)
  22  how(P,C) = removed
  23         P removed from C
  24                 \exists E s.t.
  25                         \forall D \elem Ptip,
  26                                 something
  27
  28 the ends E(C,Px) of Px = Pbase or Ptip are
  29         every maximal Ce < C in Px ie
  30         every Ce for which
  31                 C > Ce   ^   !\exists C s.t. C > Ce
  32
  33 cleanness of patch
  34         if P(C) = Ptip
  35            B \elem E(C,Pbase)
  36         then
  37            C ] Cx  ^  B !] Cx  =>  P
  38
  39 normal commits
  40  make C from D
  41  result
  42         C < { D }
  43         P(C) = P(D)
  44         Cx [ C  <=>  Cx = D  v  Cx [ D
  45         how(P,C) = how(P,D)
  46
  47 anticommit
  48  make C from D, P, A-, A+
  49  where
  50         A+ < A- < D
  51         E(D,Ptip) = { A- }
  52         E(D,Pbase) = { A+ }
  53  result
  54         C < { D }
  55         P(C) = P(D)
  56