PdlTestFree.SemiLinear

PdlTestFree
SemiLinear

Imports

module

public import Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
public import Mathlib.Tactic.Ring
public import Mathlib.LinearAlgebra.Dimension.Basic

public import Pdl.Semantics
public import Pdl.Vocab
public import PdlTestFree.Paths

@[expose] public section

Semilinearity of `L α` for programs over a single atomic program

For a test-free program α the set L α = {n | L α n} of possible execution lengths of α (see PdlTestFree.Paths) is semilinear (L_isSemilinearSet); no assumption on the vocabulary is needed for this.

Conversely, not every semilinear X ⊆ ℕ is L α for a test-free α with voc α = {a}: a test-free α always admits some positive number of steps (L_pos), so ∅ and {0} are not of this form, and if it admits 0 steps then it admits all multiples of some p > 0 (L_zero), so e.g. {0, 2} is not of this form either. These are the only obstructions: exists_L_eq_iff characterises the sets L α as the nonempty semilinear sets X such that 0 ∈ X implies k * p ∈ X for all k, for some p > 0.

open Set Pointwise AddSubmonoidopen scoped Finset

`L` of compound programs as set operations

lemma L_atom_set (c : ℕ) : {n | L (·c) n} = {1} := byc:ℕ⊢ {n | L (·c) n} = {1}
  ext nc:ℕn:ℕ⊢ n ∈ {n | L (·c) n} ↔ n ∈ {1}
  simp only [mem_ofPred_eq, L, mem_singleton_iff]All goals completed! 🐙lemma L_seq_set (α β : Program) : {n | L (α ;' β) n} = {n | L α n} + {n | L β n} := byα:Programβ:Program⊢ {n | L (α;'β) n} = {n | L α n} + {n | L β n}
  ext nα:Programβ:Programn:ℕ⊢ n ∈ {n | L (α;'β) n} ↔ n ∈ {n | L α n} + {n | L β n}
  simp only [mem_ofPred_eq, L, mem_add]α:Programβ:Programn:ℕ⊢ (∃ i j, L α i ∧ L β j ∧ n = i + j) ↔ ∃ x, L α x ∧ ∃ y, L β y ∧ x + y = n
  constructormpα:Programβ:Programn:ℕ⊢ (∃ i j, L α i ∧ L β j ∧ n = i + j) → ∃ x, L α x ∧ ∃ y, L β y ∧ x + y = nmprα:Programβ:Programn:ℕ⊢ (∃ x, L α x ∧ ∃ y, L β y ∧ x + y = n) → ∃ i j, L α i ∧ L β j ∧ n = i + j
  ·mpα:Programβ:Programn:ℕ⊢ (∃ i j, L α i ∧ L β j ∧ n = i + j) → ∃ x, L α x ∧ ∃ y, L β y ∧ x + y = n rintro ⟨i, j, hi, hj, rfl⟩mpα:Programβ:Programi:ℕj:ℕhi:L α ihj:L β j⊢ ∃ x, L α x ∧ ∃ y, L β y ∧ x + y = i + j; exact ⟨i, hi, j, hj, rfl⟩All goals completed! 🐙
  ·mprα:Programβ:Programn:ℕ⊢ (∃ x, L α x ∧ ∃ y, L β y ∧ x + y = n) → ∃ i j, L α i ∧ L β j ∧ n = i + j rintro ⟨i, hi, j, hj, rfl⟩mprα:Programβ:Programi:ℕhi:L α ij:ℕhj:L β j⊢ ∃ i_1 j_1, L α i_1 ∧ L β j_1 ∧ i + j = i_1 + j_1; exact ⟨i, j, hi, hj, rfl⟩All goals completed! 🐙lemma L_union_set (α β : Program) : {n | L (α ⋓ β) n} = {n | L α n} ∪ {n | L β n} := byα:Programβ:Program⊢ {n | L (α⋓β) n} = {n | L α n} ∪ {n | L β n}
  ext nα:Programβ:Programn:ℕ⊢ n ∈ {n | L (α⋓β) n} ↔ n ∈ {n | L α n} ∪ {n | L β n}
  simp only [mem_ofPred_eq, L, mem_union]All goals completed! 🐙lemma L_star_set (α : Program) : {n | L (∗α) n} = (closure {n | L α n} : Set ℕ) := byα:Program⊢ {n | L (∗α) n} = ↑(closure {n | L α n})
  ext nα:Programn:ℕ⊢ n ∈ {n | L (∗α) n} ↔ n ∈ ↑(closure {n | L α n})
  simp only [mem_ofPred_eq, L, SetLike.mem_coe]α:Programn:ℕ⊢ (∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum) ↔ n ∈ closure {n | L α n}
  constructormpα:Programn:ℕ⊢ (∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum) → n ∈ closure {n | L α n}mprα:Programn:ℕ⊢ n ∈ closure {n | L α n} → ∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum
  ·mpα:Programn:ℕ⊢ (∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum) → n ∈ closure {n | L α n} rintro ⟨l, hl, rfl⟩mpα:Programl:List ℕhl:∀ i ∈ l, L α i⊢ l.sum ∈ closure {n | L α n}
    exact list_sum_mem fun i hi => subset_closure (hl i hi)All goals completed! 🐙
  ·mprα:Programn:ℕ⊢ n ∈ closure {n | L α n} → ∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum intro hmprα:Programn:ℕh:n ∈ closure {n | L α n}⊢ ∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum
    obtain ⟨l, hl, rfl⟩ := exists_list_of_mem_closure hmprα:Programl:List ℕhl:∀ y ∈ l, y ∈ {n | L α n}h:l.sum ∈ closure {n | L α n}⊢ ∃ l_1, (∀ i ∈ l_1, L α i) ∧ l.sum = l_1.sum
    exact ⟨l, hl, rfl⟩All goals completed! 🐙

Every `L α` is semilinear

For any test-free program α the set L α is semilinear.

theorem L_isSemilinearSet : ∀ α : Program, α.testFree → IsSemilinearSet {n | L α n}
  | ?'_, hα =>a✝:Formulahα:(?'a✝).testFree⊢ IsSemilinearSet {n | L (?'a✝) n} bya✝:Formulahα:(?'a✝).testFree⊢ IsSemilinearSet {n | L (?'a✝) n} simp only [Program.testFree] at hαAll goals completed! 🐙
  | ·c, _ =>c:ℕx✝:(·c).testFree⊢ IsSemilinearSet {n | L (·c) n} byc:ℕx✝:(·c).testFree⊢ IsSemilinearSet {n | L (·c) n}
      rw [L_atom_setc:ℕx✝:(·c).testFree⊢ IsSemilinearSet {1}]c:ℕx✝:(·c).testFree⊢ IsSemilinearSet {1}
      simpAll goals completed! 🐙
  | α ;' β, hαβ =>α:Programβ:Programhαβ:(α;'β).testFree⊢ IsSemilinearSet {n | L (α;'β) n} byα:Programβ:Programhαβ:(α;'β).testFree⊢ IsSemilinearSet {n | L (α;'β) n}
      simp only [Program.testFree] at hαβα:Programβ:Programhαβ:α.testFree ∧ β.testFree⊢ IsSemilinearSet {n | L (α;'β) n}
      rw [L_seq_setα:Programβ:Programhαβ:α.testFree ∧ β.testFree⊢ IsSemilinearSet ({n | L α n} + {n | L β n})]α:Programβ:Programhαβ:α.testFree ∧ β.testFree⊢ IsSemilinearSet ({n | L α n} + {n | L β n})
      exact (L_isSemilinearSet α hαβ.1).add (L_isSemilinearSet β hαβ.2)All goals completed! 🐙
  | α ⋓ β, hαβ =>α:Programβ:Programhαβ:(α⋓β).testFree⊢ IsSemilinearSet {n | L (α⋓β) n} byα:Programβ:Programhαβ:(α⋓β).testFree⊢ IsSemilinearSet {n | L (α⋓β) n}
      simp only [Program.testFree] at hαβα:Programβ:Programhαβ:α.testFree ∧ β.testFree⊢ IsSemilinearSet {n | L (α⋓β) n}
      rw [L_union_setα:Programβ:Programhαβ:α.testFree ∧ β.testFree⊢ IsSemilinearSet ({n | L α n} ∪ {n | L β n})]α:Programβ:Programhαβ:α.testFree ∧ β.testFree⊢ IsSemilinearSet ({n | L α n} ∪ {n | L β n})
      exact (L_isSemilinearSet α hαβ.1).union (L_isSemilinearSet β hαβ.2)All goals completed! 🐙
  | ∗α, hα =>α:Programhα:(∗α).testFree⊢ IsSemilinearSet {n | L (∗α) n} byα:Programhα:(∗α).testFree⊢ IsSemilinearSet {n | L (∗α) n}
      simp only [Program.testFree] at hαα:Programhα:α.testFree⊢ IsSemilinearSet {n | L (∗α) n}
      rw [L_star_setα:Programhα:α.testFree⊢ IsSemilinearSet ↑(closure {n | L α n})]α:Programhα:α.testFree⊢ IsSemilinearSet ↑(closure {n | L α n})
      exact (L_isSemilinearSet α hα).closureAll goals completed! 🐙

Two obstructions to the converse

A test-free program admits some positive number of steps.

theorem L_pos : ∀ α : Program, α.testFree → ∃ n, 0 < n ∧ L α n
  | ?'_, hα =>a✝:Formulahα:(?'a✝).testFree⊢ ∃ n, 0 < n ∧ L (?'a✝) n bya✝:Formulahα:(?'a✝).testFree⊢ ∃ n, 0 < n ∧ L (?'a✝) n simp only [Program.testFree] at hαAll goals completed! 🐙
  | ·_, _ => ⟨1, one_pos, rfl⟩
  | α ;' β, hαβ =>α:Programβ:Programhαβ:(α;'β).testFree⊢ ∃ n, 0 < n ∧ L (α;'β) n byα:Programβ:Programhαβ:(α;'β).testFree⊢ ∃ n, 0 < n ∧ L (α;'β) n
      simp only [Program.testFree] at hαβα:Programβ:Programhαβ:α.testFree ∧ β.testFree⊢ ∃ n, 0 < n ∧ L (α;'β) n
      obtain ⟨i, hi, hLi⟩ := L_pos α hαβ.1α:Programβ:Programhαβ:α.testFree ∧ β.testFreei:ℕhi:0 < ihLi:L α i⊢ ∃ n, 0 < n ∧ L (α;'β) n
      obtain ⟨j, hj, hLj⟩ := L_pos β hαβ.2α:Programβ:Programhαβ:α.testFree ∧ β.testFreei:ℕhi:0 < ihLi:L α ij:ℕhj:0 < jhLj:L β j⊢ ∃ n, 0 < n ∧ L (α;'β) n
      exact ⟨i + j, byα:Programβ:Programhαβ:α.testFree ∧ β.testFreei:ℕhi:0 < ihLi:L α ij:ℕhj:0 < jhLj:L β j⊢ 0 < i + j omegaAll goals completed! 🐙, i, j, hLi, hLj, rfl⟩
  | α ⋓ β, hαβ =>α:Programβ:Programhαβ:(α⋓β).testFree⊢ ∃ n, 0 < n ∧ L (α⋓β) n byα:Programβ:Programhαβ:(α⋓β).testFree⊢ ∃ n, 0 < n ∧ L (α⋓β) n
      simp only [Program.testFree] at hαβα:Programβ:Programhαβ:α.testFree ∧ β.testFree⊢ ∃ n, 0 < n ∧ L (α⋓β) n
      obtain ⟨i, hi, hLi⟩ := L_pos α hαβ.1α:Programβ:Programhαβ:α.testFree ∧ β.testFreei:ℕhi:0 < ihLi:L α i⊢ ∃ n, 0 < n ∧ L (α⋓β) n
      exact ⟨i, hi, Or.inl hLi⟩All goals completed! 🐙
  | ∗α, hα =>α:Programhα:(∗α).testFree⊢ ∃ n, 0 < n ∧ L (∗α) n byα:Programhα:(∗α).testFree⊢ ∃ n, 0 < n ∧ L (∗α) n
      simp only [Program.testFree] at hαα:Programhα:α.testFree⊢ ∃ n, 0 < n ∧ L (∗α) n
      obtain ⟨i, hi, hLi⟩ := L_pos α hαα:Programhα:α.testFreei:ℕhi:0 < ihLi:L α i⊢ ∃ n, 0 < n ∧ L (∗α) n
      exact ⟨i, hi, [i], byα:Programhα:α.testFreei:ℕhi:0 < ihLi:L α i⊢ ∀ i_1 ∈ [i], L α i_1 simpaAll goals completed! 🐙, byα:Programhα:α.testFreei:ℕhi:0 < ihLi:L α i⊢ i = [i].sum simpAll goals completed! 🐙⟩

If a test-free program admits 0 steps, then it admits all multiples of some p > 0.

theorem L_zero : ∀ α : Program, α.testFree → L α 0 → ∃ p, 0 < p ∧ ∀ k, L α (k * p)
  | ?'_, hα, _ =>a✝:Formulahα:(?'a✝).testFreex✝:L (?'a✝) 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (?'a✝) (k * p) bya✝:Formulahα:(?'a✝).testFreex✝:L (?'a✝) 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (?'a✝) (k * p) simp only [Program.testFree] at hαAll goals completed! 🐙
  | ·c, _, h0 =>c:ℕx✝:(·c).testFreeh0:L (·c) 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (·c) (k * p) byc:ℕx✝:(·c).testFreeh0:L (·c) 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (·c) (k * p) simp [L] at h0All goals completed! 🐙
  | α ;' β, hαβ, h0 =>α:Programβ:Programhαβ:(α;'β).testFreeh0:L (α;'β) 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (α;'β) (k * p) byα:Programβ:Programhαβ:(α;'β).testFreeh0:L (α;'β) 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (α;'β) (k * p)
      simp only [Program.testFree] at hαβα:Programβ:Programhαβ:α.testFree ∧ β.testFreeh0:L (α;'β) 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (α;'β) (k * p)
      obtain ⟨i, j, hi, hj, hij⟩ := h0α:Programβ:Programhαβ:α.testFree ∧ β.testFreei:ℕj:ℕhi:L α ihj:L β jhij:0 = i + j⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (α;'β) (k * p)
      obtain ⟨rfl, rfl⟩ : i = 0 ∧ j = 0 := byα:Programβ:Programhαβ:α.testFree ∧ β.testFreei:ℕj:ℕhi:L α ihj:L β jhij:0 = i + j⊢ i = 0 ∧ j = 0 omegaα:Programβ:Programhαβ:α.testFree ∧ β.testFreehi:L α 0hj:L β 0hij:0 = 0 + 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (α;'β) (k * p)
      obtain ⟨p, hp, hLp⟩ := L_zero α hαβ.1 hiα:Programβ:Programhαβ:α.testFree ∧ β.testFreehi:L α 0hj:L β 0hij:0 = 0 + 0p:ℕhp:0 < phLp:∀ (k : ℕ), L α (k * p)⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (α;'β) (k * p)
      exact ⟨p, hp, fun k => ⟨k * p, 0, hLp k, hj, byα:Programβ:Programhαβ:α.testFree ∧ β.testFreehi:L α 0hj:L β 0hij:0 = 0 + 0p:ℕhp:0 < phLp:∀ (k : ℕ), L α (k * p)k:ℕ⊢ k * p = k * p + 0 simpAll goals completed! 🐙⟩⟩
  | α ⋓ β, hαβ, h0 =>α:Programβ:Programhαβ:(α⋓β).testFreeh0:L (α⋓β) 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (α⋓β) (k * p) byα:Programβ:Programhαβ:(α⋓β).testFreeh0:L (α⋓β) 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (α⋓β) (k * p)
      simp only [Program.testFree] at hαβα:Programβ:Programhαβ:α.testFree ∧ β.testFreeh0:L (α⋓β) 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (α⋓β) (k * p)
      rcases h0 with h0 | h0inlα:Programβ:Programhαβ:α.testFree ∧ β.testFreeh0:L α 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (α⋓β) (k * p)inrα:Programβ:Programhαβ:α.testFree ∧ β.testFreeh0:L β 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (α⋓β) (k * p)
      ·inlα:Programβ:Programhαβ:α.testFree ∧ β.testFreeh0:L α 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (α⋓β) (k * p) obtain ⟨p, hp, hLp⟩ := L_zero α hαβ.1 h0inlα:Programβ:Programhαβ:α.testFree ∧ β.testFreeh0:L α 0p:ℕhp:0 < phLp:∀ (k : ℕ), L α (k * p)⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (α⋓β) (k * p)
        exact ⟨p, hp, fun k => Or.inl (hLp k)⟩All goals completed! 🐙
      ·inrα:Programβ:Programhαβ:α.testFree ∧ β.testFreeh0:L β 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (α⋓β) (k * p) obtain ⟨p, hp, hLp⟩ := L_zero β hαβ.2 h0inrα:Programβ:Programhαβ:α.testFree ∧ β.testFreeh0:L β 0p:ℕhp:0 < phLp:∀ (k : ℕ), L β (k * p)⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (α⋓β) (k * p)
        exact ⟨p, hp, fun k => Or.inr (hLp k)⟩All goals completed! 🐙
  | ∗α, hα, _ =>α:Programhα:(∗α).testFreex✝:L (∗α) 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (∗α) (k * p) byα:Programhα:(∗α).testFreex✝:L (∗α) 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (∗α) (k * p)
      simp only [Program.testFree] at hαα:Programhα:α.testFreex✝:L (∗α) 0⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (∗α) (k * p)
      obtain ⟨p, hp, hLp⟩ := L_pos α hαα:Programhα:α.testFreex✝:L (∗α) 0p:ℕhp:0 < phLp:L α p⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), L (∗α) (k * p)
      refine ⟨p, hp, fun k => ⟨List.replicate k p, ?_, byα:Programhα:α.testFreex✝:L (∗α) 0p:ℕhp:0 < phLp:L α pk:ℕ⊢ k * p = (List.replicate k p).sum simpAll goals completed! 🐙⟩⟩
      intro i hiα:Programhα:α.testFreex✝:L (∗α) 0p:ℕhp:0 < phLp:L α pk:ℕi:ℕhi:i ∈ List.replicate k p⊢ L α i
      rw [List.eq_of_mem_replicate hiα:Programhα:α.testFreex✝:L (∗α) 0p:ℕhp:0 < phLp:L α pk:ℕi:ℕhi:i ∈ List.replicate k p⊢ L α p]α:Programhα:α.testFreex✝:L (∗α) 0p:ℕhp:0 < phLp:L α pk:ℕi:ℕhi:i ∈ List.replicate k p⊢ L α p
      exact hLpAll goals completed! 🐙

The converse, for the sets without these obstructions

aPow n is the program a^(n+1), i.e. a ;' ⋯ ;' a with n + 1 copies of a = ·0.

def aPow : ℕ → Program
  | 0 => ·0
  | n + 1 => ·0 ;' aPow n

@[simp] lemma L_aPow (n m : ℕ) : L (aPow n) m ↔ m = n + 1 := byn:ℕm:ℕ⊢ L (aPow n) m ↔ m = n + 1
  induction n generalizing m with
  | zero =>zerom:ℕ⊢ L (aPow 0) m ↔ m = 0 + 1 simp [aPow, L]All goals completed! 🐙
  | succ n IH =>succn:ℕIH:∀ (m : ℕ), L (aPow n) m ↔ m = n + 1m:ℕ⊢ L (aPow (n + 1)) m ↔ m = n + 1 + 1
      simp only [aPow, L, IH]succn:ℕIH:∀ (m : ℕ), L (aPow n) m ↔ m = n + 1m:ℕ⊢ (∃ i j, i = 1 ∧ j = n + 1 ∧ m = i + j) ↔ m = n + 1 + 1
      constructorsucc.mpn:ℕIH:∀ (m : ℕ), L (aPow n) m ↔ m = n + 1m:ℕ⊢ (∃ i j, i = 1 ∧ j = n + 1 ∧ m = i + j) → m = n + 1 + 1succ.mprn:ℕIH:∀ (m : ℕ), L (aPow n) m ↔ m = n + 1m:ℕ⊢ m = n + 1 + 1 → ∃ i j, i = 1 ∧ j = n + 1 ∧ m = i + j
      ·succ.mpn:ℕIH:∀ (m : ℕ), L (aPow n) m ↔ m = n + 1m:ℕ⊢ (∃ i j, i = 1 ∧ j = n + 1 ∧ m = i + j) → m = n + 1 + 1 rintro ⟨i, j, rfl, rfl, rfl⟩succ.mpn:ℕIH:∀ (m : ℕ), L (aPow n) m ↔ m = n + 1⊢ 1 + (n + 1) = n + 1 + 1; ringAll goals completed! 🐙
      ·succ.mprn:ℕIH:∀ (m : ℕ), L (aPow n) m ↔ m = n + 1m:ℕ⊢ m = n + 1 + 1 → ∃ i j, i = 1 ∧ j = n + 1 ∧ m = i + j rintro rflsucc.mprn:ℕIH:∀ (m : ℕ), L (aPow n) m ↔ m = n + 1⊢ ∃ i j, i = 1 ∧ j = n + 1 ∧ n + 1 + 1 = i + j; exact ⟨1, n + 1, rfl, rfl, byn:ℕIH:∀ (m : ℕ), L (aPow n) m ↔ m = n + 1⊢ n + 1 + 1 = 1 + (n + 1) ringAll goals completed! 🐙⟩lemma aPow_testFree (n : ℕ) : (aPow n).testFree := byn:ℕ⊢ (aPow n).testFree
  induction nzero⊢ (aPow 0).testFreesuccn✝:ℕa✝:(aPow n✝).testFree⊢ (aPow (n✝ + 1)).testFree <;>zero⊢ (aPow 0).testFreesuccn✝:ℕa✝:(aPow n✝).testFree⊢ (aPow (n✝ + 1)).testFree simp [aPow, *]All goals completed! 🐙lemma aPow_voc (n : ℕ) : (aPow n).voc = {Sum.inr 0} := byn:ℕ⊢ (aPow n).voc = {Sum.inr 0}
  induction nzero⊢ (aPow 0).voc = {Sum.inr 0}succn✝:ℕa✝:(aPow n✝).voc = {Sum.inr 0}⊢ (aPow (n✝ + 1)).voc = {Sum.inr 0} <;>zero⊢ (aPow 0).voc = {Sum.inr 0}succn✝:ℕa✝:(aPow n✝).voc = {Sum.inr 0}⊢ (aPow (n✝ + 1)).voc = {Sum.inr 0} simp [aPow, *]All goals completed! 🐙

IsL X: the set X ⊆ ℕ is L α for a test-free program α with voc α = {a}.

def IsL (X : Set ℕ) : Prop :=
  ∃ α : Program, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X

lemma IsL.union {X Y : Set ℕ} (hX : IsL X) (hY : IsL Y) : IsL (X ∪ Y) := byX:Set ℕY:Set ℕhX:IsL XhY:IsL Y⊢ IsL (X ∪ Y)
  obtain ⟨α, hα, hvα, rfl⟩ := hXY:Set ℕhY:IsL Yα:Programhα:α.testFreehvα:α.voc = {Sum.inr 0}⊢ IsL ({n | L α n} ∪ Y)
  obtain ⟨β, hβ, hvβ, rfl⟩ := hYα:Programhα:α.testFreehvα:α.voc = {Sum.inr 0}β:Programhβ:β.testFreehvβ:β.voc = {Sum.inr 0}⊢ IsL ({n | L α n} ∪ {n | L β n})
  exact ⟨α ⋓ β, ⟨hα, hβ⟩, byα:Programhα:α.testFreehvα:α.voc = {Sum.inr 0}β:Programhβ:β.testFreehvβ:β.voc = {Sum.inr 0}⊢ (α⋓β).voc = {Sum.inr 0} simp [hvα, hvβ]All goals completed! 🐙, L_union_set α β⟩lemma IsL.add {X Y : Set ℕ} (hX : IsL X) (hY : IsL Y) : IsL (X + Y) := byX:Set ℕY:Set ℕhX:IsL XhY:IsL Y⊢ IsL (X + Y)
  obtain ⟨α, hα, hvα, rfl⟩ := hXY:Set ℕhY:IsL Yα:Programhα:α.testFreehvα:α.voc = {Sum.inr 0}⊢ IsL ({n | L α n} + Y)
  obtain ⟨β, hβ, hvβ, rfl⟩ := hYα:Programhα:α.testFreehvα:α.voc = {Sum.inr 0}β:Programhβ:β.testFreehvβ:β.voc = {Sum.inr 0}⊢ IsL ({n | L α n} + {n | L β n})
  exact ⟨α ;' β, ⟨hα, hβ⟩, byα:Programhα:α.testFreehvα:α.voc = {Sum.inr 0}β:Programhβ:β.testFreehvβ:β.voc = {Sum.inr 0}⊢ (α;'β).voc = {Sum.inr 0} simp [hvα, hvβ]All goals completed! 🐙, L_seq_set α β⟩lemma IsL.closure {X : Set ℕ} (hX : IsL X) : IsL (closure X : Set ℕ) := byX:Set ℕhX:IsL X⊢ IsL ↑(AddSubmonoid.closure X)
  obtain ⟨α, hα, hvα, rfl⟩ := hXα:Programhα:α.testFreehvα:α.voc = {Sum.inr 0}⊢ IsL ↑(AddSubmonoid.closure {n | L α n})
  exact ⟨∗α, hα, byα:Programhα:α.testFreehvα:α.voc = {Sum.inr 0}⊢ (∗α).voc = {Sum.inr 0} simp [hvα]All goals completed! 🐙, L_star_set α⟩lemma IsL.singleton_succ (n : ℕ) : IsL {n + 1} :=
  ⟨aPow n, aPow_testFree n, aPow_voc n, byn:ℕ⊢ {n_1 | L (aPow n) n_1} = {n + 1} ext mn:ℕm:ℕ⊢ m ∈ {n_1 | L (aPow n) n_1} ↔ m ∈ {n + 1}; simpAll goals completed! 🐙⟩lemma IsL.singleton_of_pos {n : ℕ} (hn : 0 < n) : IsL {n} := byn:ℕhn:0 < n⊢ IsL {n}
  obtain ⟨m, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn.ne'm:ℕhn:0 < m + 1⊢ IsL {m + 1}
  exact IsL.singleton_succ mAll goals completed! 🐙

The positive part of a proper linear subset of ℕ is empty or IsL.

lemma IsProperLinearSet.isL_diff_zero {s : Set ℕ} (hs : IsProperLinearSet s) :
    s \ {0} = ∅ ∨ IsL (s \ {0}) := bys:Set ℕhs:IsProperLinearSet s⊢ s \ {0} = ∅ ∨ IsL (s \ {0})
  rw [isProperLinearSet_iffs:Set ℕhs:∃ a t, LinearIndepOn ℕ id ↑t ∧ s = a +ᵥ ↑(closure ↑t)⊢ s \ {0} = ∅ ∨ IsL (s \ {0})] at hss:Set ℕhs:∃ a t, LinearIndepOn ℕ id ↑t ∧ s = a +ᵥ ↑(closure ↑t)⊢ s \ {0} = ∅ ∨ IsL (s \ {0})
  obtain ⟨a, t, ht, rfl⟩ := hsa:ℕt:Finset ℕht:LinearIndepOn ℕ id ↑t⊢ (a +ᵥ ↑(closure ↑t)) \ {0} = ∅ ∨ IsL ((a +ᵥ ↑(closure ↑t)) \ {0})
  have hcard : #t ≤ 1 := bys:Set ℕhs:IsProperLinearSet s⊢ s \ {0} = ∅ ∨ IsL (s \ {0}) simpa [CommSemiring.rank_self] using ht.cardinal_le_ranka:ℕt:Finset ℕht:LinearIndepOn ℕ id ↑thcard:#t ≤ 1⊢ (a +ᵥ ↑(closure ↑t)) \ {0} = ∅ ∨ IsL ((a +ᵥ ↑(closure ↑t)) \ {0})
  simp_rw [a:ℕt:Finset ℕht:LinearIndepOn ℕ id ↑thcard:#t ≤ 1⊢ (a +ᵥ ↑(closure ↑t)) \ {0} = ∅ ∨ IsL ((a +ᵥ ↑(closure ↑t)) \ {0})Finset.card_le_one_iff_subset_singleton,a:ℕt:Finset ℕht:LinearIndepOn ℕ id ↑thcard:∃ x, t ⊆ {x}⊢ (a +ᵥ ↑(closure ↑t)) \ {0} = ∅ ∨ IsL ((a +ᵥ ↑(closure ↑t)) \ {0}) Finset.subset_singleton_iffa:ℕt:Finset ℕht:LinearIndepOn ℕ id ↑thcard:∃ x, t = ∅ ∨ t = {x}⊢ (a +ᵥ ↑(closure ↑t)) \ {0} = ∅ ∨ IsL ((a +ᵥ ↑(closure ↑t)) \ {0})] at hcard
  rcases hcard with ⟨b, (rfl | rfl)⟩inla:ℕb:ℕht:LinearIndepOn ℕ id ↑∅⊢ (a +ᵥ ↑(closure ↑∅)) \ {0} = ∅ ∨ IsL ((a +ᵥ ↑(closure ↑∅)) \ {0})inra:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}⊢ (a +ᵥ ↑(closure ↑{b})) \ {0} = ∅ ∨ IsL ((a +ᵥ ↑(closure ↑{b})) \ {0})
  ·inla:ℕb:ℕht:LinearIndepOn ℕ id ↑∅⊢ (a +ᵥ ↑(closure ↑∅)) \ {0} = ∅ ∨ IsL ((a +ᵥ ↑(closure ↑∅)) \ {0}) -- `s = {a}`
    have hs : a +ᵥ (closure ((∅ : Finset ℕ) : Set ℕ) : Set ℕ) = {a} := bys:Set ℕhs:IsProperLinearSet s⊢ s \ {0} = ∅ ∨ IsL (s \ {0})
      ext na:ℕb:ℕht:LinearIndepOn ℕ id ↑∅n:ℕ⊢ n ∈ a +ᵥ ↑(closure ↑∅) ↔ n ∈ {a}; simpinla:ℕb:ℕht:LinearIndepOn ℕ id ↑∅hs:a +ᵥ ↑(closure ↑∅) = {a}⊢ (a +ᵥ ↑(closure ↑∅)) \ {0} = ∅ ∨ IsL ((a +ᵥ ↑(closure ↑∅)) \ {0})
    rw [hsinla:ℕb:ℕht:LinearIndepOn ℕ id ↑∅hs:a +ᵥ ↑(closure ↑∅) = {a}⊢ {a} \ {0} = ∅ ∨ IsL ({a} \ {0})]inla:ℕb:ℕht:LinearIndepOn ℕ id ↑∅hs:a +ᵥ ↑(closure ↑∅) = {a}⊢ {a} \ {0} = ∅ ∨ IsL ({a} \ {0})
    rcases Nat.eq_zero_or_pos a with rfl | hainl.inlb:ℕht:LinearIndepOn ℕ id ↑∅hs:0 +ᵥ ↑(closure ↑∅) = {0}⊢ {0} \ {0} = ∅ ∨ IsL ({0} \ {0})inl.inra:ℕb:ℕht:LinearIndepOn ℕ id ↑∅hs:a +ᵥ ↑(closure ↑∅) = {a}ha:a > 0⊢ {a} \ {0} = ∅ ∨ IsL ({a} \ {0})
    ·inl.inlb:ℕht:LinearIndepOn ℕ id ↑∅hs:0 +ᵥ ↑(closure ↑∅) = {0}⊢ {0} \ {0} = ∅ ∨ IsL ({0} \ {0}) leftinl.inlb:ℕht:LinearIndepOn ℕ id ↑∅hs:0 +ᵥ ↑(closure ↑∅) = {0}⊢ {0} \ {0} = ∅; simpAll goals completed! 🐙
    ·inl.inra:ℕb:ℕht:LinearIndepOn ℕ id ↑∅hs:a +ᵥ ↑(closure ↑∅) = {a}ha:a > 0⊢ {a} \ {0} = ∅ ∨ IsL ({a} \ {0}) rightinl.inra:ℕb:ℕht:LinearIndepOn ℕ id ↑∅hs:a +ᵥ ↑(closure ↑∅) = {a}ha:a > 0⊢ IsL ({a} \ {0})
      rw [sdiff_singleton_eq_self (bya:ℕb:ℕht:LinearIndepOn ℕ id ↑∅hs:a +ᵥ ↑(closure ↑∅) = {a}ha:a > 0⊢ 0 ∉ {a} simpa using ha.neAll goals completed! 🐙)]inl.inra:ℕb:ℕht:LinearIndepOn ℕ id ↑∅hs:a +ᵥ ↑(closure ↑∅) = {a}ha:a > 0⊢ IsL {a}
      exact IsL.singleton_of_pos haAll goals completed! 🐙
  ·inra:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}⊢ (a +ᵥ ↑(closure ↑{b})) \ {0} = ∅ ∨ IsL ((a +ᵥ ↑(closure ↑{b})) \ {0}) -- `s = a + bℕ` with `b ≠ 0`
    have hb : b ≠ 0 := bys:Set ℕhs:IsProperLinearSet s⊢ s \ {0} = ∅ ∨ IsL (s \ {0}) simpa [ne_comm] using ht.zero_notMem_imageinra:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0⊢ (a +ᵥ ↑(closure ↑{b})) \ {0} = ∅ ∨ IsL ((a +ᵥ ↑(closure ↑{b})) \ {0})
    have hb' : 0 < b := Nat.pos_of_ne_zero hbinra:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < b⊢ (a +ᵥ ↑(closure ↑{b})) \ {0} = ∅ ∨ IsL ((a +ᵥ ↑(closure ↑{b})) \ {0})
    rightinra:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < b⊢ IsL ((a +ᵥ ↑(closure ↑{b})) \ {0})
    have hmem : ∀ n,
        n ∈ a +ᵥ (closure (({b} : Finset ℕ) : Set ℕ) : Set ℕ) ↔ ∃ m, a + m * b = n := bys:Set ℕhs:IsProperLinearSet s⊢ s \ {0} = ∅ ∨ IsL (s \ {0})
      intro na:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bn:ℕ⊢ n ∈ a +ᵥ ↑(closure ↑{b}) ↔ ∃ m, a + m * b = n
      simp only [Finset.coe_singleton, mem_vadd_set, SetLike.mem_coe,
        AddSubmonoid.mem_closure_singleton, smul_eq_mul, vadd_eq_add, exists_exists_eq_and]inra:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ a +ᵥ ↑(closure ↑{b}) ↔ ∃ m, a + m * b = n⊢ IsL ((a +ᵥ ↑(closure ↑{b})) \ {0})
    rcases Nat.eq_zero_or_pos a with rfl | hainr.inlb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{b}) ↔ ∃ m, 0 + m * b = n⊢ IsL ((0 +ᵥ ↑(closure ↑{b})) \ {0})inr.inra:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ a +ᵥ ↑(closure ↑{b}) ↔ ∃ m, a + m * b = nha:a > 0⊢ IsL ((a +ᵥ ↑(closure ↑{b})) \ {0})
    ·inr.inlb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{b}) ↔ ∃ m, 0 + m * b = n⊢ IsL ((0 +ᵥ ↑(closure ↑{b})) \ {0}) -- `bℕ \ {0} = {b} + bℕ`
      convert (IsL.singleton_of_pos hb').add (IsL.singleton_of_pos hb').closure using 1b:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{b}) ↔ ∃ m, 0 + m * b = n⊢ (0 +ᵥ ↑(closure ↑{b})) \ {0} = {b} + ↑(closure {b})
      ext nb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{b}) ↔ ∃ m, 0 + m * b = nn:ℕ⊢ n ∈ (0 +ᵥ ↑(closure ↑{b})) \ {0} ↔ n ∈ {b} + ↑(closure {b})
      simp only [mem_sdiff, hmem, mem_singleton_iff, mem_add, SetLike.mem_coe,
        AddSubmonoid.mem_closure_singleton, smul_eq_mul, zero_add]b:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{b}) ↔ ∃ m, 0 + m * b = nn:ℕ⊢ (∃ m, m * b = n) ∧ ¬n = 0 ↔ ∃ x, x = b ∧ ∃ y, (∃ n, n * b = y) ∧ x + y = n
      constructormpb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{b}) ↔ ∃ m, 0 + m * b = nn:ℕ⊢ (∃ m, m * b = n) ∧ ¬n = 0 → ∃ x, x = b ∧ ∃ y, (∃ n, n * b = y) ∧ x + y = nmprb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{b}) ↔ ∃ m, 0 + m * b = nn:ℕ⊢ (∃ x, x = b ∧ ∃ y, (∃ n, n * b = y) ∧ x + y = n) → (∃ m, m * b = n) ∧ ¬n = 0
      ·mpb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{b}) ↔ ∃ m, 0 + m * b = nn:ℕ⊢ (∃ m, m * b = n) ∧ ¬n = 0 → ∃ x, x = b ∧ ∃ y, (∃ n, n * b = y) ∧ x + y = n rintro ⟨⟨m, rfl⟩, hm⟩mpb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{b}) ↔ ∃ m, 0 + m * b = nm:ℕhm:¬m * b = 0⊢ ∃ x, x = b ∧ ∃ y, (∃ n, n * b = y) ∧ x + y = m * b
        obtain ⟨m, rfl⟩ : ∃ m', m = m' + 1 :=
          Nat.exists_eq_add_one_of_ne_zero (byb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{b}) ↔ ∃ m, 0 + m * b = nm:ℕhm:¬m * b = 0⊢ m ≠ 0 rintro rflb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{b}) ↔ ∃ m, 0 + m * b = nhm:¬0 * b = 0⊢ False; simp at hmAll goals completed! 🐙)mpb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{b}) ↔ ∃ m, 0 + m * b = nm:ℕhm:¬(m + 1) * b = 0⊢ ∃ x, x = b ∧ ∃ y, (∃ n, n * b = y) ∧ x + y = (m + 1) * b
        exact ⟨b, rfl, m * b, ⟨m, rfl⟩, byb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{b}) ↔ ∃ m, 0 + m * b = nm:ℕhm:¬(m + 1) * b = 0⊢ b + m * b = (m + 1) * b ringAll goals completed! 🐙⟩
      ·mprb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{b}) ↔ ∃ m, 0 + m * b = nn:ℕ⊢ (∃ x, x = b ∧ ∃ y, (∃ n, n * b = y) ∧ x + y = n) → (∃ m, m * b = n) ∧ ¬n = 0 rintro ⟨x, rfl, y, ⟨m, rfl⟩, rfl⟩mprx:ℕht:LinearIndepOn ℕ id ↑{x}hb:x ≠ 0hb':0 < xhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{x}) ↔ ∃ m, 0 + m * x = nm:ℕ⊢ (∃ m_1, m_1 * x = x + m * x) ∧ ¬x + m * x = 0
        exact ⟨⟨m + 1, byx:ℕht:LinearIndepOn ℕ id ↑{x}hb:x ≠ 0hb':0 < xhmem:∀ (n : ℕ), n ∈ 0 +ᵥ ↑(closure ↑{x}) ↔ ∃ m, 0 + m * x = nm:ℕ⊢ (m + 1) * x = x + m * x ringAll goals completed! 🐙⟩, (Nat.add_pos_left hb' _).ne'⟩
    ·inr.inra:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ a +ᵥ ↑(closure ↑{b}) ↔ ∃ m, a + m * b = nha:a > 0⊢ IsL ((a +ᵥ ↑(closure ↑{b})) \ {0}) -- `(a + bℕ) \ {0} = {a} + bℕ`
      convert (IsL.singleton_of_pos ha).add (IsL.singleton_of_pos hb').closure using 1a:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ a +ᵥ ↑(closure ↑{b}) ↔ ∃ m, a + m * b = nha:a > 0⊢ (a +ᵥ ↑(closure ↑{b})) \ {0} = {a} + ↑(closure {b})
      ext na:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ a +ᵥ ↑(closure ↑{b}) ↔ ∃ m, a + m * b = nha:a > 0n:ℕ⊢ n ∈ (a +ᵥ ↑(closure ↑{b})) \ {0} ↔ n ∈ {a} + ↑(closure {b})
      simp only [mem_sdiff, hmem, mem_singleton_iff, mem_add, SetLike.mem_coe,
        AddSubmonoid.mem_closure_singleton, smul_eq_mul]a:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ a +ᵥ ↑(closure ↑{b}) ↔ ∃ m, a + m * b = nha:a > 0n:ℕ⊢ (∃ m, a + m * b = n) ∧ ¬n = 0 ↔ ∃ x, x = a ∧ ∃ y, (∃ n, n * b = y) ∧ x + y = n
      constructormpa:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ a +ᵥ ↑(closure ↑{b}) ↔ ∃ m, a + m * b = nha:a > 0n:ℕ⊢ (∃ m, a + m * b = n) ∧ ¬n = 0 → ∃ x, x = a ∧ ∃ y, (∃ n, n * b = y) ∧ x + y = nmpra:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ a +ᵥ ↑(closure ↑{b}) ↔ ∃ m, a + m * b = nha:a > 0n:ℕ⊢ (∃ x, x = a ∧ ∃ y, (∃ n, n * b = y) ∧ x + y = n) → (∃ m, a + m * b = n) ∧ ¬n = 0
      ·mpa:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ a +ᵥ ↑(closure ↑{b}) ↔ ∃ m, a + m * b = nha:a > 0n:ℕ⊢ (∃ m, a + m * b = n) ∧ ¬n = 0 → ∃ x, x = a ∧ ∃ y, (∃ n, n * b = y) ∧ x + y = n rintro ⟨⟨m, rfl⟩, -⟩mpa:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ a +ᵥ ↑(closure ↑{b}) ↔ ∃ m, a + m * b = nha:a > 0m:ℕ⊢ ∃ x, x = a ∧ ∃ y, (∃ n, n * b = y) ∧ x + y = a + m * b
        exact ⟨a, rfl, m * b, ⟨m, rfl⟩, rfl⟩All goals completed! 🐙
      ·mpra:ℕb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bhmem:∀ (n : ℕ), n ∈ a +ᵥ ↑(closure ↑{b}) ↔ ∃ m, a + m * b = nha:a > 0n:ℕ⊢ (∃ x, x = a ∧ ∃ y, (∃ n, n * b = y) ∧ x + y = n) → (∃ m, a + m * b = n) ∧ ¬n = 0 rintro ⟨x, rfl, y, ⟨m, rfl⟩, rfl⟩mprb:ℕht:LinearIndepOn ℕ id ↑{b}hb:b ≠ 0hb':0 < bx:ℕhmem:∀ (n : ℕ), n ∈ x +ᵥ ↑(closure ↑{b}) ↔ ∃ m, x + m * b = nha:x > 0m:ℕ⊢ (∃ m_1, x + m_1 * b = x + m * b) ∧ ¬x + m * b = 0
        exact ⟨⟨m, rfl⟩, (Nat.add_pos_left ha _).ne'⟩All goals completed! 🐙

The positive part of a semilinear subset of ℕ is empty or IsL.

lemma IsSemilinearSet.isL_diff_zero {X : Set ℕ} (hX : IsSemilinearSet X) :
    X \ {0} = ∅ ∨ IsL (X \ {0}) := byX:Set ℕhX:IsSemilinearSet X⊢ X \ {0} = ∅ ∨ IsL (X \ {0})
  obtain ⟨S, hS, rfl⟩ := isProperSemilinearSet_iff.mp hX.isProperSemilinearSetS:Finset (Set ℕ)hS:∀ t ∈ S, IsProperLinearSet thX:IsSemilinearSet (⋃₀ ↑S)⊢ ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})
  clear hXS:Finset (Set ℕ)hS:∀ t ∈ S, IsProperLinearSet t⊢ ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})
  induction S using Finset.induction_on with
  | empty =>emptyhS:∀ t ∈ ∅, IsProperLinearSet t⊢ ⋃₀ ↑∅ \ {0} = ∅ ∨ IsL (⋃₀ ↑∅ \ {0}) leftemptyhS:∀ t ∈ ∅, IsProperLinearSet t⊢ ⋃₀ ↑∅ \ {0} = ∅; simpAll goals completed! 🐙
  | insert t S _ IH =>insertt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:∀ t_1 ∈ insert t S, IsProperLinearSet t_1⊢ ⋃₀ ↑(insert t S) \ {0} = ∅ ∨ IsL (⋃₀ ↑(insert t S) \ {0})
      simp only [Finset.mem_insert, forall_eq_or_imp] at hSinsertt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet a⊢ ⋃₀ ↑(insert t S) \ {0} = ∅ ∨ IsL (⋃₀ ↑(insert t S) \ {0})
      rw [Finset.coe_insert,insertt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet a⊢ ⋃₀ insert t ↑S \ {0} = ∅ ∨ IsL (⋃₀ insert t ↑S \ {0}) sUnion_insert,insertt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet a⊢ (t ∪ ⋃₀ ↑S) \ {0} = ∅ ∨ IsL ((t ∪ ⋃₀ ↑S) \ {0}) union_sdiff_distribinsertt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet a⊢ t \ {0} ∪ ⋃₀ ↑S \ {0} = ∅ ∨ IsL (t \ {0} ∪ ⋃₀ ↑S \ {0})]insertt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet a⊢ t \ {0} ∪ ⋃₀ ↑S \ {0} = ∅ ∨ IsL (t \ {0} ∪ ⋃₀ ↑S \ {0})
      rcases hS.1.isL_diff_zero with h1 | h1insert.inlt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:t \ {0} = ∅⊢ t \ {0} ∪ ⋃₀ ↑S \ {0} = ∅ ∨ IsL (t \ {0} ∪ ⋃₀ ↑S \ {0})insert.inrt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:IsL (t \ {0})⊢ t \ {0} ∪ ⋃₀ ↑S \ {0} = ∅ ∨ IsL (t \ {0} ∪ ⋃₀ ↑S \ {0}) <;>insert.inlt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:t \ {0} = ∅⊢ t \ {0} ∪ ⋃₀ ↑S \ {0} = ∅ ∨ IsL (t \ {0} ∪ ⋃₀ ↑S \ {0})insert.inrt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:IsL (t \ {0})⊢ t \ {0} ∪ ⋃₀ ↑S \ {0} = ∅ ∨ IsL (t \ {0} ∪ ⋃₀ ↑S \ {0}) rcases IH hS.2 with h2 | h2insert.inr.inlt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:IsL (t \ {0})h2:⋃₀ ↑S \ {0} = ∅⊢ t \ {0} ∪ ⋃₀ ↑S \ {0} = ∅ ∨ IsL (t \ {0} ∪ ⋃₀ ↑S \ {0})insert.inr.inrt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:IsL (t \ {0})h2:IsL (⋃₀ ↑S \ {0})⊢ t \ {0} ∪ ⋃₀ ↑S \ {0} = ∅ ∨ IsL (t \ {0} ∪ ⋃₀ ↑S \ {0})
      ·insert.inl.inlt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:t \ {0} = ∅h2:⋃₀ ↑S \ {0} = ∅⊢ t \ {0} ∪ ⋃₀ ↑S \ {0} = ∅ ∨ IsL (t \ {0} ∪ ⋃₀ ↑S \ {0}) leftinsert.inl.inlt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:t \ {0} = ∅h2:⋃₀ ↑S \ {0} = ∅⊢ t \ {0} ∪ ⋃₀ ↑S \ {0} = ∅; rw [h1,insert.inl.inlt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:t \ {0} = ∅h2:⋃₀ ↑S \ {0} = ∅⊢ ∅ ∪ ⋃₀ ↑S \ {0} = ∅ h2,insert.inl.inlt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:t \ {0} = ∅h2:⋃₀ ↑S \ {0} = ∅⊢ ∅ ∪ ∅ = ∅ union_emptyinsert.inl.inlt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:t \ {0} = ∅h2:⋃₀ ↑S \ {0} = ∅⊢ ∅ = ∅]All goals completed! 🐙
      ·insert.inl.inrt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:t \ {0} = ∅h2:IsL (⋃₀ ↑S \ {0})⊢ t \ {0} ∪ ⋃₀ ↑S \ {0} = ∅ ∨ IsL (t \ {0} ∪ ⋃₀ ↑S \ {0}) rightinsert.inl.inrt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:t \ {0} = ∅h2:IsL (⋃₀ ↑S \ {0})⊢ IsL (t \ {0} ∪ ⋃₀ ↑S \ {0}); rwa [h1, empty_union]All goals completed! 🐙
      ·insert.inr.inlt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:IsL (t \ {0})h2:⋃₀ ↑S \ {0} = ∅⊢ t \ {0} ∪ ⋃₀ ↑S \ {0} = ∅ ∨ IsL (t \ {0} ∪ ⋃₀ ↑S \ {0}) rightinsert.inr.inlt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:IsL (t \ {0})h2:⋃₀ ↑S \ {0} = ∅⊢ IsL (t \ {0} ∪ ⋃₀ ↑S \ {0}); rwa [h2, union_empty]All goals completed! 🐙
      ·insert.inr.inrt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:IsL (t \ {0})h2:IsL (⋃₀ ↑S \ {0})⊢ t \ {0} ∪ ⋃₀ ↑S \ {0} = ∅ ∨ IsL (t \ {0} ∪ ⋃₀ ↑S \ {0}) rightinsert.inr.inrt:Set ℕS:Finset (Set ℕ)a✝:t ∉ SIH:(∀ t ∈ S, IsProperLinearSet t) → ⋃₀ ↑S \ {0} = ∅ ∨ IsL (⋃₀ ↑S \ {0})hS:IsProperLinearSet t ∧ ∀ a ∈ S, IsProperLinearSet ah1:IsL (t \ {0})h2:IsL (⋃₀ ↑S \ {0})⊢ IsL (t \ {0} ∪ ⋃₀ ↑S \ {0}); exact h1.union h2All goals completed! 🐙

