Supports with the same specification

def ConNF.ConvertAtom [ConNF.Params] {β : ConNF.Λ} (S : ConNF.Support ↑β) (T : ConNF.Support ↑β) (A : ConNF.ExtendedIndex ↑β) (aS : ConNF.Atom) (aT : ConNF.Atom) : Prop

Equations

• ConNF.ConvertAtom S T A aS aT = ∃ (i : ConNF.κ) (hiS : i < S.max) (hiT : i < T.max), S.f i hiS = { path := A, value := Sum.inl aS } ∧ T.f i hiT = { path := A, value := Sum.inl aT }

def ConNF.ConvertNearLitter [ConNF.Params] {β : ConNF.Λ} (S : ConNF.Support ↑β) (T : ConNF.Support ↑β) (A : ConNF.ExtendedIndex ↑β) (NS : ConNF.NearLitter) (NT : ConNF.NearLitter) : Prop

Equations

• ConNF.ConvertNearLitter S T A NS NT = ∃ (i : ConNF.κ) (hiS : i < S.max) (hiT : i < T.max), S.f i hiS = { path := A, value := Sum.inr NS } ∧ T.f i hiT = { path := A, value := Sum.inr NT }

theorem ConNF.convertAtom_subsingleton [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) (A : ConNF.ExtendedIndex ↑β) (aS : ConNF.Atom) (aT : ConNF.Atom) (aT' : ConNF.Atom) (h : ConNF.ConvertAtom S T A aS aT) (h' : ConNF.ConvertAtom S T A aS aT') : aT = aT'

theorem ConNF.convert_flexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) {A : ConNF.ExtendedIndex ↑β} {NS : ConNF.NearLitter} {NT : ConNF.NearLitter} (h : ConNF.Flexible A NS.fst) {i : ConNF.κ} (hiS : i < S.max) (hiT : i < T.max) (hiNS : S.f i hiS = { path := A, value := Sum.inr NS }) (hiNT : T.f i hiT = { path := A, value := Sum.inr NT }) : ConNF.Flexible A NT.fst

