Hypotheses for proving freedom of action

This file contains the inductive hypotheses required for proving the freedom of action theorem.

Main declarations

• ConNF.FOAData: Contains various kinds of tangle data for all levels below α.
• ConNF.FOAAssumptions: Describes how the type levels in the FOAData tangle together.

class ConNF.FOAData [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] : Type (u + 1)

The data that we will use when proving the freedom of action theorem. This structure combines the following data:

• TSet
• Allowable
• pos : Tangle β ↪ μ
• typedNearLitter

• lowerModelData : (β : ConNF.Λ) → [inst : ConNF.LeLevel ↑β] → ConNF.ModelData ↑β
• lowerPositionedTangles : (β : ConNF.Λ) → [inst : ConNF.LtLevel ↑β] → ConNF.PositionedTangles ↑β
• lowerTypedObjects : (β : ConNF.Λ) → [inst : ConNF.LeLevel ↑β] → ConNF.TypedObjects β
• lowerPositionedObjects : ∀ (β : ConNF.Λ) [inst : ConNF.LtLevel ↑β], ConNF.PositionedObjects β

theorem ConNF.FOAData.lowerPositionedObjects [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [self : ConNF.FOAData] (β : ConNF.Λ) [ConNF.LtLevel ↑β] : ConNF.PositionedObjects β

instance ConNF.FOAData.instModelDataSomeΛ [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAData] {β : ConNF.Λ} [ConNF.LeLevel ↑β] : ConNF.ModelData ↑β

Equations

• ConNF.FOAData.instModelDataSomeΛ = ConNF.FOAData.lowerModelData β

instance ConNF.FOAData.instPositionedTanglesSomeΛ [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAData] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] : ConNF.PositionedTangles ↑γ

Equations

• ConNF.FOAData.instPositionedTanglesSomeΛ = ConNF.FOAData.lowerPositionedTangles γ

instance ConNF.FOAData.instTypedObjects [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAData] {β : ConNF.Λ} [ConNF.LeLevel ↑β] : ConNF.TypedObjects β

Equations

• ConNF.FOAData.instTypedObjects = ConNF.FOAData.lowerTypedObjects β

instance ConNF.FOAData.instPositionedObjects [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAData] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] : ConNF.PositionedObjects γ

Equations

• ⋯ = ⋯

instance ConNF.FOAData.leModelData [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAData] (β : ConNF.TypeIndex) [ConNF.LeLevel β] : ConNF.ModelData β

Equations

• ConNF.FOAData.leModelData x✝ = match x✝, x with | none, x => ConNF.Bot.modelData | some β, x => ConNF.FOAData.lowerModelData β

instance ConNF.FOAData.ltPositionedTangles [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAData] (β : ConNF.TypeIndex) [ConNF.LtLevel β] : ConNF.PositionedTangles β

Equations

• ConNF.FOAData.ltPositionedTangles x✝ = match x✝, x with | none, x => ConNF.Bot.positionedTangles | some β, x => ConNF.FOAData.lowerPositionedTangles β

@[simp]

theorem ConNF.Tangle.bot_support [ConNF.Params] (t : ConNF.Tangle ⊥) : t.support = ConNF.Atom.support t

@[simp]

theorem ConNF.Tangle.coe_support [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAData] (β : ConNF.Λ) [ConNF.LeLevel ↑β] (t : ConNF.Tangle ↑β) : t.support = t.support

