Self-generating sets

DefinitionStrict growth of a set of generators#✓fully proved

A finite set \(F\) of functions \(\mathbb{N} \to \mathbb{N}\) has strict growth when \(x < f(x)\) for every \(f \in F\) and every \(x \in \mathbb{N}\).

def StrictGrowth (F : Finset (Nat → Nat)) : Prop :=
  ∀ f ∈ F, ∀ x, x < f x

Used by 4

Used byUnder strict growth, a fixed-point set is the generated set · Under strict growth, a fixed-point set is the intersection of all self-generating sets · Under strict growth, a fixed-point set is the least self-generating set · Under strict growth, fixed-point sets are unique

DefinitionSelf-generating sets#✓fully proved

Let \(F\) be a finite set of functions \(\mathbb{N} \to \mathbb{N}\) and let \(s \in \mathbb{N}\). A set \(\Gamma \subseteq \mathbb{N}\) is self-generating for \(s\) and \(F\) when \(s \in \Gamma\) and \(f(x) \in \Gamma\) for every \(f \in F\) and every \(x \in \Gamma\).

The source writes this condition as \(\mathrm{SG}(s, F)\).

def SG (F : Finset (Nat → Nat)) (seed : Nat) (Gamma : Set Nat) : Prop :=
  seed ∈ Gamma ∧ ∀ f ∈ F, ∀ x ∈ Gamma, f x ∈ Gamma

Used by 8

Used byUnder strict growth, a fixed-point set is the generated set · Under strict growth, a fixed-point set is the intersection of all self-generating sets · Under strict growth, a fixed-point set is the least self-generating set · Fixed-point sets are self-generating · The generated set is the intersection of all self-generating sets · The generated set is self-generating · The generated set lies in every self-generating set · The least self-generating set is the generated set

DefinitionFixed-point sets for a seed and generators#✓fully proved

Let \(F\) be a finite set of functions \(\mathbb{N} \to \mathbb{N}\) and let \(s \in \mathbb{N}\). A set \(C \subseteq \mathbb{N}\) is a fixed-point set for \(F\) and \(s\) when, for every \(y \in \mathbb{N}\), \(y \in C\) if and only if \(y = s\) or \(y = f(x)\) for some \(f \in F\) and some \(x \in C\); equivalently, \(C = \{s\} \cup \bigcup_{f \in F} f(C)\).

def FixedPoint (F : Finset (Nat → Nat)) (seed : Nat) (C : Set Nat) : Prop :=
  ∀ y, y ∈ C ↔ y = seed ∨ ∃ f ∈ F, ∃ x ∈ C, f x = y

Used by 6

Used byUnder strict growth, a fixed-point set is the generated set · Under strict growth, a fixed-point set is the intersection of all self-generating sets · Under strict growth, a fixed-point set is the least self-generating set · Fixed-point sets are self-generating · Under strict growth, fixed-point sets are unique · The generated set is a fixed-point set

InductiveReachability from a seed by generators#✓fully proved

Let \(F\) be a finite set of functions \(\mathbb{N} \to \mathbb{N}\) and let \(s \in \mathbb{N}\). Reachability from \(s\) is the least predicate on \(\mathbb{N}\) that holds at \(s\) and holds at \(f(w)\) whenever it holds at \(w\) and \(f \in F\). Thus \(y\) is reachable exactly when \(y = f_k(\cdots f_1(s) \cdots)\) for some \(k \ge 0\) and \(f_1, \ldots, f_k \in F\); the case \(k = 0\) is \(s\) itself.

inductive Gen (F : Finset (Nat → Nat)) (seed : Nat) : Nat → Prop where
  | seed_mem : Gen F seed seed
  | step (w : Nat) : Gen F seed w → ∀ f ∈ F, Gen F seed (f w)

Used by 5

Used byUnder strict growth, a fixed-point set is the generated set · The generated set is a fixed-point set · The generated set is self-generating · The generated set lies in every self-generating set · Set generated from a seed

DefinitionSet generated from a seed#✓fully proved

For a finite set \(F\) of functions \(\mathbb{N} \to \mathbb{N}\) and a seed \(s \in \mathbb{N}\), the set generated from \(s\) by \(F\) consists of all numbers \(f_k(\cdots f_1(s) \cdots)\) with \(k \ge 0\) and \(f_1, \dots, f_k \in F\); the case \(k = 0\) gives \(s\) itself.

def GeneratedSet (F : Finset (Nat → Nat)) (seed : Nat) : Set Nat :=
  {y | Gen F seed y}

Uses 1 · Used by 9

Statement usesReachability from a seed by generators

Used byUnder strict growth, a fixed-point set is the generated set · Under strict growth, a fixed-point set is the intersection of all self-generating sets · Under strict growth, a fixed-point set is the least self-generating set · Under strict growth, fixed-point sets are unique · The generated set is the intersection of all self-generating sets · The generated set is a fixed-point set · The generated set is self-generating · The generated set lies in every self-generating set · The least self-generating set is the generated set

