New file

In this file...

Main declarations

• ConNF.foo: Something new.

theorem ConNF.Support.not_mem_scoderiv_botDeriv [ConNF.Params] {β γ : ConNF.Λ} {hγ : ↑γ < ↑β} (S : ConNF.Support ↑γ) (N : ConNF.NearLitter) : N ∉ (S ↗ hγ ⇘. (ConNF.Path.nil ↘.))ᴺ

theorem ConNF.Support.not_mem_strong_botDeriv [ConNF.Params] {β γ : ConNF.Λ} {hγ : ↑γ < ↑β} [ConNF.Level] [ConNF.LtLevel ↑β] (S : ConNF.Support ↑γ) (N : ConNF.NearLitter) : N ∉ ((S ↗ hγ).strong ⇘. (ConNF.Path.nil ↘.))ᴺ

theorem ConNF.Support.raise_preStrong' [ConNF.Params] {β γ : ConNF.Λ} [ConNF.Level] [ConNF.LtLevel ↑β] (S : ConNF.Support ↑ConNF.α) (hS : S.Strong) (T : ConNF.Support ↑γ) (ρ : ConNF.AllPerm ↑β) (hγ : ↑γ < ↑β) : (S + (ρᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯).PreStrong

theorem ConNF.Support.raise_closed' [ConNF.Params] {β γ : ConNF.Λ} [ConNF.Level] [ConNF.LtLevel ↑β] (S : ConNF.Support ↑ConNF.α) (hS : S.Strong) (T : ConNF.Support ↑γ) (ρ : ConNF.AllPerm ↑β) (hγ : ↑γ < ↑β) (hρ : ρᵁ • S ↘ ⋯ = S ↘ ⋯) : (S + (ρᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯).Closed

theorem ConNF.Support.raise_strong' [ConNF.Params] {β γ : ConNF.Λ} [ConNF.Level] [ConNF.LtLevel ↑β] (S : ConNF.Support ↑ConNF.α) (hS : S.Strong) (T : ConNF.Support ↑γ) (ρ : ConNF.AllPerm ↑β) (hγ : ↑γ < ↑β) (hρ : ρᵁ • S ↘ ⋯ = S ↘ ⋯) : (S + (ρᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯).Strong

