From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sun, 4 Aug 2013 17:46:39 +0000 (+0100)
Subject: invariants: introduce bases' children; some of the proofs
X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=commitdiff_plain;h=7f5f6024b93005fdd9e81c6cc39934ca57999ea8

invariants: introduce bases' children; some of the proofs
---

diff --git a/anticommit.tex b/anticommit.tex
index 4993127..a50ed51 100644
--- 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 9325091..0b70ee4 100644
--- 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 382cd0c..7dec4cb 100644
--- 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 bb926ea..3134e5c 100644
--- 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 297103a..2a2501b 100644
--- 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.