Subterm enumeration and containment for syntactic objects

[MCB25] §1.1–1.2. The containment / subterm theory of the SO carrier, mirroring the legacy Basic.lean theory on FreeCommMagma (LIToken ⊕ Nat). Imports only the carrier skeleton (no Merge algebra).

Contents

• SO.immediatelyContains — membership in the root children (via Nonplanar.rootChildren).
• SO.subtrees/SO.Acc — subterm enumeration (incl. root) and MCB's accessible terms Acc(T) (Def 1.2.2, root excluded).
• SO.contains/isTermOf/containsOrEq — dominance and its reflexive/term-of variants.
• subtree ↔ containment bridges, and tree-relative c-command (cCommandsIn).

Immediate containment (via Nonplanar.rootChildren)

def Minimalist.SO.immediatelyContains (x y : SO) : Prop

x immediately contains y: y is one of x's root daughters ([MCB25] §1.1; Definition 13 of the legacy theory).

Equations

• x.immediatelyContains y = (↑y ∈ (↑x).rootChildren)

@[implicit_reducible]

instance Minimalist.instDecidableImmediatelyContains (x y : SO) : Decidable (x.immediatelyContains y)

Equations

• Minimalist.instDecidableImmediatelyContains x y = Minimalist.instDecidableImmediatelyContains._aux_1 x y

@[simp]

theorem Minimalist.SO.immediatelyContains_lexLeaf (tok : LIToken) (y : SO) : ¬(lexLeaf tok).immediatelyContains y

@[simp]

theorem Minimalist.SO.immediatelyContains_traceLeaf (y : SO) : ¬traceLeaf.immediatelyContains y

@[simp]

theorem Minimalist.SO.immediatelyContains_node (l r y : SO) : (l.node r).immediatelyContains y ↔ y = l ∨ y = r

Subterm enumeration

Nonplanar.rootChildren is single-level, so deep enumeration is built fresh at the planar level and lifted. The result is a multiset of nonplanar subtrees; its PermEquiv-invariance lets it descend to the quotient.

def Minimalist.subtreesNPlanar : RoseTree SOLabel → Multiset (RootedTree.Nonplanar SOLabel)

All subtrees of a planar tree (incl. the root), as nonplanar trees.

Equations

• Minimalist.subtreesNPlanar (RoseTree.node a cs) = RootedTree.Nonplanar.mk (RoseTree.node a cs) ::ₘ Minimalist.subtreesNPlanarList cs

def Minimalist.subtreesNPlanarList : List (RoseTree SOLabel) → Multiset (RootedTree.Nonplanar SOLabel)

Auxiliary: union of subtree-multisets across a child list.

Equations

• Minimalist.subtreesNPlanarList [] = 0
• Minimalist.subtreesNPlanarList (c :: cs) = Minimalist.subtreesNPlanar c + Minimalist.subtreesNPlanarList cs

theorem Minimalist.subtreesNPlanar_permEquiv {t s : RoseTree SOLabel} (h : t.PermEquiv s) : subtreesNPlanar t = subtreesNPlanar s

subtreesNPlanar is PermEquiv-invariant, so it descends to Nonplanar.

def Minimalist.subtreesN : RootedTree.Nonplanar SOLabel → Multiset (RootedTree.Nonplanar SOLabel)

All subtrees of a nonplanar tree (incl. the root).

Equations

• Minimalist.subtreesN = RootedTree.Nonplanar.lift Minimalist.subtreesNPlanar ⋯

@[simp]

theorem Minimalist.subtreesN_mk (t : RoseTree SOLabel) : subtreesN (RootedTree.Nonplanar.mk t) = subtreesNPlanar t

theorem Minimalist.subtreesN_leaf (a : SOLabel) : subtreesN (RootedTree.Nonplanar.leaf a) = {RootedTree.Nonplanar.leaf a}

theorem Minimalist.subtreesN_node (a b : RootedTree.Nonplanar SOLabel) : subtreesN (RootedTree.Nonplanar.node (Sum.inr ()) {a, b}) = RootedTree.Nonplanar.node (Sum.inr ()) {a, b} ::ₘ (subtreesN a + subtreesN b)

subtreesN on a bare binary node: the node plus the subtrees of each child.

@[simp]

theorem Minimalist.mem_subtreesN_leaf {m : RootedTree.Nonplanar SOLabel} {a : SOLabel} : m ∈ subtreesN (RootedTree.Nonplanar.leaf a) ↔ m = RootedTree.Nonplanar.leaf a

Membership in subtreesN of a leaf.

@[simp]

theorem Minimalist.mem_subtreesN_node {m a b : RootedTree.Nonplanar SOLabel} : m ∈ subtreesN (RootedTree.Nonplanar.node (Sum.inr ()) {a, b}) ↔ m = RootedTree.Nonplanar.node (Sum.inr ()) {a, b} ∨ m ∈ subtreesN a ∨ m ∈ subtreesN b