The sets L α for test-free α with voc α = {a} are exactly the nonempty semilinear sets X ⊆ ℕ such that, if 0 ∈ X, then X contains all multiples of some p > 0.

theorem exists_L_eq_iff (X : Set ℕ) :
    (∃ α : Program, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X) ↔
    IsSemilinearSet X ∧ X.Nonempty ∧ (0 ∈ X → ∃ p, 0 < p ∧ ∀ k, k * p ∈ X) := byX:Set ℕ⊢ (∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X) ↔
  IsSemilinearSet X ∧ X.Nonempty ∧ (0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ X)
  constructormpX:Set ℕ⊢ (∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X) →
  IsSemilinearSet X ∧ X.Nonempty ∧ (0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ X)mprX:Set ℕ⊢ IsSemilinearSet X ∧ X.Nonempty ∧ (0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ X) →
  ∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X
  ·mpX:Set ℕ⊢ (∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X) →
  IsSemilinearSet X ∧ X.Nonempty ∧ (0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ X) rintro ⟨α, hα, -, rfl⟩mpα:Programhα:α.testFree⊢ IsSemilinearSet {n | L α n} ∧ {n | L α n}.Nonempty ∧ (0 ∈ {n | L α n} → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ {n | L α n})
    refine ⟨L_isSemilinearSet α hα, ?_, ?_⟩mp.refine_1α:Programhα:α.testFree⊢ {n | L α n}.Nonemptymp.refine_2α:Programhα:α.testFree⊢ 0 ∈ {n | L α n} → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ {n | L α n}
    ·mp.refine_1α:Programhα:α.testFree⊢ {n | L α n}.Nonempty obtain ⟨n, -, hn⟩ := L_pos α hαmp.refine_1α:Programhα:α.testFreen:ℕhn:L α n⊢ {n | L α n}.Nonempty
      exact ⟨n, hn⟩All goals completed! 🐙
    ·mp.refine_2α:Programhα:α.testFree⊢ 0 ∈ {n | L α n} → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ {n | L α n} intro h0mp.refine_2α:Programhα:α.testFreeh0:0 ∈ {n | L α n}⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ {n | L α n}
      obtain ⟨p, hp, hLp⟩ := L_zero α hα h0mp.refine_2α:Programhα:α.testFreeh0:0 ∈ {n | L α n}p:ℕhp:0 < phLp:∀ (k : ℕ), L α (k * p)⊢ ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ {n | L α n}
      exact ⟨p, hp, hLp⟩All goals completed! 🐙
  ·mprX:Set ℕ⊢ IsSemilinearSet X ∧ X.Nonempty ∧ (0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ X) →
  ∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X rintro ⟨hX, hne, h0⟩mprX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ X⊢ ∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X
    rcases hX.isL_diff_zero with h | hmpr.inlX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:X \ {0} = ∅⊢ ∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = Xmpr.inrX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})⊢ ∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X
    ·mpr.inlX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:X \ {0} = ∅⊢ ∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X -- then `X ⊆ {0}`, so `X = {0}`, which is excluded
      exfalsompr.inlX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:X \ {0} = ∅⊢ False
      rw [sdiff_eq_emptympr.inlX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:X ⊆ {0}⊢ False] at hmpr.inlX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:X ⊆ {0}⊢ False
      obtain ⟨x, hx⟩ := hnempr.inlX:Set ℕhX:IsSemilinearSet Xh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:X ⊆ {0}x:ℕhx:x ∈ X⊢ False
      obtain rfl : x = 0 := h hxmpr.inlX:Set ℕhX:IsSemilinearSet Xh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:X ⊆ {0}hx:0 ∈ X⊢ False
      obtain ⟨p, hp, hLp⟩ := h0 hxmpr.inlX:Set ℕhX:IsSemilinearSet Xh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:X ⊆ {0}hx:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ X⊢ False
      have := h (hLp 1)mpr.inlX:Set ℕhX:IsSemilinearSet Xh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:X ⊆ {0}hx:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xthis:1 * p ∈ {0}⊢ False
      simp at thismpr.inlX:Set ℕhX:IsSemilinearSet Xh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:X ⊆ {0}hx:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xthis:p = 0⊢ False
      omegaAll goals completed! 🐙
    ·mpr.inrX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})⊢ ∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X by_cases h0X : 0 ∈ XposX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ X⊢ ∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = XnegX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∉ X⊢ ∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X
      ·posX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ X⊢ ∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X obtain ⟨p, hp, hLp⟩ := h0 h0XposX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ X⊢ ∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X
        obtain ⟨α, hα, hv, hL⟩ := h.union (IsL.singleton_of_pos hp).closureposX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})⊢ ∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X
        refine ⟨α, hα, hv, ?_⟩posX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})⊢ {n | L α n} = X
        rw [hLposX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})⊢ X \ {0} ∪ ↑(closure {p}) = X]posX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})⊢ X \ {0} ∪ ↑(closure {p}) = X
        ext nposX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})n:ℕ⊢ n ∈ X \ {0} ∪ ↑(closure {p}) ↔ n ∈ X
        simp only [mem_union, mem_sdiff, mem_singleton_iff, SetLike.mem_coe,
          AddSubmonoid.mem_closure_singleton, smul_eq_mul]posX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})n:ℕ⊢ (n ∈ X ∧ ¬n = 0 ∨ ∃ n_1, n_1 * p = n) ↔ n ∈ X
        constructorpos.mpX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})n:ℕ⊢ (n ∈ X ∧ ¬n = 0 ∨ ∃ n_1, n_1 * p = n) → n ∈ Xpos.mprX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})n:ℕ⊢ n ∈ X → n ∈ X ∧ ¬n = 0 ∨ ∃ n_1, n_1 * p = n
        ·pos.mpX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})n:ℕ⊢ (n ∈ X ∧ ¬n = 0 ∨ ∃ n_1, n_1 * p = n) → n ∈ X rintro (⟨hn, -⟩ | ⟨k, rfl⟩)pos.mp.inlX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})n:ℕhn:n ∈ X⊢ n ∈ Xpos.mp.inrX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})k:ℕ⊢ k * p ∈ X
          ·pos.mp.inlX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})n:ℕhn:n ∈ X⊢ n ∈ X exact hnAll goals completed! 🐙
          ·pos.mp.inrX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})k:ℕ⊢ k * p ∈ X exact hLp kAll goals completed! 🐙
        ·pos.mprX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})n:ℕ⊢ n ∈ X → n ∈ X ∧ ¬n = 0 ∨ ∃ n_1, n_1 * p = n intro hnpos.mprX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})n:ℕhn:n ∈ X⊢ n ∈ X ∧ ¬n = 0 ∨ ∃ n_1, n_1 * p = n
          by_cases hn0 : n = 0posX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})n:ℕhn:n ∈ Xhn0:n = 0⊢ n ∈ X ∧ ¬n = 0 ∨ ∃ n_1, n_1 * p = nnegX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})n:ℕhn:n ∈ Xhn0:¬n = 0⊢ n ∈ X ∧ ¬n = 0 ∨ ∃ n_1, n_1 * p = n
          ·posX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})n:ℕhn:n ∈ Xhn0:n = 0⊢ n ∈ X ∧ ¬n = 0 ∨ ∃ n_1, n_1 * p = n exact Or.inr ⟨0, byX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})n:ℕhn:n ∈ Xhn0:n = 0⊢ 0 * p = n simp [hn0]All goals completed! 🐙⟩
          ·negX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∈ Xp:ℕhp:0 < phLp:∀ (k : ℕ), k * p ∈ Xα:Programhα:α.testFreehv:α.voc = {Sum.inr 0}hL:{n | L α n} = X \ {0} ∪ ↑(closure {p})n:ℕhn:n ∈ Xhn0:¬n = 0⊢ n ∈ X ∧ ¬n = 0 ∨ ∃ n_1, n_1 * p = n exact Or.inl ⟨hn, hn0⟩All goals completed! 🐙
      ·negX:Set ℕhX:IsSemilinearSet Xhne:X.Nonemptyh0:0 ∈ X → ∃ p, 0 < p ∧ ∀ (k : ℕ), k * p ∈ Xh:IsL (X \ {0})h0X:0 ∉ X⊢ ∃ α, α.testFree ∧ α.voc = {Sum.inr 0} ∧ {n | L α n} = X rwa [sdiff_singleton_eq_self h0X] at hAll goals completed! 🐙

Semilinearity of L α for programs over a single atomic program

L of compound programs as set operations

Every L α is semilinear

Two obstructions to the converse

The converse, for the sets without these obstructions

Semilinearity of `L α` for programs over a single atomic program

`L` of compound programs as set operations

Every `L α` is semilinear