theorem ConNF.convertNearLitter_subsingleton_flexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) (A : ConNF.ExtendedIndex ↑β) (NS : ConNF.NearLitter) (NT : ConNF.NearLitter) (NT' : ConNF.NearLitter) (h : ConNF.ConvertNearLitter S T A NS NT) (h' : ConNF.ConvertNearLitter S T A NS NT') (hN : ConNF.Flexible A NS.fst) : NT = NT'

theorem ConNF.convert_inflexibleCoe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) {A : ConNF.ExtendedIndex ↑β} {NS : ConNF.NearLitter} {NT : ConNF.NearLitter} (P : ConNF.InflexibleCoePath A) (t : ConNF.Tangle ↑P.δ) (hNS : NS.fst = ConNF.fuzz ⋯ t) {i : ConNF.κ} (hiS : i < S.max) (hiT : i < T.max) (hiNS : S.f i hiS = { path := A, value := Sum.inr NS }) (hiNT : T.f i hiT = { path := A, value := Sum.inr NT }) : ∃ (t' : ConNF.Tangle ↑P.δ), NT.fst = ConNF.fuzz ⋯ t'

theorem ConNF.convert_inflexibleBot [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) {A : ConNF.ExtendedIndex ↑β} {NS : ConNF.NearLitter} {NT : ConNF.NearLitter} (P : ConNF.InflexibleBotPath A) (a : ConNF.Atom) (hNS : NS.fst = ConNF.fuzz ⋯ a) {i : ConNF.κ} (hiS : i < S.max) (hiT : i < T.max) (hiNS : S.f i hiS = { path := A, value := Sum.inr NS }) (hiNT : T.f i hiT = { path := A, value := Sum.inr NT }) : ∃ (a' : ConNF.Atom), NT.fst = ConNF.fuzz ⋯ a'

theorem ConNF.comp_eq_same [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) {i : ConNF.κ} (hiS : i < S.max) {γ : ConNF.Λ} (A : Quiver.Path ↑β ↑γ) (c : ConNF.Address ↑γ) (hc : S.f i hiS = { path := A.comp c.path, value := c.value }) : ∃ (d : ConNF.Address ↑γ), T.f i ⋯ = { path := A.comp d.path, value := d.value }

theorem ConNF.support_tangle_ext [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} (hS : S.Strong) {A : ConNF.ExtendedIndex ↑β} (P : ConNF.InflexibleCoePath A) (t₁ : ConNF.Tangle ↑P.δ) (t₂ : ConNF.Tangle ↑P.δ) (h₁ : t₁.set = t₂.set) (h₂ : t₁.support.max = t₂.support.max) (h₃ : (fun (j : ConNF.κ) => {k : ConNF.κ | ∃ (hj : j < t₁.support.max) (hk : k < S.max), { path := (P.B.cons ⋯).comp (t₁.support.f j hj).path, value := (t₁.support.f j hj).value } = S.f k hk}) = fun (j : ConNF.κ) => {k : ConNF.κ | ∃ (hj : j < t₂.support.max) (hk : k < S.max), { path := (P.B.cons ⋯).comp (t₂.support.f j hj).path, value := (t₂.support.f j hj).value } = S.f k hk}) {i : ConNF.κ} (hi₁ : i < S.max) {N : ConNF.NearLitter} (hi₂ : S.f i hi₁ = { path := A, value := Sum.inr N }) (hi₃ : N.fst = ConNF.fuzz ⋯ t₁) : t₁ = t₂

theorem ConNF.convertNearLitter_subsingleton_inflexibleCoe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) (A : ConNF.ExtendedIndex ↑β) (NS : ConNF.NearLitter) (NT : ConNF.NearLitter) (NT' : ConNF.NearLitter) (h : ConNF.ConvertNearLitter S T A NS NT) (h' : ConNF.ConvertNearLitter S T A NS NT') (hNS : ConNF.InflexibleCoe A NS.fst) : NT = NT'

theorem ConNF.convertNearLitter_subsingleton_inflexibleBot [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) (A : ConNF.ExtendedIndex ↑β) (NS : ConNF.NearLitter) (NT : ConNF.NearLitter) (NT' : ConNF.NearLitter) (h : ConNF.ConvertNearLitter S T A NS NT) (h' : ConNF.ConvertNearLitter S T A NS NT') (hNS : ConNF.InflexibleBot A NS.fst) : NT = NT'

theorem ConNF.convertNearLitter_subsingleton [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) (A : ConNF.ExtendedIndex ↑β) (NS : ConNF.NearLitter) (NT : ConNF.NearLitter) (NT' : ConNF.NearLitter) (h : ConNF.ConvertNearLitter S T A NS NT) (h' : ConNF.ConvertNearLitter S T A NS NT') : NT = NT'

theorem ConNF.convertAtom_dom_small [ConNF.Params] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} (A : ConNF.ExtendedIndex ↑β) : ConNF.Small {a : ConNF.Atom | ∃ (a' : ConNF.Atom), ConNF.ConvertAtom S T A a a'}

theorem ConNF.convertNearLitter_dom_small [ConNF.Params] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} (A : ConNF.ExtendedIndex ↑β) : ConNF.Small {N : ConNF.NearLitter | ∃ (N' : ConNF.NearLitter), ConNF.ConvertNearLitter S T A N N'}

noncomputable def ConNF.convert [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) : ConNF.StructNLAction ↑β

Equations

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

theorem ConNF.convIndex [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) {i : ConNF.κ} (h : i < S.max) : i < T.max

theorem ConNF.convert_atomMap_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} {b : ConNF.Atom} (h : ConNF.ConvertAtom S T A a b) : ((ConNF.convert hσS hσT A).atomMap a).get ⋯ = b

theorem ConNF.convert_nearLitterMap_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) {A : ConNF.ExtendedIndex ↑β} {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} (h : ConNF.ConvertNearLitter S T A N₁ N₂) : ((ConNF.convert hσS hσT A).nearLitterMap N₁).get ⋯ = N₂

theorem ConNF.convertAtom_dom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} (h : { path := A, value := Sum.inl a } ∈ S) : ∃ (b : ConNF.Atom), ConNF.ConvertAtom S T A a b

theorem ConNF.convertNearLitter_dom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter} (h : { path := A, value := Sum.inr N } ∈ S) : ∃ (N' : ConNF.NearLitter), ConNF.ConvertNearLitter S T A N N'

theorem ConNF.convertAtom_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} {b : ConNF.Atom} {c : ConNF.Atom} (ha : ConNF.ConvertAtom S T A a c) (hb : ConNF.ConvertAtom S T A b c) : a = b