Membership in subtreesN of a bare binary node.

theorem Minimalist.self_mem_subtreesN (u : RootedTree.Nonplanar SOLabel) : u ∈ subtreesN u

Every nonplanar tree is among its own subtrees.

SO.subtrees / SO.Acc

theorem Minimalist.subtreesN_closure (s : SO) (m : RootedTree.Nonplanar SOLabel) : m ∈ subtreesN ↑s → IsSO m

Subtrees of a syntactic object are themselves syntactic objects.

def Minimalist.SO.subtrees (s : SO) : Multiset SO

All subtrees of a syntactic object (incl. the root), as syntactic objects ([MCB25] §1.2; the legacy SyntacticObject.subtrees).

Equations

• s.subtrees = Multiset.pmap (fun (m : RootedTree.Nonplanar Minimalist.SOLabel) (h : Minimalist.IsSO m) => ⟨m, h⟩) (Minimalist.subtreesN ↑s) ⋯

@[simp]

theorem Minimalist.SO.mem_subtrees {x s : SO} : x ∈ s.subtrees ↔ ↑x ∈ subtreesN ↑s

theorem Minimalist.SO.self_mem_subtrees (s : SO) : s ∈ s.subtrees

The root is among its own subtrees.

@[simp]

theorem Minimalist.SO.mem_subtrees_node {x l r : SO} : x ∈ (l.node r).subtrees ↔ x = l.node r ∨ x ∈ l.subtrees ∨ x ∈ r.subtrees

Subtree membership at a bare binary node: the node itself, or a subtree of a daughter.

theorem Minimalist.SO.subtrees_subset_of_mem {w s : SO} (h : w ∈ s.subtrees) : w.subtrees ⊆ s.subtrees

subtrees is downward-closed along the subtree relation: every subtree of a subtree of s is a subtree of s.

