FiniteDegreeTree

This file defines a FiniteDegreeTree which is a PossiblyInfiniteTree where each node has only finitely many children. The offered functions are similar to the ones of PossiblyInfiniteTree. The tree can now only infinite in one dimensions, i.e. it can have infinite depth but each node has only finitely many children by definition. However, note that there is no (global) bound for the number of children. The number of children might grow arbitrarily along the tree as long as it is finite everywhere.

def PossiblyInfiniteTree.finitely_many_children {α : Type u_1} (t : PossiblyInfiniteTree α) : Prop

A PossiblyInfiniteTree has finitely_many_children if for each subtree, the list of PossiblyInfiniteTree.childTrees is PossiblyInfiniteList.finite.

Equations

• t.finitely_many_children = ∀ (subtree : PossiblyInfiniteTree α), subtree <:+ t → subtree.childTrees.finite

theorem PossiblyInfiniteTree.finitely_many_children_empty {α : Type u_1} : empty.finitely_many_children

The PossiblyInfiniteTree.empty tree has finitely_many_children.

structure FiniteDegreeTree (α : Type u) : Type u

A FiniteDegreeTree is a PossiblyInfiniteTree with the finitely_many_children property.

• tree : PossiblyInfiniteTree α
• finitely_many_children : self.tree.finitely_many_children

Basics

The essential functions on infinite trees, mainly get, drop, and root. The childTrees function is defined separately here as for the PossiblyInfiniteTree.

def FiniteDegreeTree.get? {α : Type u_1} (t : FiniteDegreeTree α) (ns : List Nat) : Option α

Obtains the element of the tree at the given address.

Equations

• t.get? ns = t.tree.get? ns

def FiniteDegreeTree.drop {α : Type u_1} (t : FiniteDegreeTree α) (ns : List Nat) : FiniteDegreeTree α

Obtains the subtree at the given address (by dropping everything else).

Equations

• t.drop ns = { tree := t.tree.drop ns, finitely_many_children := ⋯ }

def FiniteDegreeTree.root {α : Type u_1} (t : FiniteDegreeTree α) : Option α

Get the element at the root of the tree (i.e. at the empty address).

Equations

• t.root = t.tree.root

instance FiniteDegreeTree.instMembership {α : Type u_1} : Membership α (FiniteDegreeTree α)

Equations

• FiniteDegreeTree.instMembership = { mem := fun (t : FiniteDegreeTree α) (a : α) => a ∈ t.tree }

theorem FiniteDegreeTree.mem_iff {α : Type u_1} {t : FiniteDegreeTree α} {e : α} : e ∈ t ↔ ∃ (ns : List Nat), t.get? ns = some e

An element is a member of the tree iff it occurs at some address.

theorem FiniteDegreeTree.ext {α : Type u_1} {t1 t2 : FiniteDegreeTree α} : (∀ (ns : List Nat), t1.get? ns = t2.get? ns) → t1 = t2

Two FiniteDegreeTrees are the same if they agree on all addresses.

theorem FiniteDegreeTree.ext_iff {α : Type u_1} {t1 t2 : FiniteDegreeTree α} : t1 = t2 ↔ ∀ (ns : List Nat), t1.get? ns = t2.get? ns