TheoremFixed-point sets are self-generating#✓fully proved

Let \(F\) be a finite set of functions \(\mathbb{N} \to \mathbb{N}\) and \(s \in \mathbb{N}\). Every fixed-point set \(C\) for \(F\) and \(s\) is self-generating: \(s \in C\), and \(f(x) \in C\) for every \(f \in F\) and every \(x \in C\).

theorem fixedPoint_isSG {F : Finset (Nat → Nat)} {seed : Nat} {C : Set Nat}
    (hC : FixedPoint F seed C) : SG F seed C

Uses 2 · Used by 2

Statement usesFixed-point sets for a seed and generators · Self-generating sets

Used byUnder strict growth, a fixed-point set is the generated set · Under strict growth, a fixed-point set is the least self-generating set

TheoremThe generated set is self-generating#✓fully proved

Let \(F\) be a finite set of functions \(\mathbb{N} \to \mathbb{N}\) and \(s \in \mathbb{N}\). The set generated from \(s\) by \(F\) contains \(s\) and is closed under every \(f \in F\): if \(x\) is in it and \(f \in F\), then \(f(x)\) is in it.

theorem generated_isSG {F : Finset (Nat → Nat)} {seed : Nat} :
    SG F seed (GeneratedSet F seed)

Uses 3 · Used by 2

Statement usesSet generated from a seed · Self-generating sets

Proof usesReachability from a seed by generators

Used byThe generated set is the intersection of all self-generating sets · The least self-generating set is the generated set

TheoremThe generated set lies in every self-generating set#✓fully proved

Let \(F\) be a finite set of functions \(\mathbb{N} \to \mathbb{N}\) and let \(s \in \mathbb{N}\). If a set \(G \subseteq \mathbb{N}\) contains \(s\) and satisfies \(f(x) \in G\) for every \(f \in F\) and every \(x \in G\), then \(G\) contains the set generated from \(s\) by \(F\), that is, every number obtained from \(s\) by applying finitely many (possibly no) functions of \(F\) in succession.

theorem generated_le_of_sg {F : Finset (Nat → Nat)} {seed : Nat} {G : Set Nat}
    (hG : SG F seed G) : GeneratedSet F seed ⊆ G

Uses 3 · Used by 4

Statement usesSet generated from a seed · Self-generating sets

Proof usesReachability from a seed by generators

Used byUnder strict growth, a fixed-point set is the generated set · Under strict growth, a fixed-point set is the least self-generating set · The generated set is the intersection of all self-generating sets · The least self-generating set is the generated set

TheoremThe generated set is a fixed-point set#✓fully proved

Let \(F\) be a finite set of functions \(\mathbb{N} \to \mathbb{N}\) and \(s \in \mathbb{N}\), and let \(\Gamma\) be the set generated from \(s\) by \(F\). Then for every \(y \in \mathbb{N}\), \(y \in \Gamma\) if and only if \(y = s\) or \(y = f(x)\) for some \(f \in F\) and \(x \in \Gamma\).

This direction does not require the generators to be strictly increasing.

theorem generated_fixedPoint {F : Finset (Nat → Nat)} {seed : Nat} :
    FixedPoint F seed (GeneratedSet F seed)

Uses 3

Statement usesFixed-point sets for a seed and generators · Set generated from a seed

Proof usesReachability from a seed by generators

TheoremUnder strict growth, a fixed-point set is the generated set#✓fully proved

Let \(F\) be a finite set of functions \(\mathbb{N} \to \mathbb{N}\) with \(x < f(x)\) for every \(f \in F\) and every \(x \in \mathbb{N}\), let \(s \in \mathbb{N}\), and let \(C \subseteq \mathbb{N}\) be a fixed-point set for \(F\) and \(s\): \(y \in C\) exactly when \(y = s\) or \(y = f(x)\) for some \(f \in F\) and \(x \in C\). Then \(C\) equals the set generated from \(s\) by \(F\), the numbers obtained from \(s\) by applying finitely many functions of \(F\).

The proof is by strong induction: if an element of \(C\) is \(f(x)\) with \(f \in F\) and \(x \in C\), then strict growth gives \(x < f(x)\).

theorem fixedPoint_eq_generated {F : Finset (Nat → Nat)} {seed : Nat} {C : Set Nat}
    (hg : StrictGrowth F) (hC : FixedPoint F seed C) :
    C = GeneratedSet F seed

Uses 7 · Used by 3

Statement usesFixed-point sets for a seed and generators · Set generated from a seed · Strict growth of a set of generators

Proof usesReachability from a seed by generators · Self-generating sets · Fixed-point sets are self-generating · The generated set lies in every self-generating set

