-\[\eqn{Foreign Contents:}{
- \bigforall_{C \text{ s.t. } \patchof{C} = \bot}
- D \le C \implies \patchof{D} = \bot
+\[\eqn{Foreign Contents}{
+ \bigforall_{C \in \foreign}
+ D \le C \implies \isforeign{D}
+}\]
+\[\eqn{Bases' Children}{
+ C \hasparent D \land D \in \pdn
+ \implies
+ C \in \pdn \lor C \in \pdy