theorem ConNF.support_supports [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [d : ConNF.FOAData] {β : ConNF.TypeIndex} [i : ConNF.LeLevel β] (t : ConNF.Tangle β) : MulAction.Supports (ConNF.Allowable β) (ConNF.Enumeration.carrier t.support) t

def ConNF.Tangle.set [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] : ConNF.Tangle β → ConNF.TSet β

Equations

• x.set = match x✝¹, x✝, x with | some β, x, t => t.set | none, x, a => a

@[simp]

theorem ConNF.Tangle.bot_set [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAData] (t : ConNF.Tangle ⊥) : t.set = t

@[simp]

theorem ConNF.Tangle.coe_set [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAData] (β : ConNF.Λ) [ConNF.LeLevel ↑β] (t : ConNF.Tangle ↑β) : t.set = t.set

theorem ConNF.Tangle.ext [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [d : ConNF.FOAData] {β : ConNF.TypeIndex} [i : ConNF.LeLevel β] (t₁ : ConNF.Tangle β) (t₂ : ConNF.Tangle β) (hs : t₁.set = t₂.set) (hS : t₁.support = t₂.support) : t₁ = t₂

@[simp]

theorem ConNF.Tangle.smul_set [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [d : ConNF.FOAData] {β : ConNF.TypeIndex} [i : ConNF.LeLevel β] (t : ConNF.Tangle β) (ρ : ConNF.Allowable β) : (ρ • t).set = ρ • t.set

theorem ConNF.FOAAssumptions.ext : ∀ {inst : ConNF.Params} {inst_1 : ConNF.Level} {inst_2 : ConNF.BasePositions} (x y : ConNF.FOAAssumptions), ConNF.FOAData.lowerModelData = ConNF.FOAData.lowerModelData → HEq ConNF.FOAData.lowerPositionedTangles ConNF.FOAData.lowerPositionedTangles → HEq ConNF.FOAData.lowerTypedObjects ConNF.FOAData.lowerTypedObjects → HEq (@ConNF.allowableCons inst inst_1 inst_2 x) (@ConNF.allowableCons inst inst_1 inst_2 y) → x = y

theorem ConNF.FOAAssumptions.ext_iff : ∀ {inst : ConNF.Params} {inst_1 : ConNF.Level} {inst_2 : ConNF.BasePositions} (x y : ConNF.FOAAssumptions), x = y ↔ ConNF.FOAData.lowerModelData = ConNF.FOAData.lowerModelData ∧ HEq ConNF.FOAData.lowerPositionedTangles ConNF.FOAData.lowerPositionedTangles ∧ HEq ConNF.FOAData.lowerTypedObjects ConNF.FOAData.lowerTypedObjects ∧ HEq (@ConNF.allowableCons inst inst_1 inst_2 x) (@ConNF.allowableCons inst inst_1 inst_2 y)

class ConNF.FOAAssumptions [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] extends ConNF.FOAData : Type (u + 1)

Assumptions detailing how the different levels of the tangled structure interact.

• lowerModelData : (β : ConNF.Λ) → [inst : ConNF.LeLevel ↑β] → ConNF.ModelData ↑β
• lowerPositionedTangles : (β : ConNF.Λ) → [inst : ConNF.LtLevel ↑β] → ConNF.PositionedTangles ↑β
• lowerTypedObjects : (β : ConNF.Λ) → [inst : ConNF.LeLevel ↑β] → ConNF.TypedObjects β
• lowerPositionedObjects : ∀ (β : ConNF.Λ) [inst : ConNF.LtLevel ↑β], ConNF.PositionedObjects β
• allowableCons : {β : ConNF.TypeIndex} → [inst : ConNF.LeLevel β] → {γ : ConNF.TypeIndex} → [inst_1 : ConNF.LeLevel γ] → γ < β → ConNF.Allowable β →* ConNF.Allowable γ

  The one-step derivative map between types of allowable permutations. We can think of this map as consing a single morphism on a path.

• allowableCons_eq : ∀ (β : ConNF.TypeIndex) [inst : ConNF.LeLevel β] (γ : ConNF.TypeIndex) [inst_1 : ConNF.LeLevel γ] (hγ : γ < β) (ρ : ConNF.Allowable β), ConNF.Tree.comp (Quiver.Path.nil.cons hγ) (ConNF.Allowable.toStructPerm ρ) = ConNF.Allowable.toStructPerm ((ConNF.allowableCons hγ) ρ)

  The one-step derivative map commutes with toStructPerm.

• pos_lt_pos_atom : ∀ {β : ConNF.Λ} [inst : ConNF.LtLevel ↑β] (t : ConNF.Tangle ↑β) {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom}, { path := A, value := Sum.inl a } ∈ t.support → ConNF.pos a < ConNF.pos t

  If an atom occurs in the support associated to an inflexible litter, it must have position less than the associated tangle.

• pos_lt_pos_nearLitter : ∀ {β : ConNF.Λ} [inst : ConNF.LtLevel ↑β] (t : ConNF.Tangle ↑β) {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter}, { path := A, value := Sum.inr N } ∈ t.support → t.set ≠ ConNF.typedNearLitter N → ConNF.pos N < ConNF.pos t

  If a near-litter occurs in the support associated to an inflexible litter, it must have position less than the associated tangle. The only exception is in the case that the tangle is a typed near-litter.

• smul_fuzz : ∀ {β : ConNF.TypeIndex} [inst : ConNF.LeLevel β] {γ : ConNF.TypeIndex} [inst_1 : ConNF.LtLevel γ] {δ : ConNF.Λ} [inst_2 : ConNF.LtLevel ↑δ] (hγ : γ < β) (hδ : ↑δ < β) (hγδ : γ ≠ ↑δ) (ρ : ConNF.Allowable β) (t : ConNF.Tangle γ), ConNF.Allowable.toStructPerm ρ ((Quiver.Hom.toPath hδ).cons ⋯) • ConNF.fuzz hγδ t = ConNF.fuzz hγδ ((ConNF.allowableCons hγ) ρ • t)

  The fuzz map commutes with allowable permutations.

• allowable_of_smulFuzz : ∀ (β : ConNF.Λ) [inst : ConNF.LeLevel ↑β] (ρs : (γ : ConNF.TypeIndex) → [inst : ConNF.LtLevel γ] → γ < ↑β → ConNF.Allowable γ), (∀ (γ : ConNF.TypeIndex) [inst : ConNF.LtLevel γ] (δ : ConNF.Λ) [inst_1 : 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)) → ∃ (ρ : ConNF.Allowable ↑β), ∀ (γ : ConNF.TypeIndex) [inst_1 : ConNF.LtLevel γ] (hγ : γ < ↑β), (ConNF.allowableCons hγ) ρ = ρs γ hγ

  We can build an β-allowable permutation from a family of allowable permutations at each level γ < β if they commute with the fuzz map.

theorem ConNF.FOAAssumptions.allowableCons_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [self : ConNF.FOAAssumptions] (β : ConNF.TypeIndex) [ConNF.LeLevel β] (γ : ConNF.TypeIndex) [ConNF.LeLevel γ] (hγ : γ < β) (ρ : ConNF.Allowable β) : ConNF.Tree.comp (Quiver.Path.nil.cons hγ) (ConNF.Allowable.toStructPerm ρ) = ConNF.Allowable.toStructPerm ((ConNF.allowableCons hγ) ρ)

The one-step derivative map commutes with toStructPerm.

theorem ConNF.FOAAssumptions.pos_lt_pos_atom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [self : ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LtLevel ↑β] (t : ConNF.Tangle ↑β) {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} : { path := A, value := Sum.inl a } ∈ t.support → ConNF.pos a < ConNF.pos t

If an atom occurs in the support associated to an inflexible litter, it must have position less than the associated tangle.

theorem ConNF.FOAAssumptions.pos_lt_pos_nearLitter [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [self : ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LtLevel ↑β] (t : ConNF.Tangle ↑β) {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter} : { path := A, value := Sum.inr N } ∈ t.support → t.set ≠ ConNF.typedNearLitter N → ConNF.pos N < ConNF.pos t

If a near-litter occurs in the support associated to an inflexible litter, it must have position less than the associated tangle. The only exception is in the case that the tangle is a typed near-litter.

theorem ConNF.FOAAssumptions.smul_fuzz [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [self : ConNF.FOAAssumptions] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {δ : ConNF.Λ} [ConNF.LtLevel ↑δ] (hγ : γ < β) (hδ : ↑δ < β) (hγδ : γ ≠ ↑δ) (ρ : ConNF.Allowable β) (t : ConNF.Tangle γ) : ConNF.Allowable.toStructPerm ρ ((Quiver.Hom.toPath hδ).cons ⋯) • ConNF.fuzz hγδ t = ConNF.fuzz hγδ ((ConNF.allowableCons hγ) ρ • t)

The fuzz map commutes with allowable permutations.

theorem ConNF.FOAAssumptions.allowable_of_smulFuzz [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [self : ConNF.FOAAssumptions] (β : ConNF.Λ) [ConNF.LeLevel ↑β] (ρs : (γ : ConNF.TypeIndex) → [inst : ConNF.LtLevel γ] → γ < ↑β → ConNF.Allowable γ) : (∀ (γ : ConNF.TypeIndex) [inst : ConNF.LtLevel γ] (δ : ConNF.Λ) [inst_1 : 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)) → ∃ (ρ : ConNF.Allowable ↑β), ∀ (γ : ConNF.TypeIndex) [inst : ConNF.LtLevel γ] (hγ : γ < ↑β), (ConNF.allowableCons hγ) ρ = ρs γ hγ

We can build an β-allowable permutation from a family of allowable permutations at each level γ < β if they commute with the fuzz map.

def ConNF.Allowable.comp' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {γ : ConNF.TypeIndex} (A : Quiver.Path β γ) : let x := ⋯; ConNF.Allowable β →* ConNF.Allowable γ

A primitive version of Allowable.comp with different arguments. This is always the wrong spelling to use.

Equations

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

def ConNF.Allowable.comp [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} [ConNF.LeLevel β] [ConNF.LeLevel γ] (A : Quiver.Path β γ) : ConNF.Allowable β →* ConNF.Allowable γ

Define the full derivative map on allowable permutations by recursion along paths. This agrees with Tree.comp, but yields allowable permutations. Note that the LeLevel γ hypothesis is technically redundant, but is used to give us more direct access to Allowable γ. In practice, we already have this assumption wherever we use Allowable.comp.

Equations

• ConNF.Allowable.comp A = ConNF.Allowable.comp' A

We prove that Allowable.comp is functorial. In addition, we prove a number of lemmas about FOAAssumptions.

@[simp]

theorem ConNF.Allowable.comp_nil [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} [ConNF.LeLevel β] : ConNF.Allowable.comp Quiver.Path.nil = MonoidHom.id (ConNF.Allowable β)

@[simp]

theorem ConNF.Allowable.comp_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} [ConNF.LeLevel β] [ConNF.LeLevel γ] (h : γ < β) : ConNF.allowableCons h = ConNF.Allowable.comp (Quiver.Path.nil.cons h)

@[simp]

theorem ConNF.Allowable.comp_cons [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} {δ : ConNF.TypeIndex} [ConNF.LeLevel β] [ConNF.LeLevel γ] [ConNF.LeLevel δ] (A : Quiver.Path β γ) (h : δ < γ) : (ConNF.allowableCons h).comp (ConNF.Allowable.comp A) = ConNF.Allowable.comp (A.cons h)

@[simp]

theorem ConNF.Allowable.comp_cons_apply [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} {δ : ConNF.TypeIndex} [ConNF.LeLevel β] [ConNF.LeLevel γ] [ConNF.LeLevel δ] (A : Quiver.Path β γ) (h : δ < γ) (π : ConNF.Allowable β) : (ConNF.allowableCons h) ((ConNF.Allowable.comp A) π) = (ConNF.Allowable.comp (A.cons h)) π

@[simp]

theorem ConNF.Allowable.comp_comp_apply [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} {δ : ConNF.TypeIndex} [ConNF.LeLevel β] [ConNF.LeLevel γ] [i : ConNF.LeLevel δ] (A : Quiver.Path β γ) (B : Quiver.Path γ δ) (π : ConNF.Allowable β) : (ConNF.Allowable.comp B) ((ConNF.Allowable.comp A) π) = (ConNF.Allowable.comp (A.comp B)) π

@[simp]

theorem ConNF.Allowable.toStructPerm_comp [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} [ConNF.LeLevel β] [i : ConNF.LeLevel γ] (A : Quiver.Path β γ) (π : ConNF.Allowable β) : ConNF.Allowable.toStructPerm ((ConNF.Allowable.comp A) π) = ConNF.Tree.comp A (ConNF.Allowable.toStructPerm π)

@[simp]

theorem ConNF.Allowable.toStructPerm_apply [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (A : Quiver.Path β ⊥) (π : ConNF.Allowable β) : BasePerm.ofBot ((ConNF.Allowable.comp A) π) = ConNF.Allowable.toStructPerm π A

theorem ConNF.Allowable.comp_bot [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (A : Quiver.Path β ⊥) (ρ : ConNF.Allowable β) : (ConNF.Allowable.comp A) ρ = ConNF.Allowable.toStructPerm ρ A

@[simp]

theorem ConNF.smul_support [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (t : ConNF.Tangle ↑β) (ρ : ConNF.Allowable ↑β) : (ρ • t).support = ρ • t.support

theorem ConNF.smul_mem_support [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {c : ConNF.Address ↑β} {t : ConNF.Tangle ↑β} (h : c ∈ t.support) (π : ConNF.Allowable ↑β) : π • c ∈ (π • t).support

@[simp]

theorem ConNF.BasePerm.ofBot_comp' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {hβ : ⊥ < β} {ρ : ConNF.Allowable β} : BasePerm.ofBot ((ConNF.allowableCons hβ) ρ) = ConNF.Allowable.toStructPerm ρ (Quiver.Hom.toPath hβ)

@[simp]

theorem ConNF.ofBot_smul [ConNF.Params] {X : Type u_1} [MulAction ConNF.BasePerm X] (π : ConNF.Allowable ⊥) (x : X) : π • x = BasePerm.ofBot π • x

@[simp]

theorem ConNF.comp_bot_smul_atom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (ρ : ConNF.Allowable β) (A : Quiver.Path β ⊥) (a : ConNF.Tangle ⊥) : (ConNF.Allowable.comp A) ρ • a = ConNF.Allowable.toStructPerm ρ A • let_fun this := a; this

We now show some different spellings of the theorem that allowable permutations commute with the fuzz maps.

theorem ConNF.toStructPerm_smul_fuzz' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {δ : ConNF.Λ} [ConNF.LtLevel ↑δ] (hγ : γ < β) (hδ : ↑δ < β) (hγδ : γ ≠ ↑δ) (ρ : ConNF.Allowable β) (t : ConNF.Tangle γ) : ConNF.Allowable.toStructPerm ρ ((Quiver.Path.nil.cons hδ).cons ⋯) • ConNF.fuzz hγδ t = ConNF.fuzz hγδ ((ConNF.allowableCons hγ) ρ • t)

@[simp]

theorem ConNF.toStructPerm_smul_fuzz [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {γ : ConNF.TypeIndex} [ConNF.LeLevel γ] {δ : ConNF.TypeIndex} [ConNF.LtLevel δ] {ε : ConNF.Λ} [ConNF.LtLevel ↑ε] (hδ : δ < γ) (hε : ↑ε < γ) (hδε : δ ≠ ↑ε) (A : Quiver.Path β γ) (ρ : ConNF.Allowable β) (t : ConNF.Tangle δ) : ConNF.Allowable.toStructPerm ρ ((A.cons hε).cons ⋯) • ConNF.fuzz hδε t = ConNF.fuzz hδε ((ConNF.Allowable.comp (A.cons hδ)) ρ • t)