Licensed unordered trees #

A relation R between a value and a multiset of values licenses an unordered tree when every subtree satisfies it at its root, the daughters' labels read without order. Since R reads a multiset, it licenses every ordered representative of the tree alike (RoseTree.licensed_of_perm), so licensing descends to the quotient.

Main definitions #

UnorderedTree.Licensed R u: every subtree of u satisfies R at its root.
UnorderedTree.IsFullBinary u: every vertex of u has zero or two children.

source

def UnorderedTree.Licensed {α : Type u_1} (R : α → Multiset α → Prop) (u : UnorderedTree α) :

Prop

A relation R licenses an unordered tree when it licenses its ordered representatives, the children's values read as a multiset.

Equations

UnorderedTree.Licensed R u = Quotient.liftOn u (fun (t : RoseTree α) => RoseTree.Licensed (fun (a : α) (ks : List α) => R a ↑ks) t) ⋯

Instances For

source

@[simp]

theorem UnorderedTree.licensed_mk {α : Type u_1} (R : α → Multiset α → Prop) (t : RoseTree α) :

Licensed R (mk t) ↔ RoseTree.Licensed (fun (a : α) (ks : List α) => R a ↑ks) t

source

theorem UnorderedTree.Licensed.mono {α : Type u_1} {R R' : α → Multiset α → Prop} (h : ∀ (a : α) (ks : Multiset α), R a ks → R' a ks) {u : UnorderedTree α} (hu : Licensed R u) :

Licensed R' u

source

@[instance_reducible]

instance UnorderedTree.instDecidableLicensed {α : Type u_1} (R : α → Multiset α → Prop) [(a : α) → (ks : Multiset α) → Decidable (R a ks)] (u : UnorderedTree α) :

Decidable (Licensed R u)

Equations