Used byUnder strict growth, a fixed-point set is the intersection of all self-generating sets · Under strict growth, a fixed-point set is the least self-generating set · Under strict growth, fixed-point sets are unique

TheoremThe generated set is the intersection of all self-generating sets#✓fully proved

Let \(F\) be a finite set of functions \(\mathbb{N} \to \mathbb{N}\) and \(s \in \mathbb{N}\). The set generated from \(s\) by \(F\) equals the intersection of all sets \(G \subseteq \mathbb{N}\) that contain \(s\) and are closed under every \(f \in F\).

theorem generated_eq_sInter {F : Finset (Nat → Nat)} {seed : Nat} :
    GeneratedSet F seed = Set.sInter {G | SG F seed G}

Uses 4 · Used by 1

Statement usesSet generated from a seed · Self-generating sets

Proof usesThe generated set is self-generating · The generated set lies in every self-generating set

Used byUnder strict growth, a fixed-point set is the intersection of all self-generating sets

TheoremUnder strict growth, a fixed-point set is the intersection of all self-generating sets#✓fully proved

Let \(F\) be a finite set of functions \(\mathbb{N} \to \mathbb{N}\) with \(x < f(x)\) for every \(f \in F\) and every \(x \in \mathbb{N}\), and let \(s \in \mathbb{N}\). If \(C\) is a fixed-point set for \(F\) and \(s\), then \(C\) is the intersection of all sets \(G \subseteq \mathbb{N}\) that contain \(s\) and are closed under every \(f \in F\).

theorem fixedPoint_eq_sInter {F : Finset (Nat → Nat)} {seed : Nat} {C : Set Nat}
    (hg : StrictGrowth F) (hC : FixedPoint F seed C) :
    C = Set.sInter {G | SG F seed G}

Uses 6

Statement usesFixed-point sets for a seed and generators · Self-generating sets · Strict growth of a set of generators

Proof usesSet generated from a seed · Under strict growth, a fixed-point set is the generated set · The generated set is the intersection of all self-generating sets

TheoremUnder strict growth, a fixed-point set is the least self-generating set#✓fully proved

Let \(F\) be a finite set of functions \(\mathbb{N} \to \mathbb{N}\) with \(x < f(x)\) for every \(f \in F\) and every \(x \in \mathbb{N}\), and let \(s \in \mathbb{N}\). If \(C\) is a fixed-point set for \(F\) and \(s\), then \(C\) contains \(s\) and is closed under every \(f \in F\), and \(C \subseteq G\) for every set \(G \subseteq \mathbb{N}\) that contains \(s\) and is closed under every \(f \in F\).

theorem fixedPoint_isLeast {F : Finset (Nat → Nat)} {seed : Nat} {C : Set Nat}
    (hg : StrictGrowth F) (hC : FixedPoint F seed C) :
    SG F seed C ∧ ∀ G, SG F seed G → C ⊆ G

Uses 7

Statement usesFixed-point sets for a seed and generators · Self-generating sets · Strict growth of a set of generators

Proof usesSet generated from a seed · Under strict growth, a fixed-point set is the generated set · Fixed-point sets are self-generating · The generated set lies in every self-generating set

TheoremThe least self-generating set is the generated set#✓fully proved

Let \(F\) be a finite set of functions \(\mathbb{N} \to \mathbb{N}\) and let \(s \in \mathbb{N}\). Call a set \(G \subseteq \mathbb{N}\) self-generating if \(s \in G\) and \(f(x) \in G\) for every \(f \in F\) and every \(x \in G\). If \(C\) is self-generating and is contained in every self-generating set, then \(C\) equals the set generated from \(s\) by \(F\).

theorem isLeast_eq_generated {F : Finset (Nat → Nat)} {seed : Nat} {C : Set Nat}
    (hC : SG F seed C) (hle : ∀ G, SG F seed G → C ⊆ G) :
    C = GeneratedSet F seed

Uses 4

Statement usesSet generated from a seed · Self-generating sets

Proof usesThe generated set is self-generating · The generated set lies in every self-generating set

TheoremUnder strict growth, fixed-point sets are unique#✓fully proved

Let \(F\) be a finite set of functions \(\mathbb{N} \to \mathbb{N}\) with \(x < f(x)\) for every \(f \in F\) and every \(x \in \mathbb{N}\), and let \(s \in \mathbb{N}\). If \(C_1\) and \(C_2\) are both fixed-point sets for \(F\) and \(s\), then \(C_1 = C_2\).

theorem fixedPoint_unique {F : Finset (Nat → Nat)} {seed : Nat} {C1 C2 : Set Nat}
    (hg : StrictGrowth F) (h1 : FixedPoint F seed C1)
    (h2 : FixedPoint F seed C2) : C1 = C2

Uses 4

Statement usesFixed-point sets for a seed and generators · Strict growth of a set of generators

Proof usesSet generated from a seed · Under strict growth, a fixed-point set is the generated set

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.