chiark / gitweb /
invariants: introduce bases' children; some of the proofs
authorIan Jackson <ijackson@chiark.greenend.org.uk>
Sun, 4 Aug 2013 17:46:39 +0000 (18:46 +0100)
committerIan Jackson <ijackson@chiark.greenend.org.uk>
Sun, 4 Aug 2013 17:46:39 +0000 (18:46 +0100)
anticommit.tex
create-base.tex
create-tip.tex
invariants.tex
simple.tex

index 4993127..a50ed51 100644 (file)
@@ -144,3 +144,7 @@ $\qed$
 
 Not applicable.
 
+\subsection{Bases' Children}
+
+Trivial.
+
index 9325091..0b70ee4 100644 (file)
@@ -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.
+
index 382cd0c..7dec4cb 100644 (file)
@@ -80,3 +80,7 @@ Simple Foreign Inclusion applies.  $\qed$
 
 Not applicable.
 
+\subsection{Bases' Children}
+
+Trivial, by Ingredients.
+
index bb926ea..3134e5c 100644 (file)
@@ -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
index 297103a..2a2501b 100644 (file)
@@ -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.