theorem ConNF.Support.convAtoms_injective_of_fixes [ConNF.Params] {β γ : ConNF.Λ} [ConNF.Level] [ConNF.LtLevel ↑β] {S : ConNF.Support ↑ConNF.α} {T : ConNF.Support ↑γ} {ρ₁ ρ₂ : ConNF.AllPerm ↑β} {hγ : ↑γ < ↑β} (hρ₁ : ρ₁ᵁ • S ↘ ⋯ = S ↘ ⋯) (hρ₂ : ρ₂ᵁ • S ↘ ⋯ = S ↘ ⋯) (A : ↑ConNF.α ↝ ⊥) : (ConNF.convAtoms (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A).Injective

theorem ConNF.Support.atomMemRel_le_of_fixes [ConNF.Params] {β γ : ConNF.Λ} [ConNF.Level] [ConNF.LtLevel ↑β] {S : ConNF.Support ↑ConNF.α} {T : ConNF.Support ↑γ} {ρ₁ ρ₂ : ConNF.AllPerm ↑β} {hγ : ↑γ < ↑β} (hρ₁ : ρ₁ᵁ • S ↘ ⋯ = S ↘ ⋯) (hρ₂ : ρ₂ᵁ • S ↘ ⋯ = S ↘ ⋯) (A : ↑ConNF.α ↝ ⊥) : ConNF.atomMemRel (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A ≤ ConNF.atomMemRel (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A

theorem ConNF.Support.convNearLitters_cases [ConNF.Params] {β γ : ConNF.Λ} [ConNF.Level] [ConNF.LtLevel ↑β] {S : ConNF.Support ↑ConNF.α} {T : ConNF.Support ↑γ} {ρ₁ ρ₂ : ConNF.AllPerm ↑β} {hγ : ↑γ < ↑β} {A : ↑ConNF.α ↝ ⊥} {N₁ N₂ : ConNF.NearLitter} : ConNF.convNearLitters (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A N₁ N₂ → N₁ = N₂ ∧ N₁ ∈ (S ⇘. A)ᴺ ∨ ∃ (B : ↑β ↝ ⊥), A = B ↗ ⋯ ∧ (ρ₁ᵁ B)⁻¹ • N₁ = (ρ₂ᵁ B)⁻¹ • N₂ ∧ (ρ₁ᵁ B)⁻¹ • N₁ ∈ (((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport) ⇘. B)ᴺ

theorem ConNF.Support.inflexible_of_inflexible_of_fixes [ConNF.Params] {β γ : ConNF.Λ} [ConNF.Level] [ConNF.LtLevel ↑β] {S : ConNF.Support ↑ConNF.α} {T : ConNF.Support ↑γ} {ρ₁ ρ₂ : ConNF.AllPerm ↑β} {hγ : ↑γ < ↑β} (hρ₁ : ρ₁ᵁ • S ↘ ⋯ = S ↘ ⋯) (hρ₂ : ρ₂ᵁ • S ↘ ⋯ = S ↘ ⋯) {A : ↑ConNF.α ↝ ⊥} {N₁ N₂ : ConNF.NearLitter} : ConNF.convNearLitters (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A N₁ N₂ → ∀ (P : ConNF.InflexiblePath ↑ConNF.α) (t : ConNF.Tangle P.δ), A = P.A ↘ ⋯ ↘. → N₁ᴸ = ConNF.fuzz ⋯ t → ∃ (ρ : ConNF.AllPerm P.δ), N₂ᴸ = ConNF.fuzz ⋯ (ρ • t)

theorem ConNF.Support.atoms_of_inflexible_of_fixes [ConNF.Params] {β γ : ConNF.Λ} [ConNF.Level] [ConNF.LtLevel ↑β] {S : ConNF.Support ↑ConNF.α} (hS : S.Strong) {T : ConNF.Support ↑γ} {ρ₁ ρ₂ : ConNF.AllPerm ↑β} {hγ : ↑γ < ↑β} (hρ₁ : ρ₁ᵁ • S ↘ ⋯ = S ↘ ⋯) (hρ₂ : ρ₂ᵁ • S ↘ ⋯ = S ↘ ⋯) (A : ↑ConNF.α ↝ ⊥) (N₁ N₂ : ConNF.NearLitter) (P : ConNF.InflexiblePath ↑ConNF.α) (t : ConNF.Tangle P.δ) (ρ : ConNF.AllPerm P.δ) : A = P.A ↘ ⋯ ↘. → N₁ᴸ = ConNF.fuzz ⋯ t → N₂ᴸ = ConNF.fuzz ⋯ (ρ • t) → ConNF.convNearLitters (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A N₁ N₂ → ∀ (B : P.δ ↝ ⊥), ∀ a ∈ (t.support ⇘. B)ᴬ, ∀ (i : ConNF.κ), ((S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i a → ((S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i (ρᵁ B • a)

theorem ConNF.Support.nearLitters_of_inflexible_of_fixes [ConNF.Params] {β γ : ConNF.Λ} [ConNF.Level] [ConNF.LtLevel ↑β] {S : ConNF.Support ↑ConNF.α} (hS : S.Strong) {T : ConNF.Support ↑γ} {ρ₁ ρ₂ : ConNF.AllPerm ↑β} {hγ : ↑γ < ↑β} (hρ₁ : ρ₁ᵁ • S ↘ ⋯ = S ↘ ⋯) (hρ₂ : ρ₂ᵁ • S ↘ ⋯ = S ↘ ⋯) (A : ↑ConNF.α ↝ ⊥) (N₁ N₂ : ConNF.NearLitter) (P : ConNF.InflexiblePath ↑ConNF.α) (t : ConNF.Tangle P.δ) (ρ : ConNF.AllPerm P.δ) : A = P.A ↘ ⋯ ↘. → N₁ᴸ = ConNF.fuzz ⋯ t → N₂ᴸ = ConNF.fuzz ⋯ (ρ • t) → ConNF.convNearLitters (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A N₁ N₂ → ∀ (B : P.δ ↝ ⊥), ∀ N ∈ (t.support ⇘. B)ᴺ, ∀ (i : ConNF.κ), ((S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i N → ((S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i (ρᵁ B • N)

theorem ConNF.Support.litter_eq_of_flexible_of_fixes [ConNF.Params] {β γ : ConNF.Λ} [ConNF.Level] [ConNF.LtLevel ↑β] {S : ConNF.Support ↑ConNF.α} {T : ConNF.Support ↑γ} {ρ₁ ρ₂ : ConNF.AllPerm ↑β} {hγ : ↑γ < ↑β} (hρ₁ : ρ₁ᵁ • S ↘ ⋯ = S ↘ ⋯) (hρ₂ : ρ₂ᵁ • S ↘ ⋯ = S ↘ ⋯) {A : ↑ConNF.α ↝ ⊥} {N₁ N₂ N₃ N₄ : ConNF.NearLitter} : ConNF.convNearLitters (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A N₁ N₂ → ConNF.convNearLitters (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A N₃ N₄ → ¬ConNF.Inflexible A N₁ᴸ → ¬ConNF.Inflexible A N₂ᴸ → ¬ConNF.Inflexible A N₃ᴸ → ¬ConNF.Inflexible A N₄ᴸ → N₁ᴸ = N₃ᴸ → N₂ᴸ = N₄ᴸ

theorem ConNF.Support.sameSpecLe_of_fixes [ConNF.Params] {β γ : ConNF.Λ} [ConNF.Level] [ConNF.LtLevel ↑β] (S : ConNF.Support ↑ConNF.α) (hS : S.Strong) (T : ConNF.Support ↑γ) (ρ₁ ρ₂ : ConNF.AllPerm ↑β) (hγ : ↑γ < ↑β) (hρ₁ : ρ₁ᵁ • S ↘ ⋯ = S ↘ ⋯) (hρ₂ : ρ₂ᵁ • S ↘ ⋯ = S ↘ ⋯) : ConNF.SameSpecLE (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯)

theorem ConNF.Support.spec_same_of_fixes [ConNF.Params] {β γ : ConNF.Λ} {hγ : ↑γ < ↑β} [ConNF.Level] [ConNF.LtLevel ↑β] (S : ConNF.Support ↑ConNF.α) (hS : S.Strong) (T : ConNF.Support ↑γ) (ρ : ConNF.AllPerm ↑β) (hρ : ρᵁ • S ↘ ⋯ = S ↘ ⋯) : (S + ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport) ↗ ⋯).spec = (S + (ρᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯).spec

theorem ConNF.Support.exists_allowable_of_fixes [ConNF.Params] {β γ : ConNF.Λ} [ConNF.Level] [ConNF.LtLevel ↑β] (S : ConNF.Support ↑ConNF.α) (hS : S.Strong) (T : ConNF.Support ↑γ) (ρ : ConNF.AllPerm ↑β) (hγ : ↑γ < ↑β) (hρ : ρᵁ • S ↘ ⋯ = S ↘ ⋯) : ∃ (ρ' : ConNF.AllPerm ↑ConNF.α), ρ'ᵁ • S = S ∧ ρ'ᵁ ↘ ⋯ ↘ hγ • T = ρᵁ ↘ hγ • T