theorem ConNF.convertAtom_mem_convertLitter_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} {a' : ConNF.Atom} {N : ConNF.NearLitter} {N' : ConNF.NearLitter} (ha : ConNF.ConvertAtom S T A a a') (hb : ConNF.ConvertNearLitter S T A N N') : a' ∈ N' ↔ a ∈ N

theorem ConNF.support_tangle_ext' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} (hT : T.Strong) {A : ConNF.ExtendedIndex ↑β} (P : ConNF.InflexibleCoePath A) (t₁ : ConNF.Tangle ↑P.δ) (t₂ : ConNF.Tangle ↑P.δ) (ρ : ConNF.Allowable ↑P.δ) (h₁ : t₁.set = ρ • t₂.set) (h₂ : t₁.support.max = t₂.support.max) (h₃ : (fun (j : ConNF.κ) => {k : ConNF.κ | ∃ (hj : j < t₁.support.max) (hk : k < T.max), { path := (P.B.cons ⋯).comp (t₁.support.f j hj).path, value := (t₁.support.f j hj).value } = T.f k hk}) = fun (j : ConNF.κ) => {k : ConNF.κ | ∃ (hj : j < t₂.support.max) (hk : k < S.max), { path := (P.B.cons ⋯).comp (t₂.support.f j hj).path, value := (t₂.support.f j hj).value } = S.f k hk}) {i : ConNF.κ} (hi₁ : i < S.max) (hi₂ : i < T.max) {N : ConNF.NearLitter} (hi₃ : T.f i hi₂ = { path := A, value := Sum.inr N }) (hi₄ : N.fst = ConNF.fuzz ⋯ t₁) (hi₅ : (T.before i hi₂).comp (P.B.cons ⋯) = ρ • (S.before i hi₁).comp (P.B.cons ⋯)) : t₁ = ρ • t₂

theorem ConNF.convertNearLitter_fst [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) {A : ConNF.ExtendedIndex ↑β} {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} {N₃ : ConNF.NearLitter} {N₄ : ConNF.NearLitter} (h₁ : ConNF.ConvertNearLitter S T A N₁ N₃) (h₂ : ConNF.ConvertNearLitter S T A N₂ N₄) (h : N₁.fst = N₂.fst) : N₃.fst = N₄.fst

theorem ConNF.convertNearLitter_fst' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) {A : ConNF.ExtendedIndex ↑β} {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} {N₃ : ConNF.NearLitter} {N₄ : ConNF.NearLitter} (h₁ : ConNF.ConvertNearLitter S T A N₁ N₃) (h₂ : ConNF.ConvertNearLitter S T A N₂ N₄) (h : N₃.fst = N₄.fst) : N₁.fst = N₂.fst

theorem ConNF.convert_lawful [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) : (ConNF.convert hσS hσT).Lawful

theorem ConNF.convert_coherentDom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) : (ConNF.convert hσS hσT).CoherentDom

theorem ConNF.convert_coherent [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) : (ConNF.convert hσS hσT).Coherent

noncomputable def ConNF.convertAllowable [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) : ConNF.Allowable ↑β

Equations

• ConNF.convertAllowable hσS hσT = ⋯.choose

theorem ConNF.convertAllowable_spec [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) : (ConNF.convert hσS hσT).Approximates (ConNF.Allowable.toStructPerm (ConNF.convertAllowable hσS hσT))

theorem ConNF.convert_atomMap_get [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} {i : ConNF.κ} (hiS : i < S.max) (h : S.f i hiS = { path := A, value := Sum.inl a }) : T.f i ⋯ = { path := A, value := Sum.inl (((ConNF.convert hσS hσT A).atomMap a).get ⋯) }

theorem ConNF.convert_nearLitterMap_get [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter} {i : ConNF.κ} (hiS : i < S.max) (h : S.f i hiS = { path := A, value := Sum.inr N }) : T.f i ⋯ = { path := A, value := Sum.inr (((ConNF.convert hσS hσT A).nearLitterMap N).get ⋯) }

theorem ConNF.convertAllowable_smul' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) (i : ConNF.κ) (hiS : i < S.max) (hiT : i < T.max) : ConNF.convertAllowable hσS hσT • S.f i hiS = T.f i hiT

theorem ConNF.convertAllowable_smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {S : ConNF.Support ↑β} {T : ConNF.Support ↑β} {hS : S.Strong} {hT : T.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) : ConNF.convertAllowable hσS hσT • S = T