theorem FiniteDegreeTree.get?_drop {α : Type u_1} {t : FiniteDegreeTree α} {ns ns' : List Nat} : (t.drop ns).get? ns' = t.get? (ns ++ ns')

Get after drop can be rewritten into get.

theorem FiniteDegreeTree.drop_nil {α : Type u_1} {t : FiniteDegreeTree α} : t.drop [] = t

Dropping the empty address changes nothing.

theorem FiniteDegreeTree.drop_drop {α : Type u_1} {t : FiniteDegreeTree α} {ns ns' : List Nat} : (t.drop ns).drop ns' = t.drop (ns ++ ns')

Two calls to drop can be combined.

theorem FiniteDegreeTree.root_eq {α : Type u_1} {t : FiniteDegreeTree α} : t.root = t.get? []

The root is equal to getting the empty address.

theorem FiniteDegreeTree.root_mem {α : Type u_1} {t : FiniteDegreeTree α} (r : α) : r ∈ t.root → r ∈ t

The root is in the tree.

theorem FiniteDegreeTree.root_drop {α : Type u_1} {t : FiniteDegreeTree α} {ns : List Nat} : (t.drop ns).root = t.get? ns

The root of the dropped tree at address ns is exactly the element at address ns.

Empty Infinite Trees

The empty FiniteDegreeTree is simply the FiniteDegreeTree that is none on all addresses. That is, its underlying PossiblyInfiniteTree is PossiblyInfiniteTree.empty.

def FiniteDegreeTree.empty {α : Type u_1} : FiniteDegreeTree α

The empty FiniteDegreeTree is essentially PossiblyInfiniteTree.empty.

Equations

• FiniteDegreeTree.empty = { tree := PossiblyInfiniteTree.empty, finitely_many_children := ⋯ }

theorem FiniteDegreeTree.get?_empty {α : Type u_1} {n : List Nat} : empty.get? n = none

Getting from the empty tree always returns none.

theorem FiniteDegreeTree.drop_empty {α : Type u_1} {ns : List Nat} : empty.drop ns = empty

Dropping from the empty tree again yields the empty tree.

theorem FiniteDegreeTree.root_empty {α : Type u_1} : empty.root = none

The root of the empty tree is none.

theorem FiniteDegreeTree.empty_iff_root_none {α : Type u_1} {t : FiniteDegreeTree α} : t = empty ↔ t.root = none

A tree is empty if and only if the root is none.

Child Trees

Defining the childTrees function requires a bit of machinery. We only want to return the child trees that are not already empty. Then all returned trees have a non-none root, which we aim to capture directly in the return type.

@[reducible, inline]

abbrev FiniteDegreeTree.FiniteDegreeTreeWithRoot (α : Type u) : Type u

The FiniteDegreeTreeWithRoot is a FiniteDegreeTree where the root is not none.

Equations

• FiniteDegreeTree.FiniteDegreeTreeWithRoot α = { t : FiniteDegreeTree α // t.root ≠ none }

FiniteDegreeTreeWithRoot

For the FiniteDegreeTreeWithRoot we mainly provide some functions to convert FiniteDegreeTree to and from Option FiniteDegreeTreeWithRoot. Clearly, if a FiniteDegreeTree has a non-none root, we can convert it directly into a FiniteDegreeTreeWithRoot, otherwise, we simply convert it to none. Also in the other direction, none can just be converted to PossiblyInfiniteTree.empty and any FiniteDegreeTreeWithRoot is already a FiniteDegreeTree.

So far this is similar to PossiblyInfiniteTreeWithRoot and mainly implemented using its existing methods. For this purpose, we also provide methods from_possibly_infinite and to_possibly_infinite that allow to convert between FiniteDegreeTreeWithRoot and PossiblyInfiniteTreeWithRoot.

def FiniteDegreeTree.FiniteDegreeTreeWithRoot.from_possibly_infinite {α : Type u_1} (t : PossiblyInfiniteTree.PossiblyInfiniteTreeWithRoot α) (fin : t.val.finitely_many_children) : FiniteDegreeTreeWithRoot α

Equations

• FiniteDegreeTree.FiniteDegreeTreeWithRoot.from_possibly_infinite t fin = ⟨{ tree := t.val, finitely_many_children := fin }, ⋯⟩

def FiniteDegreeTree.FiniteDegreeTreeWithRoot.to_possibly_infinite {α : Type u_1} (t : FiniteDegreeTreeWithRoot α) : PossiblyInfiniteTree.PossiblyInfiniteTreeWithRoot α

Equations

• t.to_possibly_infinite = ⟨t.val.tree, ⋯⟩

def FiniteDegreeTree.FiniteDegreeTreeWithRoot.opt_to_tree {α : Type u_1} (opt : Option (FiniteDegreeTreeWithRoot α)) : FiniteDegreeTree α

Equations

• One or more equations did not get rendered due to their size.

def FiniteDegreeTree.FiniteDegreeTreeWithRoot.tree_to_opt {α : Type u_1} (t : FiniteDegreeTree α) : Option (FiniteDegreeTreeWithRoot α)

Equations

• One or more equations did not get rendered due to their size.

theorem FiniteDegreeTree.FiniteDegreeTreeWithRoot.from_possibly_infinite_after_to_possibly_infinite {α : Type u_1} {t : FiniteDegreeTreeWithRoot α} : from_possibly_infinite t.to_possibly_infinite ⋯ = t

theorem FiniteDegreeTree.FiniteDegreeTreeWithRoot.to_possibly_infinite_after_from_possibly_infinite {α : Type u_1} (t : PossiblyInfiniteTree.PossiblyInfiniteTreeWithRoot α) (fin : t.val.finitely_many_children) : (from_possibly_infinite t fin).to_possibly_infinite = t

theorem FiniteDegreeTree.FiniteDegreeTreeWithRoot.opt_to_tree_none_iff {α : Type u_1} {opt : Option (FiniteDegreeTreeWithRoot α)} : opt = none ↔ (opt_to_tree opt).root = none

theorem FiniteDegreeTree.FiniteDegreeTreeWithRoot.tree_to_opt_none_iff {α : Type u_1} {t : FiniteDegreeTree α} : tree_to_opt t = none ↔ t.root = none

theorem FiniteDegreeTree.FiniteDegreeTreeWithRoot.tree_to_opt_some_iff {α : Type u_1} {t : FiniteDegreeTree α} {t' : FiniteDegreeTreeWithRoot α} : tree_to_opt t = some t' ↔ t = t'.val ∧ t.root.isSome = true

theorem FiniteDegreeTree.FiniteDegreeTreeWithRoot.tree_to_opt_after_opt_to_tree {α : Type u_1} {opt : Option (FiniteDegreeTreeWithRoot α)} : tree_to_opt (opt_to_tree opt) = opt

theorem FiniteDegreeTree.FiniteDegreeTreeWithRoot.opt_to_tree_after_tree_to_opt {α : Type u_1} {t : FiniteDegreeTree α} : opt_to_tree (tree_to_opt t) = t

The actual childTrees definition

With FiniteDegreeTreeWithRoot in place, we can now define the actual childTrees function.

def FiniteDegreeTree.childTrees {α : Type u_1} (t : FiniteDegreeTree α) : List (FiniteDegreeTreeWithRoot α)

The childTrees of a FiniteDegreeTree are the List of all child trees that are not empty, i.e. it only consists of FiniteDegreeTreeWithRoot. Note that we can indeed build a finite List since we have finitely_many_children in place.

Equations

• One or more equations did not get rendered due to their size.

theorem FiniteDegreeTree.mem_childTrees_iff {α : Type u_1} {t : FiniteDegreeTree α} (c : FiniteDegreeTreeWithRoot α) : c ∈ t.childTrees ↔ c.to_possibly_infinite ∈ t.tree.childTrees

FiniteDegreeTree.childTrees can be expressed through PossiblyInfiniteTree.childTrees.

theorem FiniteDegreeTree.get?_childTrees {α : Type u_1} {t : FiniteDegreeTree α} (n : Nat) : t.childTrees[n]? = FiniteDegreeTreeWithRoot.tree_to_opt (t.drop [n])

Getting a child tree is the same as dropping the corresponding singleton address.

theorem FiniteDegreeTree.get_childTrees {α : Type u_1} {t : FiniteDegreeTree α} (n : Nat) (lt : n < t.childTrees.length) : t.childTrees[n].val = t.drop [n]

Getting a child tree is the same as dropping the corresponding singleton address.

theorem FiniteDegreeTree.get?_get?_childTrees {α : Type u_1} {t : FiniteDegreeTree α} (n : Nat) (ns : List Nat) : (FiniteDegreeTreeWithRoot.opt_to_tree t.childTrees[n]?).get? ns = t.get? (n :: ns)

Getting at an address in a child tree can be combined into a single get call.

theorem FiniteDegreeTree.childTrees_empty {α : Type u_1} : empty.childTrees = []

The childTrees of the empty tree are exactly [].

Node Constructor

Similar to the PossiblyInfiniteTree, we can also define a node constructor on the FiniteDegreeTree.

def FiniteDegreeTree.node {α : Type u_1} (root : α) (childTrees : List (FiniteDegreeTreeWithRoot α)) : FiniteDegreeTree α

Construct a FiniteDegreeTree from a List of FiniteDegreeTreeWithRoot and a new root element.

Equations

• One or more equations did not get rendered due to their size.

theorem FiniteDegreeTree.get?_node_nil {α : Type u_1} {root : α} {childTrees : List (FiniteDegreeTreeWithRoot α)} : (node root childTrees).get? [] = some root

Getting the element at address [] on node is the new root.

theorem FiniteDegreeTree.get?_node_cons {α : Type u_1} {root : α} {childTrees : List (FiniteDegreeTreeWithRoot α)} (n : Nat) (ns : List Nat) : (node root childTrees).get? (n :: ns) = (FiniteDegreeTreeWithRoot.opt_to_tree childTrees[n]?).get? ns

Getting any address != [] on node yields the respective element from the previous FiniteDegreeTreeWithRoot.

theorem FiniteDegreeTree.drop_node_cons {α : Type u_1} {root : α} {childTrees : List (FiniteDegreeTreeWithRoot α)} {n : Nat} {ns : List Nat} : (node root childTrees).drop (n :: ns) = (FiniteDegreeTreeWithRoot.opt_to_tree childTrees[n]?).drop ns

Dropping from node with an address of the form n::ns is the same as getting the n child from the child trees used in the construction and then dropping ns there.

theorem FiniteDegreeTree.root_node {α : Type u_1} {root : α} {childTrees : List (FiniteDegreeTreeWithRoot α)} : (node root childTrees).root = some root

The root of node is the root used in the construction.

theorem FiniteDegreeTree.childTrees_node {α : Type u_1} {root : α} {childTrees : List (FiniteDegreeTreeWithRoot α)} : (node root childTrees).childTrees = childTrees

The childTrees of node are the childTrees used in the construction.

theorem FiniteDegreeTree.node_root_childTrees {α : Type u_1} {t : FiniteDegreeTree α} {root : α} (h : t.root = some root) : t = node root t.childTrees

Any FiniteDegreeTree where the root is not none can be written using the node constructor.

ChildNodes

It can be convenient to obtain a list of the immediate child nodes of a given tree. This is equivalent to mapping each child tree to its root.

def FiniteDegreeTree.childNodes {α : Type u_1} (t : FiniteDegreeTree α) : List α

The childNodes are PossiblyInfiniteTree.childNodes.

Equations

• t.childNodes = t.tree.childNodes.toList_of_finite ⋯

theorem FiniteDegreeTree.get?_childNodes {α : Type u_1} {t : FiniteDegreeTree α} {n : Nat} : t.childNodes[n]? = (FiniteDegreeTreeWithRoot.opt_to_tree t.childTrees[n]?).root

Getting the nth childNodes is the root of the nth childTrees.

theorem FiniteDegreeTree.childNodes_eq {α : Type u_1} {t : FiniteDegreeTree α} : t.childNodes = List.map (fun (t : FiniteDegreeTreeWithRoot α) => t.val.root.get ⋯) t.childTrees

The childNodes are the roots of the childTrees.

theorem FiniteDegreeTree.length_childNodes {α : Type u_1} {t : FiniteDegreeTree α} : t.childNodes.length = t.childTrees.length

The childNodes have the same length as the childTrees.

theorem FiniteDegreeTree.get_childNodes {α : Type u_1} {t : FiniteDegreeTree α} (n : Nat) (lt : n < t.childNodes.length) : some t.childNodes[n] = t.childTrees[n].val.root

Getting the nth childNodes is the root of the nth childTrees.

theorem FiniteDegreeTree.mem_of_mem_childNodes {α : Type u_1} {t : FiniteDegreeTree α} (c : α) : c ∈ t.childNodes → c ∈ t

Each child node is a tree member.

theorem FiniteDegreeTree.childNodes_empty {α : Type u_1} : empty.childNodes = []

The childNodes of the empty tree are [].

Suffixes

Here, we define a suffix relation on FiniteDegreeTree inspired by List.IsSuffix. For t1 and t2, t1 <:+ t2 denotes that t1 is a subtree of t2.

The suffix relation is reflexive and transitive but not necesarrily antisymmetric! Note also that InfiniteList.suffix_or_suffix_of_suffix has no equivalent statement here, i.e. just because two trees are subtrees of the same parent tree, we cannot say anything about their relation to one another. They might be totally "disconnected".

def FiniteDegreeTree.IsSuffix {α : Type u_1} (t1 t2 : FiniteDegreeTree α) : Prop

A suffix relation on infinite trees. This is inspired by List.IsSuffix. Read t1 <:+ t2 as: t1 is a subtree of t2.

Equations

• (t1 <:+ t2) = (t1.tree <:+ t2.tree)

def FiniteDegreeTree.«term_<:+_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem FiniteDegreeTree.IsSuffix_iff {α : Type u_1} {t1 t2 : FiniteDegreeTree α} : t1 <:+ t2 ↔ ∃ (ns : List Nat), t2.drop ns = t1

t1 is a subtree of t2 if t1 can be obtained from t2 by dropping.

theorem FiniteDegreeTree.IsSuffix_refl {α : Type u_1} {t : FiniteDegreeTree α} : t <:+ t

The suffix relation is reflexive.

theorem FiniteDegreeTree.IsSuffix_trans {α : Type u_1} {t1 t2 t3 : FiniteDegreeTree α} : t1 <:+ t2 → t2 <:+ t3 → t1 <:+ t3

The suffix relation is transitive.

theorem FiniteDegreeTree.mem_of_mem_suffix {α : Type u_1} {t1 t2 : FiniteDegreeTree α} (suffix : t1 <:+ t2) (e : α) : e ∈ t1 → e ∈ t2

A member of a subtree is also a member of the current tree.

theorem FiniteDegreeTree.IsSuffix_drop {α : Type u_1} {t : FiniteDegreeTree α} (ns : List Nat) : t.drop ns <:+ t

Dropping elements yields a subtree.

theorem FiniteDegreeTree.IsSuffix_of_mem_childTrees {α : Type u_1} {t : FiniteDegreeTree α} (c : FiniteDegreeTreeWithRoot α) : c ∈ t.childTrees → c.val <:+ t

Each child tree is a subtree.

theorem FiniteDegreeTree.empty_suffix_of_empty {α : Type u_1} {t : FiniteDegreeTree α} : t <:+ empty → t = empty

Every suffix of the empty tree is empty.

theorem FiniteDegreeTree.no_orphans {α : Type u_1} {t : FiniteDegreeTree α} (subtree : FiniteDegreeTree α) : subtree <:+ t → subtree.root = none → subtree.childNodes = []

We can express the PossiblyInfiniteTree.no_orphans' condition directly on FiniteDegreeTree.

Recursor for Members

We define a recursion (induction) principle for members (Elements) of an FiniteDegreeTree called mem_rec. This can be used with the induction tactic to prove a property for each Element of an FiniteDegreeTree. Note that for using this coveniently, the goal needs to expressed (rewritten) using an Element.

def FiniteDegreeTree.Element {α : Type u_1} (t : FiniteDegreeTree α) : Type u_1

A tree Element is a Subtype featuring a proof of being a tree member.

Equations

• t.Element = { e : α // e ∈ t }

theorem FiniteDegreeTree.mem_rec {α : Type u_1} {t : FiniteDegreeTree α} {motive : t.Element → Prop} (root : ∀ (r : α) (mem : r ∈ t.root), motive ⟨r, ⋯⟩) (step : ∀ (t2 : FiniteDegreeTree α) (suffix : t2 <:+ t), (∃ (r : α), ∃ (mem : r ∈ t2.root), motive ⟨r, ⋯⟩) → ∀ {c : α} (mem : c ∈ t2.childNodes), motive ⟨c, ⋯⟩) (a : t.Element) : motive a

A recursor for proving properties about tree members (Elements) via induction.

Branches

Branches are essentially PossiblyInfiniteLists in a FiniteDegreeTree and can be characterizes by an infinite "address", i.e. InfiniteList Nat. Here, we merely define them as the branches of the underlying PossiblyInfiniteTree.

def FiniteDegreeTree.branches {α : Type u_1} (t : FiniteDegreeTree α) : Set (PossiblyInfiniteList α)

The branches in the FiniteDegreeTree are exactly the branches in the underlying PossiblyInfiniteTree.

Equations

• t.branches = t.tree.branches

theorem FiniteDegreeTree.branches_eq {α : Type u_1} {t : FiniteDegreeTree α} : t.branches = fun (b : PossiblyInfiniteList α) => b.head = t.root ∧ (t.childTrees = [] ∧ b.tail = PossiblyInfiniteList.empty ∨ ∃ (c : FiniteDegreeTreeWithRoot α), c ∈ t.childTrees ∧ b.tail ∈ c.val.branches)

The set of branches can equivalently be expressed as the set of all PossiblyInfiniteLists where the head equals the root of the tree and the tail occurs in the branches of some childTree. If there are no childTrees, then the tail needs to be empty.

Branch Generation

We can use PossiblyInfiniteList.generate to construct branches in a FiniteDegreeTree. Here, we just proxy the existing function PossiblyInfiniteTree.generate_branch. First of all, this requires that the mapper function produces a FiniteDegreeTreeWithRoot. Intuitively, using all the roots of these trees gives us a branch. But this is only true if the generate trees are always child trees of each other and the generation indeed creates a maximal branch, meaning that once the generation stops, there would indeed by no childTrees to continue. This condition is used in the generate_branch_mem_branches theorem to proof that a PossiblyInfiniteList from the generate_branch function is indeed in branches.

def FiniteDegreeTree.generate_branch {β : Type u_1} {α : Type u_2} (start : Option β) (generator : β → Option β) (mapper : β → FiniteDegreeTreeWithRoot α) : PossiblyInfiniteList α

Given a generator and a mapper that maps generated elements to FiniteDegreeTreeWithRoot, construct an PossiblyInfiniteList with the goal of constructing a branch in a tree.

Equations

• FiniteDegreeTree.generate_branch start generator mapper = PossiblyInfiniteTree.generate_branch start generator fun (b : β) => (mapper b).to_possibly_infinite

theorem FiniteDegreeTree.generate_branch_mem_branches {β : Type u_1} {α : Type u_2} {start : Option β} {generator : β → Option β} {mapper : β → FiniteDegreeTreeWithRoot α} (next_is_child : ∀ (b b' : β), b' ∈ generator b → mapper b' ∈ (mapper b).val.childTrees) (maximal : ∀ (b : β), generator b = none → (mapper b).val.childTrees = []) (isSome_start : start.isSome = true) : generate_branch start generator mapper ∈ (mapper (start.get isSome_start)).val.branches

If the generated trees are childTrees of each other and the generated branch is maximal, i.e. the generation only stops if there are no childTrees available anymore, then the generated PossiblyInfiniteList is indeed a branch.

theorem FiniteDegreeTree.head_generate_branch {β : Type u_1} {α : Type u_2} {start : Option β} {generator : β → Option β} {mapper : β → FiniteDegreeTreeWithRoot α} : (generate_branch start generator mapper).head = Option.map (fun (s : β) => (mapper s).val.root.get ⋯) start

The PossiblyInfiniteList.head of generate_branch is the root of the first tree.

theorem FiniteDegreeTree.get?_generate_branch {β : Type u_1} {α : Type u_2} {start : Option β} {generator : β → Option β} {mapper : β → FiniteDegreeTreeWithRoot α} (n : Nat) : (generate_branch start generator mapper).get? n = Option.map (fun (t : FiniteDegreeTreeWithRoot α) => t.val.root.get ⋯) ((PossiblyInfiniteList.generate start generator mapper).get? n)

Getting the nth element from a generate_branch result is the root of the nth generated tree.

theorem FiniteDegreeTree.tail_generate_branch {β : Type u_1} {α : Type u_2} {start : Option β} {generator : β → Option β} {mapper : β → FiniteDegreeTreeWithRoot α} : (generate_branch start generator mapper).tail = generate_branch (start.bind generator) generator mapper

The PossiblyInfiniteList.tail of generate_branch is the branch generated when applying the generator function once on the starting element before the actual generation.

Leaves

The leaves of a FiniteDegreeTree is the set of elements that occur in a node that has no childNodes. The function is simply defined via PossiblyInfiniteTree.leaves for the underlying tree.

def FiniteDegreeTree.leaves {α : Type u_1} (t : FiniteDegreeTree α) : Set α

Equations

• t.leaves = t.tree.leaves

Constructing a Tree from a Branch

A PossiblyInfiniteList directly corresponds to the FiniteDegreeTree where the list is the "first" branch (with the address that only consists of zeros) and all other nodes are none.

def FiniteDegreeTree.from_branch {α : Type u_1} (b : PossiblyInfiniteList α) : FiniteDegreeTree α

Equations

• FiniteDegreeTree.from_branch b = { tree := PossiblyInfiniteTree.from_branch b, finitely_many_children := ⋯ }