invariants: introduce bases' children; some of the proofs

diff --git a/anticommit.tex b/anticommit.tex
index 49931279917b36872d16a2f179788458ee4a7d17..a50ed51c2814c7c3257c91bf6dea55a94534051d 100644 (file)
--- a/anticommit.tex
+++ b/anticommit.tex
@@ -144,3 +144,7 @@ $\qed$
 
 Not applicable.
 
+\subsection{Bases' Children}
+
+Trivial.
+

diff --git a/create-base.tex b/create-base.tex
index 9325091196c21b02e9ffbe047e17eb9ac4a14934..0b70ee4a33187289503af3c93e95c014b7c9c261 100644 (file)
--- a/create-base.tex
+++ b/create-base.tex
@@ -15,6 +15,9 @@ create a Topbloke base branch initial commit $B$.
 \[ \eqn{ Create Acyclic }{
  L \nothaspatch \pq
 }\]
+\[ \eqn{ Ingredients }{
+ \patchof L = \foreign \lor \patchof L = \py
+}\]
 
 \subsection{No Replay}
 
@@ -57,3 +60,7 @@ Simple Foreign Inclusion applies. $\qed$
 
 Not applicable.
 
+\subsection{Bases' Children}
+
+Not applicable, by Ingredients.
+

diff --git a/create-tip.tex b/create-tip.tex
index 382cd0c69a516e431b51289e421398ac3cb9a33e..7dec4cb0d7d81b03adb8eb331934137abbba9ca1 100644 (file)
--- a/create-tip.tex
+++ b/create-tip.tex
@@ -80,3 +80,7 @@ Simple Foreign Inclusion applies.  $\qed$
 
 Not applicable.
 
+\subsection{Bases' Children}
+
+Trivial, by Ingredients.
+

diff --git a/invariants.tex b/invariants.tex
index bb926ea1f71460e1db981d110bf06078ab818a78..3134e5c9cde1d48718b1cfb70d883a9e624c0283 100644 (file)
--- a/invariants.tex
+++ b/invariants.tex
@@ -28,6 +28,11 @@ We maintain these each time we construct a new commit. \\
   \bigforall_{C \in \foreign}
     D \le C \implies \isforeign{D}
 }\]
+\[\eqn{Bases' Children}{
+  C \hasparent D \land D \in \pn
+    \implies
+  C \in \pn \lor C \in \py
+}\]
 
 We also assign each new commit $C$ to zero or one of the sets $\p$, as
 stated in the definition of $\patchof{C}$ in the summary for each kind

diff --git a/simple.tex b/simple.tex
index 297103adf419b066cb5269773de20409c14c0135..2a2501b29e6355d8046ec1eb08ef8c14eb3574c3 100644 (file)
--- a/simple.tex
+++ b/simple.tex
@@ -103,3 +103,6 @@ Simple Foreign Inclusion applies.  $\qed$
 Only relevant if $\isforeign{C}$, and in that case Totally
 Foreign Contents applies. $\qed$
 
+\subsection{Bases' Children:}
+
+Trivial.