noncomputable def ConNF.StructApprox.completeAtomPerm [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) : Equiv.Perm ConNF.Atom

Equations

• ConNF.StructApprox.completeAtomPerm hπf A = Equiv.ofBijective (π.completeAtomMap A) ⋯

noncomputable def ConNF.StructApprox.completeLitterPerm [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) : Equiv.Perm ConNF.Litter

Equations

• ConNF.StructApprox.completeLitterPerm hπf A = Equiv.ofBijective (π.completeLitterMap A) ⋯

theorem ConNF.StructApprox.completeAtomPerm_apply [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom) : (ConNF.StructApprox.completeAtomPerm hπf A) a = π.completeAtomMap A a

theorem ConNF.StructApprox.completeLitterPerm_apply [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) : (ConNF.StructApprox.completeLitterPerm hπf A) L = π.completeLitterMap A L

noncomputable def ConNF.StructApprox.completeBasePerm [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) : ConNF.BasePerm

Equations

• ConNF.StructApprox.completeBasePerm hπf A = { atomPerm := ConNF.StructApprox.completeAtomPerm hπf A, litterPerm := ConNF.StructApprox.completeLitterPerm hπf A, near := ⋯ }

theorem ConNF.StructApprox.completeBasePerm_smul_atom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom) : ConNF.StructApprox.completeBasePerm hπf A • a = π.completeAtomMap A a

theorem ConNF.StructApprox.completeBasePerm_smul_litter [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) : ConNF.StructApprox.completeBasePerm hπf A • L = π.completeLitterMap A L

theorem ConNF.StructApprox.completeBasePerm_smul_nearLitter [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) : ConNF.StructApprox.completeBasePerm hπf A • N = π.completeNearLitterMap A N

def ConNF.StructApprox.AllowableBelow [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (γ : ConNF.TypeIndex) [ConNF.LeLevel γ] (A : Quiver.Path (↑β) γ) : Prop

Equations

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

@[simp]

theorem ConNF.StructApprox.ofBot_toStructPerm [ConNF.Params] (π : ConNF.Allowable ⊥) : ConNF.Tree.ofBot (ConNF.Allowable.toStructPerm π) = π

theorem ConNF.StructApprox.allowableBelow_bot [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) : ConNF.StructApprox.AllowableBelow hπf ⊥ A

theorem ConNF.StructApprox.exists_nil_cons_of_path' [ConNF.Params] {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} (A : Quiver.Path β γ) (hA : A.length ≠ 0) : ∃ (δ : ConNF.TypeIndex) (h : δ < β) (B : Quiver.Path δ γ), A = (Quiver.Path.nil.cons h).comp B

theorem ConNF.StructApprox.exists_nil_cons_of_path [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (A : ConNF.ExtendedIndex ↑β) : ∃ (γ : ConNF.TypeIndex) (_ : ConNF.LtLevel γ) (h : γ < ↑β) (B : ConNF.ExtendedIndex γ), A = (Quiver.Path.nil.cons h).comp B

theorem ConNF.StructApprox.ConNF.StructApprox.extracted_1' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (γ : ConNF.Λ) [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) (ρs : (δ : ConNF.TypeIndex) → [inst : ConNF.LtLevel δ] → δ < ↑γ → ConNF.Allowable δ) (hρ : ∀ (δ : ConNF.TypeIndex) [inst : ConNF.LtLevel δ] (h : δ < ↑γ) (B : ConNF.ExtendedIndex δ), ConNF.Tree.ofBot (ConNF.Tree.comp B (ConNF.Allowable.toStructPerm (ρs δ h))) = ConNF.StructApprox.completeBasePerm hπf ((A.cons h).comp B)) (ε : ConNF.Λ) [ConNF.LtLevel ↑ε] (hε : ↑ε < ↑γ) (a : ConNF.Atom) : ConNF.Allowable.toStructPerm (ρs (↑ε) hε) (Quiver.Hom.toPath ⋯) • ConNF.fuzz ⋯ a = ConNF.fuzz ⋯ (BasePerm.ofBot (ρs ⊥ ⋯) • a)

theorem ConNF.StructApprox.ConNF.StructApprox.extracted_2' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (γ : ConNF.Λ) [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) (ρs : (δ : ConNF.TypeIndex) → [inst : ConNF.LtLevel δ] → δ < ↑γ → ConNF.Allowable δ) (hρ : ∀ (δ : ConNF.TypeIndex) [inst : ConNF.LtLevel δ] (h : δ < ↑γ) (B : ConNF.ExtendedIndex δ), ConNF.Tree.ofBot (ConNF.Tree.comp B (ConNF.Allowable.toStructPerm (ρs δ h))) = ConNF.StructApprox.completeBasePerm hπf ((A.cons h).comp B)) (δ : ConNF.Λ) [ConNF.LtLevel ↑δ] (ε : ConNF.Λ) [ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) (t : ConNF.Tangle ↑δ) : ConNF.Allowable.toStructPerm (ρs (↑ε) hε) (Quiver.Hom.toPath ⋯) • ConNF.fuzz hδε t = ConNF.fuzz hδε (ρs (↑δ) hδ • t)

theorem ConNF.StructApprox.allowableBelow_extends [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (γ : ConNF.Λ) [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) (h : ∀ (δ : ConNF.TypeIndex) [inst : ConNF.LtLevel δ] (h : δ < ↑γ), ConNF.StructApprox.AllowableBelow hπf δ (A.cons h)) : ConNF.StructApprox.AllowableBelow hπf (↑γ) A

theorem ConNF.StructApprox.allowableBelow_all [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (γ : ConNF.Λ) [i : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) : ConNF.StructApprox.AllowableBelow hπf (↑γ) A

noncomputable def ConNF.StructApprox.completeAllowable [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) : ConNF.Allowable ↑β

Equations

• ConNF.StructApprox.completeAllowable hπf = Exists.choose ⋯

theorem ConNF.StructApprox.completeAllowable_comp [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) : ConNF.Allowable.toStructPerm (ConNF.StructApprox.completeAllowable hπf) = ConNF.StructApprox.completeBasePerm hπf

theorem ConNF.StructApprox.complete_exception_mem [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom) (ha : (ConNF.StructApprox.completeBasePerm hπf A).IsException a) : a ∈ (π A).atomPerm.domain

theorem ConNF.StructApprox.completeAllowable_exactlyApproximates [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) : π.ExactlyApproximates (ConNF.Allowable.toStructPerm (ConNF.StructApprox.completeAllowable hπf))

def ConNF.StructApprox.foa_extends [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] : ConNF.StructApprox.FOAIh β

Equations

• ⋯ = ⋯

theorem ConNF.StructApprox.freedom_of_action [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [i : ConNF.LeLevel ↑β] (π₀ : ConNF.StructApprox ↑β) (h : π₀.Free) : ∃ (π : ConNF.Allowable ↑β), π₀.ExactlyApproximates (ConNF.Allowable.toStructPerm π)