Cardinality (MCB's vertex/accessible-term counts, Def 1.2.2 eq. 1.2.5)

theorem Minimalist.subtreesNPlanar_card (p : RoseTree SOLabel) : (subtreesNPlanar p).card = p.numNodes

subtreesN has one element per vertex: its cardinality is the node count.

theorem Minimalist.subtreesNPlanarList_card (cs : List (RoseTree SOLabel)) : (subtreesNPlanarList cs).card = (List.map RoseTree.numNodes cs).sum

Auxiliary list version.

theorem Minimalist.subtreesN_card (u : RootedTree.Nonplanar SOLabel) : (subtreesN u).card = u.numNodes

theorem Minimalist.SO.subtrees_card (s : SO) : s.subtrees.card = (↑s).numNodes

subtrees enumerates the vertices ([MCB25] Def 1.2.2: subtrees = Acc'(T), so its size is #V(T), the MCB workspace-size primitive).

Accessible terms Acc(T) (Def 1.2.2)

def Minimalist.SO.Acc (s : SO) : Multiset SO

MCB's accessible-terms operator Acc(T) ([MCB25] Def 1.2.2, eq. 1.2.2): the subtrees at all non-root vertices (leaves included — the counting identity eq. 1.2.5 #V = b₀ + #Acc forces this). Defined as subtrees − {self} (Acc'(T) = {T} ∪ Acc(T), eq. 1.2.3).

Equations

• s.Acc = s.subtrees - {s}

theorem Minimalist.SO.Acc_card (s : SO) : s.Acc.card = (↑s).numNodes - 1

MCB counting identity (eq. 1.2.5, one-component case): #Acc(T) = #V(T) − 1.

@[simp]

theorem Minimalist.SO.Acc_lexLeaf (tok : LIToken) : (lexLeaf tok).Acc = 0

@[simp]

theorem Minimalist.SO.Acc_traceLeaf : traceLeaf.Acc = 0

Containment / dominance

theorem Minimalist.weight_node_pair (a b : RootedTree.Nonplanar SOLabel) : (RootedTree.Nonplanar.node (Sum.inr ()) {a, b}).numNodes = a.numNodes + b.numNodes + 1

Weight of a bare binary node is one more than the sum of its daughters'.

inductive Minimalist.SO.contains : SO → SO → Prop

Containment (dominance) is the transitive closure of immediate containment ([MCB25] §1.1; the legacy contains).

• imm (x y : SO) : x.immediatelyContains y → x.contains y
• trans (x y z : SO) : x.immediatelyContains z → z.contains y → x.contains y

theorem Minimalist.SO.imm_implies_contains {x y : SO} (h : x.immediatelyContains y) : x.contains y

theorem Minimalist.SO.contains_trans {x y z : SO} (hxy : x.contains y) (hyz : y.contains z) : x.contains z

theorem Minimalist.SO.immediatelyContains_lt_weight {x y : SO} (h : x.immediatelyContains y) : (↑y).numNodes < (↑x).numNodes

Immediate containment strictly decreases weight.

theorem Minimalist.SO.contains_lt_weight {x y : SO} (h : x.contains y) : (↑y).numNodes < (↑x).numNodes

Containment strictly decreases weight; hence it is irreflexive.

theorem Minimalist.SO.contains_irrefl (x : SO) : ¬x.contains x

Subtree ↔ containment bridge

theorem Minimalist.SO.mem_subtrees_of_immediatelyContains {x y : SO} (h : x.immediatelyContains y) : y ∈ x.subtrees

theorem Minimalist.SO.mem_subtrees_of_contains {x y : SO} (h : x.contains y) : y ∈ x.subtrees

theorem Minimalist.SO.mem_subtrees_iff_eq_or_contains {x y : SO} : y ∈ x.subtrees ↔ y = x ∨ x.contains y

A subtree of x is either x itself or properly contained in x.

theorem Minimalist.SO.contains_iff_mem_subtrees_and_ne {x y : SO} : x.contains y ↔ y ∈ x.subtrees ∧ y ≠ x

Containment ↔ proper subtree membership. Gives a decision procedure for contains without well-founded recursion: y is properly contained in x iff it is a subtree distinct from x.

@[implicit_reducible]

instance Minimalist.instDecidableContains (x y : SO) : Decidable (x.contains y)

Equations

• Minimalist.instDecidableContains x y = decidable_of_iff (y ∈ x.subtrees ∧ y ≠ x) ⋯

Term-of and reflexive containment

def Minimalist.SO.isTermOf (x y : SO) : Prop

x is a term of y: x = y or y contains x.

Equations

• x.isTermOf y = (x = y ∨ y.contains x)

@[implicit_reducible]

instance Minimalist.instDecidableIsTermOf (x y : SO) : Decidable (x.isTermOf y)

Equations

• Minimalist.instDecidableIsTermOf x y = Minimalist.instDecidableIsTermOf._aux_1 x y

theorem Minimalist.SO.isTermOf_iff_mem_subtrees (x y : SO) : x.isTermOf y ↔ x ∈ y.subtrees

def Minimalist.SO.containsOrEq (x y : SO) : Prop

Reflexive containment.

Equations

• x.containsOrEq y = (x = y ∨ x.contains y)

@[implicit_reducible]

instance Minimalist.instDecidableContainsOrEq (x y : SO) : Decidable (x.containsOrEq y)

Equations

• Minimalist.instDecidableContainsOrEq x y = Minimalist.instDecidableContainsOrEq._aux_1 x y

theorem Minimalist.SO.containsOrEq_trans {x y z : SO} (hxy : x.containsOrEq y) (hyz : y.containsOrEq z) : x.containsOrEq z

RoseTree-relative c-command ([Rei76])

def Minimalist.SO.areSistersIn (root x y : SO) : Prop

x and y are sisters in root: distinct co-daughters of some subtree.

Equations

• root.areSistersIn x y = ∃ z ∈ root.subtrees, z.immediatelyContains x ∧ z.immediatelyContains y ∧ x ≠ y

@[implicit_reducible]

instance Minimalist.instDecidableAreSistersIn (root x y : SO) : Decidable (root.areSistersIn x y)

Equations

• Minimalist.instDecidableAreSistersIn root x y = Multiset.decidableExistsMultiset

def Minimalist.SO.cCommandsIn (root x y : SO) : Prop

x c-commands y in root: x has a sister (in root) that contains-or-equals y.

Equations

• root.cCommandsIn x y = ∃ z ∈ root.subtrees, root.areSistersIn x z ∧ z.containsOrEq y

@[implicit_reducible]

instance Minimalist.instDecidableCCommandsIn (root x y : SO) : Decidable (root.cCommandsIn x y)

Equations

• Minimalist.instDecidableCCommandsIn root x y = Multiset.decidableExistsMultiset

def Minimalist.SO.asymCCommandsIn (root x y : SO) : Prop

x asymmetrically c-commands y in root.

Equations

• root.asymCCommandsIn x y = (root.cCommandsIn x y ∧ ¬root.cCommandsIn y x)

@[implicit_reducible]

instance Minimalist.instDecidableAsymCCommandsIn (root x y : SO) : Decidable (root.asymCCommandsIn x y)

Equations

• Minimalist.instDecidableAsymCCommandsIn root x y = Minimalist.instDecidableAsymCCommandsIn._aux_1 root x y

decide demonstrations

The containment / c-command decision procedures reduce on concrete trees built via Nonplanar.mk ∘ RoseTree.node (not the noncomputable SO.node), confirming the "state result trees directly" discipline carries through to the relational layer.