Documentation

ConNF.Model.MainInduction

theorem ConNF.MainInduction.Tang.ext :

∀ {inst : ConNF.Params} {α : ConNF.Λ} {TSet Allowable : Type u} {inst_1 : Group Allowable} {inst_2 : MulAction Allowable TSet} {inst_3 : MulAction Allowable (ConNF.Address ↑α)} (x y : ConNF.MainInduction.Tang α TSet Allowable), x.set = y.set → x.support = y.support → x = y

theorem ConNF.MainInduction.Tang.ext_iff :

∀ {inst : ConNF.Params} {α : ConNF.Λ} {TSet Allowable : Type u} {inst_1 : Group Allowable} {inst_2 : MulAction Allowable TSet} {inst_3 : MulAction Allowable (ConNF.Address ↑α)} (x y : ConNF.MainInduction.Tang α TSet Allowable), x = y ↔ x.set = y.set ∧ x.support = y.support

structure ConNF.MainInduction.Tang [ConNF.Params] (α : ConNF.Λ) (TSet : Type u) (Allowable : Type u) [Group Allowable] [MulAction Allowable TSet] [MulAction Allowable (ConNF.Address ↑α)] :

set : TSet
support : ConNF.Support ↑α
support_supports : MulAction.Supports Allowable (ConNF.Enumeration.carrier self.support) self.set

Instances For

theorem ConNF.MainInduction.Tang.support_supports [ConNF.Params] {α : ConNF.Λ} {TSet : Type u} {Allowable : Type u} [Group Allowable] [MulAction Allowable TSet] [MulAction Allowable (ConNF.Address ↑α)] (self : ConNF.MainInduction.Tang α TSet Allowable) :

MulAction.Supports Allowable (ConNF.Enumeration.carrier self.support) self.set

structure ConNF.MainInduction.IH [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) :

Type (u + 1)

The data for the main inductive hypothesis, containing the things we need to construct at each level α.

TSet : Type u
Allowable : Type u
allowableGroup : Group self.Allowable
allowableToStructPerm : self.Allowable →* ConNF.StructPerm ↑α
allowableToStructPerm_injective : Function.Injective ⇑self.allowableToStructPerm
We make this assumption for convenience, since it makes IHProp into a subsingleton, and so we can encode it as a Prop.
allowableAction : MulAction self.Allowable self.TSet
has_support : ∀ (t : self.TSet), ∃ (S : ConNF.Support ↑α), MulAction.Supports self.Allowable (ConNF.Enumeration.carrier S) t
pos : ConNF.MainInduction.Tang α self.TSet self.Allowable ↪ ConNF.μ
typedNearLitter : ConNF.NearLitter ↪ self.TSet
pos_typedNearLitter : ∀ (N : ConNF.NearLitter) (t : ConNF.MainInduction.Tang α self.TSet self.Allowable), t.set = self.typedNearLitter N → ConNF.pos N ≤ self.pos t
smul_typedNearLitter : ∀ (ρ : self.Allowable) (N : ConNF.NearLitter), ρ • self.typedNearLitter N = self.typedNearLitter (self.allowableToStructPerm ρ (Quiver.Hom.toPath ⋯) • N)
toStructSet : self.TSet ↪ ConNF.StructSet ↑α
toStructSet_smul : ∀ (ρ : self.Allowable) (t : self.TSet), self.toStructSet (ρ • t) = ρ • self.toStructSet t

Instances For

theorem ConNF.MainInduction.IH.allowableToStructPerm_injective [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} (self : ConNF.MainInduction.IH α) :

Function.Injective ⇑self.allowableToStructPerm

We make this assumption for convenience, since it makes IHProp into a subsingleton, and so we can encode it as a Prop.

theorem ConNF.MainInduction.IH.has_support [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} (self : ConNF.MainInduction.IH α) (t : self.TSet) :

∃ (S : ConNF.Support ↑α), MulAction.Supports self.Allowable (ConNF.Enumeration.carrier S) t

theorem ConNF.MainInduction.IH.pos_typedNearLitter [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} (self : ConNF.MainInduction.IH α) (N : ConNF.NearLitter) (t : ConNF.MainInduction.Tang α self.TSet self.Allowable) :

t.set = self.typedNearLitter N → ConNF.pos N ≤ self.pos t

theorem ConNF.MainInduction.IH.smul_typedNearLitter [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} (self : ConNF.MainInduction.IH α) (ρ : self.Allowable) (N : ConNF.NearLitter) :

ρ • self.typedNearLitter N = self.typedNearLitter (self.allowableToStructPerm ρ (Quiver.Hom.toPath ⋯) • N)

theorem ConNF.MainInduction.IH.toStructSet_smul [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} (self : ConNF.MainInduction.IH α) (ρ : self.Allowable) (t : self.TSet) :

self.toStructSet (ρ • t) = ρ • self.toStructSet t

instance ConNF.MainInduction.instGroupAllowable [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : ConNF.MainInduction.IH α} :

Group ih.Allowable

Equations

ConNF.MainInduction.instGroupAllowable = ih.allowableGroup

instance ConNF.MainInduction.instMulActionAllowableTSet [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : ConNF.MainInduction.IH α} :

MulAction ih.Allowable ih.TSet

Equations

ConNF.MainInduction.instMulActionAllowableTSet = ih.allowableAction

instance ConNF.MainInduction.instMulActionAllowableOfStructPermSomeΛ [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : ConNF.MainInduction.IH α} {X : Type u_1} [MulAction (ConNF.StructPerm ↑α) X] :

MulAction ih.Allowable X

Equations

ConNF.MainInduction.instMulActionAllowableOfStructPermSomeΛ = MulAction.compHom X ih.allowableToStructPerm

def ConNF.MainInduction.IH.modelData [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} (ih : ConNF.MainInduction.IH α) :

ConNF.ModelData ↑α

Equations

ih.modelData = ConNF.ModelData.mk ih.TSet ih.Allowable ih.allowableToStructPerm ⋯ ⋯ ih.toStructSet ⋯

Instances For

def ConNF.MainInduction.IH.Tangle [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} (ih : ConNF.MainInduction.IH α) :

Equations

ih.Tangle = ConNF.Tangle ↑α

Instances For

instance ConNF.MainInduction.instMulActionAllowableTangle [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : ConNF.MainInduction.IH α} :

MulAction ih.Allowable ih.Tangle

Equations

ConNF.MainInduction.instMulActionAllowableTangle = inferInstanceAs (MulAction (ConNF.Allowable ↑α) (ConNF.Tangle ↑α))

instance ConNF.MainInduction.instMulActionAllowableTangleSomeΛ [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : ConNF.MainInduction.IH α} :

MulAction ih.Allowable (ConNF.Tangle ↑α)

Equations

ConNF.MainInduction.instMulActionAllowableTangleSomeΛ = inferInstanceAs (MulAction (ConNF.Allowable ↑α) (ConNF.Tangle ↑α))

def ConNF.MainInduction.IH.tangleEquiv [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} (ih : ConNF.MainInduction.IH α) :

ConNF.Tangle ↑α ≃ ConNF.MainInduction.Tang α ih.TSet ih.Allowable

Equations

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

Instances For

def ConNF.MainInduction.IH.positionedTangles [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} (ih : ConNF.MainInduction.IH α) :

ConNF.PositionedTangles ↑α

Equations

ih.positionedTangles = { pos := { toFun := fun (t : ConNF.Tangle ↑α) => ih.pos (ih.tangleEquiv t), inj' := ⋯ } }

Instances For

def ConNF.MainInduction.IH.typedObjects [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} (ih : ConNF.MainInduction.IH α) :

ConNF.TypedObjects α

Equations

ih.typedObjects = { typedNearLitter := ih.typedNearLitter, smul_typedNearLitter := ⋯ }

Instances For

@[simp]

theorem ConNF.MainInduction.IH.pos_tangleEquiv [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} (ih : ConNF.MainInduction.IH α) (t : ConNF.Tangle ↑α) :

ConNF.pos t = ih.pos (ih.tangleEquiv t)

theorem ConNF.MainInduction.IH.positionedObjects [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} (ih : ConNF.MainInduction.IH α) :

ConNF.PositionedObjects α

noncomputable def ConNF.MainInduction.fuzz' [ConNF.Params] [ConNF.BasePositions] {β : ConNF.Λ} {γ : ConNF.Λ} (ihβ : ConNF.MainInduction.IH β) (ihγ : ConNF.MainInduction.IH γ) (h : ↑β ≠ ↑γ) :

ConNF.Tangle ↑β → ConNF.Litter

A renaming of fuzz that uses only data from the IHs.

Equations

ConNF.MainInduction.fuzz' ihβ ihγ h = ConNF.fuzz h

Instances For

noncomputable def ConNF.MainInduction.fuzz'Bot [ConNF.Params] [ConNF.BasePositions] {γ : ConNF.Λ} (ihγ : ConNF.MainInduction.IH γ) :

ConNF.Atom → ConNF.Litter

A renaming of fuzz that uses only data from the IHs.

Equations

ConNF.MainInduction.fuzz'Bot ihγ = ConNF.fuzz ⋯

Instances For

def ConNF.MainInduction.modelDataStep [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) :

ConNF.ModelData ↑α

Equations

ConNF.MainInduction.modelDataStep α ihs = ConNF.ModelData.mk ConNF.NewTSet ConNF.NewAllowable ConNF.NewAllowable.toStructPerm ⋯ ⋯ { toFun := ConNF.NewTSet.toStructSet, inj' := ⋯ } ⋯

Instances For

def ConNF.MainInduction.typedObjectsStep [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) :

ConNF.TypedObjects α

Equations

ConNF.MainInduction.typedObjectsStep α ihs = { typedNearLitter := { toFun := ConNF.newTypedNearLitter, inj' := ⋯ }, smul_typedNearLitter := ⋯ }

Instances For

noncomputable def ConNF.MainInduction.modelDataStepFn [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β ≤ α) :

ConNF.ModelData ↑β

Equations

ConNF.MainInduction.modelDataStepFn α ihs β hβ = if hβ' : β = α then ⋯ ▸ ConNF.MainInduction.modelDataStep α ihs else (ihs β ⋯).modelData

Instances For

theorem ConNF.MainInduction.modelDataStepFn_eq [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) :

ConNF.MainInduction.modelDataStepFn α ihs α ⋯ = ConNF.MainInduction.modelDataStep α ihs

theorem ConNF.MainInduction.modelDataStepFn_lt [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) :

ConNF.MainInduction.modelDataStepFn α ihs β ⋯ = (ihs β hβ).modelData

noncomputable def ConNF.MainInduction.typedObjectsStepFn [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β ≤ α) :

ConNF.TypedObjects β

Equations

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

Instances For

theorem ConNF.MainInduction.typedObjectsStepFn_lt [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) :

ConNF.MainInduction.typedObjectsStepFn α ihs β ⋯ = cast ⋯ (ihs β hβ).typedObjects

noncomputable def ConNF.MainInduction.buildStepFOAData [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) :

ConNF.FOAData

Equations

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

Instances For

theorem ConNF.MainInduction.buildStepFOAData_positioned_lt [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) :

HEq (ConNF.FOAData.lowerPositionedTangles β) (ihs β hβ).positionedTangles

theorem ConNF.MainInduction.foaData_tSet_eq [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) :

ConNF.TSet ↑α = ConNF.NewTSet

def ConNF.MainInduction.foaData_tSet_eq_equiv [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) :

ConNF.TSet ↑α ≃ ConNF.NewTSet

Equations

ConNF.MainInduction.foaData_tSet_eq_equiv α ihs = Equiv.cast ⋯

Instances For

theorem ConNF.MainInduction.foaData_tSet_lt [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) :

ConNF.TSet ↑β = (ihs β hβ).TSet

def ConNF.MainInduction.foaData_tSet_lt_equiv [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) :

ConNF.TSet ↑β ≃ (ihs β hβ).TSet

Equations

ConNF.MainInduction.foaData_tSet_lt_equiv α ihs β hβ = Equiv.cast ⋯

Instances For

theorem ConNF.MainInduction.foaData_tangle_lt [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) :

ConNF.Tangle ↑β = ConNF.Tangle ↑β

def ConNF.MainInduction.foaData_tangle_lt_equiv [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) :

ConNF.Tangle ↑β ≃ ConNF.Tangle ↑β

Equations

ConNF.MainInduction.foaData_tangle_lt_equiv α ihs β hβ = Equiv.cast ⋯

Instances For

theorem ConNF.MainInduction.foaData_allowable_eq [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) :

ConNF.Allowable ↑α = ConNF.NewAllowable

def ConNF.MainInduction.foaData_allowable_eq_equiv [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) :

ConNF.Allowable ↑α ≃ ConNF.NewAllowable

Equations

ConNF.MainInduction.foaData_allowable_eq_equiv α ihs = Equiv.cast ⋯

Instances For

theorem ConNF.MainInduction.modelData_cast_one [ConNF.Params] (α : ConNF.Λ) (i₁ : ConNF.ModelData ↑α) (i₂ : ConNF.ModelData ↑α) (h : i₁ = i₂) :

cast ⋯ One.one = One.one

theorem ConNF.MainInduction.modelData_cast_mul [ConNF.Params] (α : ConNF.Λ) (i₁ : ConNF.ModelData ↑α) (i₂ : ConNF.ModelData ↑α) (h : i₁ = i₂) (ρ₁ : ConNF.Allowable ↑α) (ρ₂ : ConNF.Allowable ↑α) :

cast ⋯ (Mul.mul ρ₁ ρ₂) = Mul.mul (cast ⋯ ρ₁) (cast ⋯ ρ₂)

theorem ConNF.MainInduction.modelData_cast_toStructPerm [ConNF.Params] (α : ConNF.Λ) (i₁ : ConNF.ModelData ↑α) (i₂ : ConNF.ModelData ↑α) (h : i₁ = i₂) (ρ : ConNF.Allowable ↑α) :

ConNF.ModelData.allowableToStructPerm ρ = ConNF.ModelData.allowableToStructPerm (cast ⋯ ρ)

theorem ConNF.MainInduction.modelData_cast_toStructSet [ConNF.Params] (α : ConNF.Λ) (i₁ : ConNF.ModelData ↑α) (i₂ : ConNF.ModelData ↑α) (h : i₁ = i₂) (t : ConNF.TSet ↑α) :

ConNF.toStructSet t = ConNF.toStructSet (cast ⋯ t)

theorem ConNF.MainInduction.modelData_cast_smul [ConNF.Params] (α : ConNF.Λ) (i₁ : ConNF.ModelData ↑α) (i₂ : ConNF.ModelData ↑α) (h : i₁ = i₂) (ρ : ConNF.Allowable ↑α) (t : ConNF.TSet ↑α) :

cast ⋯ (SMul.smul ρ t) = SMul.smul (cast ⋯ ρ) (cast ⋯ t)

theorem ConNF.MainInduction.modelData_cast_smul' [ConNF.Params] (α : ConNF.Λ) (i₁ : ConNF.ModelData ↑α) (i₂ : ConNF.ModelData ↑α) (h : i₁ = i₂) (ρ : ConNF.Allowable ↑α) (t : ConNF.Tangle ↑α) :

cast ⋯ (SMul.smul ρ t) = SMul.smul (cast ⋯ ρ) (cast ⋯ t)

theorem ConNF.MainInduction.modelData_cast_set [ConNF.Params] (α : ConNF.Λ) (i₁ : ConNF.ModelData ↑α) (i₂ : ConNF.ModelData ↑α) (hi : i₁ = i₂) (t : ConNF.TangleCoe α) :

cast ⋯ t.set = (cast ⋯ t).set

theorem ConNF.MainInduction.modelData_cast_support [ConNF.Params] (α : ConNF.Λ) (i₁ : ConNF.ModelData ↑α) (i₂ : ConNF.ModelData ↑α) (hi : i₁ = i₂) (t : ConNF.Tangle ↑α) :

t.support = (cast ⋯ t).support

theorem ConNF.MainInduction.positionedTangles_cast_pos [ConNF.Params] (α : ConNF.Λ) (i₁ : ConNF.ModelData ↑α) (i₂ : ConNF.ModelData ↑α) (hi : i₁ = i₂) (j₁ : ConNF.PositionedTangles ↑α) (j₂ : ConNF.PositionedTangles ↑α) (hj : HEq j₁ j₂) (t : ConNF.Tangle ↑α) :

ConNF.pos t = ConNF.pos (cast ⋯ t)

theorem ConNF.MainInduction.typedObjects_cast_typedNearLitter [ConNF.Params] (α : ConNF.Λ) (i₁ : ConNF.ModelData ↑α) (i₂ : ConNF.ModelData ↑α) (hi : i₁ = i₂) (j₁ : ConNF.TypedObjects α) (j₂ : ConNF.TypedObjects α) (hj : HEq j₁ j₂) (N : ConNF.NearLitter) :

ConNF.typedNearLitter N = cast ⋯ (ConNF.typedNearLitter N)

theorem ConNF.MainInduction.fuzz_cast [ConNF.Params] [ConNF.BasePositions] (β : ConNF.TypeIndex) (γ : ConNF.Λ) (hβγ : β ≠ ↑γ) (i₁ : ConNF.ModelData β) (i₂ : ConNF.ModelData β) (hi : i₁ = i₂) (j₁ : ConNF.PositionedTangles β) (j₂ : ConNF.PositionedTangles β) (hj : HEq j₁ j₂) (t : ConNF.Tangle β) :

ConNF.fuzz hβγ t = ConNF.fuzz hβγ (cast ⋯ t)

@[simp]

theorem ConNF.MainInduction.foaData_tSet_eq_equiv_toStructSet [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (t : ConNF.TSet ↑ConNF.α) :

ConNF.toStructSet t = ((ConNF.MainInduction.foaData_tSet_eq_equiv α ihs) t).toStructSet

@[simp]

theorem ConNF.MainInduction.foaData_allowable_eq_equiv_one [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) :

(ConNF.MainInduction.foaData_allowable_eq_equiv α ihs) 1 = 1

@[simp]

theorem ConNF.MainInduction.foaData_allowable_eq_equiv_mul [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (ρ₁ : ConNF.Allowable ↑α) (ρ₂ : ConNF.Allowable ↑α) :

(ConNF.MainInduction.foaData_allowable_eq_equiv α ihs) (ρ₁ * ρ₂) = (ConNF.MainInduction.foaData_allowable_eq_equiv α ihs) ρ₁ * (ConNF.MainInduction.foaData_allowable_eq_equiv α ihs) ρ₂

@[simp]

theorem ConNF.MainInduction.foaData_allowable_eq_equiv_toStructPerm [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (ρ : ConNF.Allowable ↑α) :

ConNF.Allowable.toStructPerm ρ = ConNF.NewAllowable.toStructPerm ((ConNF.MainInduction.foaData_allowable_eq_equiv α ihs) ρ)

@[simp]

theorem ConNF.MainInduction.foaData_allowable_eq_equiv_smul [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (ρ : ConNF.Allowable ↑α) (t : ConNF.TSet ↑α) :

(ConNF.MainInduction.foaData_tSet_eq_equiv α ihs) (ρ • t) = (ConNF.MainInduction.foaData_allowable_eq_equiv α ihs) ρ • (ConNF.MainInduction.foaData_tSet_eq_equiv α ihs) t

@[simp]

theorem ConNF.MainInduction.foaData_tSet_lt_equiv_toStructSet [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) (t : ConNF.TSet ↑β) :

ConNF.toStructSet t = (ihs β hβ).toStructSet ((ConNF.MainInduction.foaData_tSet_lt_equiv α ihs β hβ) t)

@[simp]

theorem ConNF.MainInduction.foaData_tSet_lt_equiv_toStructSet' [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) (t : ConNF.TSet ↑β) :

ConNF.toStructSet t = ConNF.toStructSet ((ConNF.MainInduction.foaData_tSet_lt_equiv α ihs β hβ) t)

theorem ConNF.MainInduction.foaData_allowable_lt [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) :

ConNF.Allowable ↑β = (ihs β hβ).Allowable

def ConNF.MainInduction.foaData_allowable_lt_equiv [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) :

ConNF.Allowable ↑β ≃ (ihs β hβ).Allowable

Equations

ConNF.MainInduction.foaData_allowable_lt_equiv α ihs β hβ = Equiv.cast ⋯

Instances For

@[simp]

theorem ConNF.MainInduction.foaData_allowable_lt_equiv_one [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) :

(ConNF.MainInduction.foaData_allowable_lt_equiv α ihs β hβ) 1 = 1

@[simp]

theorem ConNF.MainInduction.foaData_allowable_lt_equiv_mul [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) (ρ₁ : ConNF.Allowable ↑β) (ρ₂ : ConNF.Allowable ↑β) :

(ConNF.MainInduction.foaData_allowable_lt_equiv α ihs β hβ) (ρ₁ * ρ₂) = (ConNF.MainInduction.foaData_allowable_lt_equiv α ihs β hβ) ρ₁ * (ConNF.MainInduction.foaData_allowable_lt_equiv α ihs β hβ) ρ₂

@[simp]

theorem ConNF.MainInduction.foaData_allowable_lt_equiv_toStructPerm [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) (ρ : ConNF.Allowable ↑β) :

ConNF.Allowable.toStructPerm ρ = ConNF.Allowable.toStructPerm ((ConNF.MainInduction.foaData_allowable_lt_equiv α ihs β hβ) ρ)

@[simp]

theorem ConNF.MainInduction.foaData_allowable_lt_equiv_smul [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) (ρ : ConNF.Allowable ↑β) (t : ConNF.TSet ↑β) :

(ConNF.MainInduction.foaData_tSet_lt_equiv α ihs β hβ) (ρ • t) = (ConNF.MainInduction.foaData_allowable_lt_equiv α ihs β hβ) ρ • (ConNF.MainInduction.foaData_tSet_lt_equiv α ihs β hβ) t

@[simp]

theorem ConNF.MainInduction.foaData_allowable_lt_equiv_smul' [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) (ρ : ConNF.Allowable ↑β) (t : ConNF.Tangle ↑β) :

(ConNF.MainInduction.foaData_tangle_lt_equiv α ihs β hβ) (ρ • t) = (ConNF.MainInduction.foaData_allowable_lt_equiv α ihs β hβ) ρ • (ConNF.MainInduction.foaData_tangle_lt_equiv α ihs β hβ) t

theorem ConNF.MainInduction.foaData_tangle_lt_set [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) (t : ConNF.TangleCoe β) :

(ConNF.MainInduction.foaData_tSet_lt_equiv α ihs β hβ) t.set = (let_fun this := (ConNF.MainInduction.foaData_tangle_lt_equiv α ihs β hβ) t; this).set

theorem ConNF.MainInduction.foaData_tangle_lt_support [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) (t : ConNF.Tangle ↑β) :

t.support = ((ConNF.MainInduction.foaData_tangle_lt_equiv α ihs β hβ) t).support

@[simp]

theorem ConNF.MainInduction.foaData_tSet_lt_equiv_pos [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) (t : ConNF.Tangle ↑β) :

ConNF.pos t = (ihs β hβ).pos ((ihs β hβ).tangleEquiv ((ConNF.MainInduction.foaData_tangle_lt_equiv α ihs β hβ) t))

@[simp]

theorem ConNF.MainInduction.foaData_tSet_lt_equiv_typedNearLitter [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) (N : ConNF.NearLitter) :

ConNF.typedNearLitter N = (ConNF.MainInduction.foaData_tSet_lt_equiv α ihs β hβ).symm ((ihs β hβ).typedNearLitter N)

@[simp]

theorem ConNF.MainInduction.foaData_tangle_lt_equiv_fuzz [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) (γ : ConNF.Λ) (hβγ : ↑β ≠ ↑γ) (t : ConNF.Tangle ↑β) :

ConNF.fuzz hβγ t = ConNF.fuzz hβγ ((ConNF.MainInduction.foaData_tangle_lt_equiv α ihs β hβ) t)

theorem ConNF.MainInduction.foaData_allowable_bot [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) :

ConNF.Allowable ⊥ = ConNF.BasePerm

theorem ConNF.MainInduction.foaData_allowable_lt' [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.TypeIndex) (hβ : β < ↑α) :

ConNF.Allowable β = ConNF.Allowable β

def ConNF.MainInduction.foaData_allowable_lt'_equiv [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.TypeIndex) (hβ : β < ↑α) :

ConNF.Allowable β ≃ ConNF.Allowable β

Equations

ConNF.MainInduction.foaData_allowable_lt'_equiv α ihs β hβ = Equiv.cast ⋯

Instances For

theorem ConNF.MainInduction.foaData_tSet_lt' [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.TypeIndex) (hβ : β < ↑α) :

ConNF.TSet β = ConNF.TSet β

def ConNF.MainInduction.foaData_tSet_lt'_equiv [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.TypeIndex) (hβ : β < ↑α) :

ConNF.TSet β ≃ ConNF.TSet β

Equations

ConNF.MainInduction.foaData_tSet_lt'_equiv α ihs β hβ = Equiv.cast ⋯

Instances For

theorem ConNF.MainInduction.foaData_tangle_lt' [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.TypeIndex) (hβ : β < ↑α) :

ConNF.Tangle β = ConNF.Tangle β

def ConNF.MainInduction.foaData_tangle_lt'_equiv [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.TypeIndex) (hβ : β < ↑α) :

ConNF.Tangle β ≃ ConNF.Tangle β

Equations

ConNF.MainInduction.foaData_tangle_lt'_equiv α ihs β hβ = Equiv.cast ⋯

Instances For

@[simp]

def ConNF.MainInduction.foaData_allowable_lt'_equiv_eq_lt_equiv [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) :

ConNF.MainInduction.foaData_allowable_lt'_equiv α ihs ↑β ⋯ = ConNF.MainInduction.foaData_allowable_lt_equiv α ihs β hβ

Equations

⋯ = ⋯

Instances For

@[simp]

def ConNF.MainInduction.foaData_allowable_lt'_equiv_eq_refl [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) :

ConNF.MainInduction.foaData_allowable_lt'_equiv α ihs ⊥ ⋯ = Equiv.refl (ConNF.Allowable ⊥)

Equations

⋯ = ⋯

Instances For

@[simp]

def ConNF.MainInduction.foaData_tangle_lt'_equiv_eq_lt_equiv [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.Λ) (hβ : β < α) :

ConNF.MainInduction.foaData_tangle_lt'_equiv α ihs ↑β ⋯ = ConNF.MainInduction.foaData_tangle_lt_equiv α ihs β hβ

Equations

⋯ = ⋯

Instances For

@[simp]

def ConNF.MainInduction.foaData_tangle_lt'_equiv_eq_refl [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) :

ConNF.MainInduction.foaData_tangle_lt'_equiv α ihs ⊥ ⋯ = Equiv.refl (ConNF.Tangle ⊥)

Equations

⋯ = ⋯

Instances For

@[simp]

theorem ConNF.MainInduction.foaData_allowable_lt'_equiv_one [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.TypeIndex) (hβ : β < ↑α) :

(ConNF.MainInduction.foaData_allowable_lt'_equiv α ihs β hβ) 1 = 1

@[simp]

theorem ConNF.MainInduction.foaData_allowable_lt'_equiv_mul [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.TypeIndex) (hβ : β < ↑α) (ρ₁ : ConNF.Allowable β) (ρ₂ : ConNF.Allowable β) :

(ConNF.MainInduction.foaData_allowable_lt'_equiv α ihs β hβ) (ρ₁ * ρ₂) = (ConNF.MainInduction.foaData_allowable_lt'_equiv α ihs β hβ) ρ₁ * (ConNF.MainInduction.foaData_allowable_lt'_equiv α ihs β hβ) ρ₂

@[simp]

theorem ConNF.MainInduction.foaData_allowable_lt'_equiv_toStructPerm [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.TypeIndex) (hβ : β < ↑α) (ρ : ConNF.Allowable β) :

ConNF.Allowable.toStructPerm ρ = ConNF.Allowable.toStructPerm ((ConNF.MainInduction.foaData_allowable_lt'_equiv α ihs β hβ) ρ)

@[simp]

theorem ConNF.MainInduction.foaData_allowable_lt'_equiv_smul [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.TypeIndex) (hβ : β < ↑α) (ρ : ConNF.Allowable β) (t : ConNF.Tangle β) :

(ConNF.MainInduction.foaData_tangle_lt'_equiv α ihs β hβ) (ρ • t) = (ConNF.MainInduction.foaData_allowable_lt'_equiv α ihs β hβ) ρ • (ConNF.MainInduction.foaData_tangle_lt'_equiv α ihs β hβ) t

@[simp]

theorem ConNF.MainInduction.foaData_tangle_lt'_equiv_fuzz [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (β : ConNF.TypeIndex) (hβ : β < ↑α) (γ : ConNF.Λ) (hβγ : β ≠ ↑γ) (t : ConNF.Tangle β) :

ConNF.fuzz hβγ t = ConNF.fuzz hβγ ((ConNF.MainInduction.foaData_tangle_lt'_equiv α ihs β hβ) t)

structure ConNF.MainInduction.IHProp [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ih : (β : ConNF.Λ) → β ≤ α → ConNF.MainInduction.IH β) :

The hypotheses on how IH relates to previous IHs.

canCons : ∀ (β : ConNF.Λ) (hβ : β < α), ∃ (f : (ih α ⋯).Allowable →* (ih β ⋯).Allowable), ∀ (ρ : (ih α ⋯).Allowable), ConNF.Tree.comp (Quiver.Hom.toPath ⋯) ((ih α ⋯).allowableToStructPerm ρ) = (ih β ⋯).allowableToStructPerm (f ρ)
canConsBot : ∃ (f : (ih α ⋯).Allowable →* ConNF.BasePerm), ∀ (ρ : (ih α ⋯).Allowable), (ih α ⋯).allowableToStructPerm ρ (Quiver.Hom.toPath ⋯) = f ρ
pos_lt_pos_atom : ∀ (t : (ih α ⋯).Tangle) {A : ConNF.ExtendedIndex ↑α} {a : ConNF.Atom}, { path := A, value := Sum.inl a } ∈ ConNF.Tangle.support t → ConNF.pos a < (ih α ⋯).pos ((ih α ⋯).tangleEquiv t)
pos_lt_pos_nearLitter : ∀ (t : (ih α ⋯).Tangle) {A : ConNF.ExtendedIndex ↑α} {N : ConNF.NearLitter}, { path := A, value := Sum.inr N } ∈ ConNF.Tangle.support t → t.set ≠ (ih α ⋯).typedNearLitter N → ConNF.pos N < (ih α ⋯).pos ((ih α ⋯).tangleEquiv t)
smul_fuzz : ∀ (β : ConNF.Λ) (hβ : β < α) (γ : ConNF.Λ) (hγ : γ < α) (hβγ : ↑β ≠ ↑γ) (ρ : (ih α ⋯).Allowable) (t : (ih β ⋯).Tangle) (fαβ : (ih α ⋯).Allowable → (ih β ⋯).Allowable), (∀ (ρ : (ih α ⋯).Allowable), ConNF.Tree.comp (Quiver.Hom.toPath ⋯) ((ih α ⋯).allowableToStructPerm ρ) = (ih β ⋯).allowableToStructPerm (fαβ ρ)) → (ih α ⋯).allowableToStructPerm ρ ((Quiver.Hom.toPath ⋯).cons ⋯) • ConNF.MainInduction.fuzz' (ih β ⋯) (ih γ ⋯) hβγ t = ConNF.MainInduction.fuzz' (ih β ⋯) (ih γ ⋯) hβγ (fαβ ρ • t)
smul_fuzz_bot : ∀ (γ : ConNF.Λ) (hγ : γ < α) (ρ : (ih α ⋯).Allowable) (t : ConNF.Atom), (ih α ⋯).allowableToStructPerm ρ ((Quiver.Hom.toPath ⋯).cons ⋯) • ConNF.MainInduction.fuzz'Bot (ih γ ⋯) t = ConNF.MainInduction.fuzz'Bot (ih γ ⋯) ((ih α ⋯).allowableToStructPerm ρ (Quiver.Hom.toPath ⋯) • t)
allowable_of_smulFuzz : ∀ (ρs : (β : ConNF.Λ) → (hβ : β < α) → (ih β ⋯).Allowable) (π : ConNF.BasePerm), (∀ (β : ConNF.Λ) (hβ : β < α) (γ : ConNF.Λ) (hγ : γ < α) (hβγ : ↑β ≠ ↑γ) (t : (ih β ⋯).Tangle), (ih γ ⋯).allowableToStructPerm (ρs γ hγ) (Quiver.Hom.toPath ⋯) • ConNF.MainInduction.fuzz' (ih β ⋯) (ih γ ⋯) hβγ t = ConNF.MainInduction.fuzz' (ih β ⋯) (ih γ ⋯) hβγ (ρs β hβ • t)) → (∀ (γ : ConNF.Λ) (hγ : γ < α) (t : ConNF.Atom), (ih γ ⋯).allowableToStructPerm (ρs γ hγ) (Quiver.Hom.toPath ⋯) • ConNF.MainInduction.fuzz'Bot (ih γ ⋯) t = ConNF.MainInduction.fuzz'Bot (ih γ ⋯) (π • t)) → ∃ (ρ : (ih α ⋯).Allowable), (∀ (β : ConNF.Λ) (hβ : β < α) (fαβ : (ih α ⋯).Allowable → (ih β ⋯).Allowable), (∀ (ρ : (ih α ⋯).Allowable), ConNF.Tree.comp (Quiver.Hom.toPath ⋯) ((ih α ⋯).allowableToStructPerm ρ) = (ih β ⋯).allowableToStructPerm (fαβ ρ)) → fαβ ρ = ρs β hβ) ∧ ∀ (fα : (ih α ⋯).Allowable → ConNF.BasePerm), (∀ (ρ : (ih α ⋯).Allowable), (ih α ⋯).allowableToStructPerm ρ (Quiver.Hom.toPath ⋯) = fα ρ) → fα ρ = π
eq_toStructSet_of_mem : ∀ (β : ConNF.Λ) (hβ : β < α) (t₁ : (ih α ⋯).TSet), ∀ t₂ ∈ ConNF.StructSet.ofCoe ((ih α ⋯).toStructSet t₁) ↑β ⋯, ∃ (t₂' : (ih β ⋯).TSet), t₂ = (ih β ⋯).toStructSet t₂'
toStructSet_ext : ∀ (β : ConNF.Λ) (hβ : β < α) (t₁ t₂ : (ih α ⋯).TSet), (∀ (t : ConNF.StructSet ↑β), t ∈ ConNF.StructSet.ofCoe ((ih α ⋯).toStructSet t₁) ↑β ⋯ ↔ t ∈ ConNF.StructSet.ofCoe ((ih α ⋯).toStructSet t₂) ↑β ⋯) → (ih α ⋯).toStructSet t₁ = (ih α ⋯).toStructSet t₂
has_singletons : ∀ (β : ConNF.Λ) (hβ : β < α), ∃ (S : (ih β ⋯).TSet → (ih α ⋯).TSet), ∀ (t : (ih β ⋯).TSet), ConNF.StructSet.ofCoe ((ih α ⋯).toStructSet (S t)) ↑β ⋯ = {(ih β ⋯).toStructSet t}
It's useful to keep this Prop-valued, because then there is no data in IH that crosses levels.
step_zero : ConNF.MainInduction.zeroModelData = (ih 0 ⋯).modelData

Instances For

theorem ConNF.MainInduction.IHProp.canCons [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : (β : ConNF.Λ) → β ≤ α → ConNF.MainInduction.IH β} (self : ConNF.MainInduction.IHProp α ih) (β : ConNF.Λ) (hβ : β < α) :

∃ (f : (ih α ⋯).Allowable →* (ih β ⋯).Allowable), ∀ (ρ : (ih α ⋯).Allowable), ConNF.Tree.comp (Quiver.Hom.toPath ⋯) ((ih α ⋯).allowableToStructPerm ρ) = (ih β ⋯).allowableToStructPerm (f ρ)

theorem ConNF.MainInduction.IHProp.canConsBot [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : (β : ConNF.Λ) → β ≤ α → ConNF.MainInduction.IH β} (self : ConNF.MainInduction.IHProp α ih) :

∃ (f : (ih α ⋯).Allowable →* ConNF.BasePerm), ∀ (ρ : (ih α ⋯).Allowable), (ih α ⋯).allowableToStructPerm ρ (Quiver.Hom.toPath ⋯) = f ρ

theorem ConNF.MainInduction.IHProp.pos_lt_pos_atom [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : (β : ConNF.Λ) → β ≤ α → ConNF.MainInduction.IH β} (self : ConNF.MainInduction.IHProp α ih) (t : (ih α ⋯).Tangle) {A : ConNF.ExtendedIndex ↑α} {a : ConNF.Atom} (ht : { path := A, value := Sum.inl a } ∈ ConNF.Tangle.support t) :

ConNF.pos a < (ih α ⋯).pos ((ih α ⋯).tangleEquiv t)

theorem ConNF.MainInduction.IHProp.pos_lt_pos_nearLitter [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : (β : ConNF.Λ) → β ≤ α → ConNF.MainInduction.IH β} (self : ConNF.MainInduction.IHProp α ih) (t : (ih α ⋯).Tangle) {A : ConNF.ExtendedIndex ↑α} {N : ConNF.NearLitter} (ht : { path := A, value := Sum.inr N } ∈ ConNF.Tangle.support t) :

t.set ≠ (ih α ⋯).typedNearLitter N → ConNF.pos N < (ih α ⋯).pos ((ih α ⋯).tangleEquiv t)

theorem ConNF.MainInduction.IHProp.smul_fuzz [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : (β : ConNF.Λ) → β ≤ α → ConNF.MainInduction.IH β} (self : ConNF.MainInduction.IHProp α ih) (β : ConNF.Λ) (hβ : β < α) (γ : ConNF.Λ) (hγ : γ < α) (hβγ : ↑β ≠ ↑γ) (ρ : (ih α ⋯).Allowable) (t : (ih β ⋯).Tangle) (fαβ : (ih α ⋯).Allowable → (ih β ⋯).Allowable) (hfαβ : ∀ (ρ : (ih α ⋯).Allowable), ConNF.Tree.comp (Quiver.Hom.toPath ⋯) ((ih α ⋯).allowableToStructPerm ρ) = (ih β ⋯).allowableToStructPerm (fαβ ρ)) :

(ih α ⋯).allowableToStructPerm ρ ((Quiver.Hom.toPath ⋯).cons ⋯) • ConNF.MainInduction.fuzz' (ih β ⋯) (ih γ ⋯) hβγ t = ConNF.MainInduction.fuzz' (ih β ⋯) (ih γ ⋯) hβγ (fαβ ρ • t)

theorem ConNF.MainInduction.IHProp.smul_fuzz_bot [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : (β : ConNF.Λ) → β ≤ α → ConNF.MainInduction.IH β} (self : ConNF.MainInduction.IHProp α ih) (γ : ConNF.Λ) (hγ : γ < α) (ρ : (ih α ⋯).Allowable) (t : ConNF.Atom) :

(ih α ⋯).allowableToStructPerm ρ ((Quiver.Hom.toPath ⋯).cons ⋯) • ConNF.MainInduction.fuzz'Bot (ih γ ⋯) t = ConNF.MainInduction.fuzz'Bot (ih γ ⋯) ((ih α ⋯).allowableToStructPerm ρ (Quiver.Hom.toPath ⋯) • t)

theorem ConNF.MainInduction.IHProp.allowable_of_smulFuzz [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : (β : ConNF.Λ) → β ≤ α → ConNF.MainInduction.IH β} (self : ConNF.MainInduction.IHProp α ih) (ρs : (β : ConNF.Λ) → (hβ : β < α) → (ih β ⋯).Allowable) (π : ConNF.BasePerm) (hρs : ∀ (β : ConNF.Λ) (hβ : β < α) (γ : ConNF.Λ) (hγ : γ < α) (hβγ : ↑β ≠ ↑γ) (t : (ih β ⋯).Tangle), (ih γ ⋯).allowableToStructPerm (ρs γ hγ) (Quiver.Hom.toPath ⋯) • ConNF.MainInduction.fuzz' (ih β ⋯) (ih γ ⋯) hβγ t = ConNF.MainInduction.fuzz' (ih β ⋯) (ih γ ⋯) hβγ (ρs β hβ • t)) (hπ : ∀ (γ : ConNF.Λ) (hγ : γ < α) (t : ConNF.Atom), (ih γ ⋯).allowableToStructPerm (ρs γ hγ) (Quiver.Hom.toPath ⋯) • ConNF.MainInduction.fuzz'Bot (ih γ ⋯) t = ConNF.MainInduction.fuzz'Bot (ih γ ⋯) (π • t)) :

∃ (ρ : (ih α ⋯).Allowable), (∀ (β : ConNF.Λ) (hβ : β < α) (fαβ : (ih α ⋯).Allowable → (ih β ⋯).Allowable), (∀ (ρ : (ih α ⋯).Allowable), ConNF.Tree.comp (Quiver.Hom.toPath ⋯) ((ih α ⋯).allowableToStructPerm ρ) = (ih β ⋯).allowableToStructPerm (fαβ ρ)) → fαβ ρ = ρs β hβ) ∧ ∀ (fα : (ih α ⋯).Allowable → ConNF.BasePerm), (∀ (ρ : (ih α ⋯).Allowable), (ih α ⋯).allowableToStructPerm ρ (Quiver.Hom.toPath ⋯) = fα ρ) → fα ρ = π

theorem ConNF.MainInduction.IHProp.eq_toStructSet_of_mem [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : (β : ConNF.Λ) → β ≤ α → ConNF.MainInduction.IH β} (self : ConNF.MainInduction.IHProp α ih) (β : ConNF.Λ) (hβ : β < α) (t₁ : (ih α ⋯).TSet) (t₂ : ConNF.StructSet ↑β) :

t₂ ∈ ConNF.StructSet.ofCoe ((ih α ⋯).toStructSet t₁) ↑β ⋯ → ∃ (t₂' : (ih β ⋯).TSet), t₂ = (ih β ⋯).toStructSet t₂'

theorem ConNF.MainInduction.IHProp.toStructSet_ext [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : (β : ConNF.Λ) → β ≤ α → ConNF.MainInduction.IH β} (self : ConNF.MainInduction.IHProp α ih) (β : ConNF.Λ) (hβ : β < α) (t₁ : (ih α ⋯).TSet) (t₂ : (ih α ⋯).TSet) :

(∀ (t : ConNF.StructSet ↑β), t ∈ ConNF.StructSet.ofCoe ((ih α ⋯).toStructSet t₁) ↑β ⋯ ↔ t ∈ ConNF.StructSet.ofCoe ((ih α ⋯).toStructSet t₂) ↑β ⋯) → (ih α ⋯).toStructSet t₁ = (ih α ⋯).toStructSet t₂

theorem ConNF.MainInduction.IHProp.has_singletons [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : (β : ConNF.Λ) → β ≤ α → ConNF.MainInduction.IH β} (self : ConNF.MainInduction.IHProp α ih) (β : ConNF.Λ) (hβ : β < α) :

∃ (S : (ih β ⋯).TSet → (ih α ⋯).TSet), ∀ (t : (ih β ⋯).TSet), ConNF.StructSet.ofCoe ((ih α ⋯).toStructSet (S t)) ↑β ⋯ = {(ih β ⋯).toStructSet t}

It's useful to keep this Prop-valued, because then there is no data in IH that crosses levels.

theorem ConNF.MainInduction.IHProp.step_zero [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} {ih : (β : ConNF.Λ) → β ≤ α → ConNF.MainInduction.IH β} (self : ConNF.MainInduction.IHProp α ih) :

ConNF.MainInduction.zeroModelData = (ih 0 ⋯).modelData

def ConNF.MainInduction.newAllowableCons [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (γ : ConNF.TypeIndex) [ConNF.LeLevel γ] (hγ : γ < ↑α) :

ConNF.NewAllowable → ConNF.Allowable γ

Equations

ConNF.MainInduction.newAllowableCons α ihs γ hγ ρ = (ConNF.MainInduction.foaData_allowable_lt'_equiv α ihs γ hγ).symm (↑ρ γ)

Instances For

@[simp]

theorem ConNF.MainInduction.newAllowableCons_map_one [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (γ : ConNF.TypeIndex) [ConNF.LeLevel γ] (hγ : γ < ↑α) :

ConNF.MainInduction.newAllowableCons α ihs γ hγ 1 = 1

@[simp]

theorem ConNF.MainInduction.newAllowableCons_map_mul [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (γ : ConNF.TypeIndex) [ConNF.LeLevel γ] (hγ : γ < ↑α) (ρ₁ : ConNF.NewAllowable) (ρ₂ : ConNF.NewAllowable) :

ConNF.MainInduction.newAllowableCons α ihs γ hγ (ρ₁ * ρ₂) = ConNF.MainInduction.newAllowableCons α ihs γ hγ ρ₁ * ConNF.MainInduction.newAllowableCons α ihs γ hγ ρ₂

theorem ConNF.MainInduction.newAllowableCons_toStructPerm [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (γ : ConNF.TypeIndex) [ConNF.LtLevel γ] (hγ : γ < ↑α) (ρ : ConNF.NewAllowable) :

ConNF.Tree.comp (Quiver.Hom.toPath hγ) (ConNF.NewAllowable.toStructPerm ρ) = ConNF.Allowable.toStructPerm (ConNF.MainInduction.newAllowableCons α ihs γ hγ ρ)

theorem ConNF.MainInduction.can_allowableConsStep [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.TypeIndex) [iβ : ConNF.LeLevel β] (γ : ConNF.TypeIndex) [iγ : ConNF.LeLevel γ] (hγ : γ < β) :

∃ (f : ConNF.Allowable β →* ConNF.Allowable γ), ∀ (ρ : ConNF.Allowable β), ConNF.Tree.comp (Quiver.Hom.toPath hγ) (ConNF.Allowable.toStructPerm ρ) = ConNF.Allowable.toStructPerm (f ρ)

noncomputable def ConNF.MainInduction.allowableConsStep [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.TypeIndex) [ConNF.LeLevel β] (γ : ConNF.TypeIndex) [ConNF.LeLevel γ] (hγ : γ < β) :

ConNF.Allowable β →* ConNF.Allowable γ

Equations

ConNF.MainInduction.allowableConsStep α ihs h β γ hγ = ⋯.choose

Instances For

theorem ConNF.MainInduction.allowableConsStep_eq [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.TypeIndex) [ConNF.LeLevel β] (γ : ConNF.TypeIndex) [ConNF.LeLevel γ] (hγ : γ < β) (ρ : ConNF.Allowable β) :

ConNF.Tree.comp (Quiver.Hom.toPath hγ) (ConNF.Allowable.toStructPerm ρ) = ConNF.Allowable.toStructPerm ((ConNF.MainInduction.allowableConsStep α ihs h β γ hγ) ρ)

theorem ConNF.MainInduction.pos_lt_pos_atom_step [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) [iβ : 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

theorem ConNF.MainInduction.pos_lt_pos_nearLitter_step [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) [iβ : 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

theorem ConNF.MainInduction.allowableConsStep_eq_lt [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β < α) (γ : ConNF.Λ) (hγ : γ < α) (hγβ : γ < β) (ρ : (ihs β hβ).Allowable) :

ConNF.Tree.comp (Quiver.Hom.toPath ⋯) ((ihs β hβ).allowableToStructPerm ρ) = (ihs γ hγ).allowableToStructPerm ((ConNF.MainInduction.foaData_allowable_lt_equiv α ihs γ hγ) ((ConNF.MainInduction.allowableConsStep α ihs h ↑β ↑γ ⋯) ((ConNF.MainInduction.foaData_allowable_lt_equiv α ihs β hβ).symm ρ)))

theorem ConNF.MainInduction.allowableConsStep_eq_eq [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (γ : ConNF.Λ) (hγ : γ < α) (ρ : ConNF.Allowable ↑α) :

↑((ConNF.MainInduction.foaData_allowable_eq_equiv α ihs) ρ) ↑γ = (ConNF.MainInduction.foaData_allowable_lt_equiv α ihs γ hγ) ((ConNF.MainInduction.allowableConsStep α ihs h ↑α ↑γ ⋯) ρ)

theorem ConNF.MainInduction.allowableConsStep_eq_eq' [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (γ : ConNF.TypeIndex) (hγ : γ < ↑α) (ρ : ConNF.Allowable ↑α) :

↑((ConNF.MainInduction.foaData_allowable_eq_equiv α ihs) ρ) γ = (ConNF.MainInduction.foaData_allowable_lt'_equiv α ihs γ hγ) ((ConNF.MainInduction.allowableConsStep α ihs h (↑α) γ hγ) ρ)

theorem ConNF.MainInduction.smul_fuzz_step [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.TypeIndex) [iβ : ConNF.LeLevel β] (γ : ConNF.TypeIndex) [iγ : ConNF.LtLevel γ] (δ : ConNF.Λ) [iδ : 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.MainInduction.allowableConsStep α ihs h β γ hγ) ρ • t)

theorem ConNF.MainInduction.allowable_of_smulFuzz_step [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) [iβ : ConNF.LeLevel ↑β] (ρs : (γ : ConNF.TypeIndex) → [inst : ConNF.LtLevel γ] → γ < ↑β → ConNF.Allowable γ) (hρs : ∀ (γ : 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.MainInduction.allowableConsStep α ihs h (↑β) γ hγ) ρ = ρs γ hγ

noncomputable def ConNF.MainInduction.buildStepFOAAssumptions [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) :

ConNF.FOAAssumptions

Equations

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

Instances For

theorem ConNF.MainInduction.eq_toStructSet_of_mem_step [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) [iβ : ConNF.LeLevel ↑β] (γ : ConNF.Λ) [iγ : ConNF.LeLevel ↑γ] (hγβ : ↑γ < ↑β) (t₁ : ConNF.TSet ↑β) (t₂ : ConNF.StructSet ↑γ) :

t₂ ∈ ConNF.StructSet.ofCoe (ConNF.toStructSet t₁) (↑γ) hγβ → ∃ (t₂' : ConNF.TSet ↑γ), t₂ = ConNF.toStructSet t₂'

theorem ConNF.MainInduction.toStructSet_ext_step [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (γ : ConNF.Λ) [iβ : ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (hγβ : ↑γ < ↑β) (t₁ : ConNF.TSet ↑β) (t₂ : ConNF.TSet ↑β) :

(∀ (t : ConNF.StructSet ↑γ), t ∈ ConNF.StructSet.ofCoe (ConNF.toStructSet t₁) (↑γ) hγβ ↔ t ∈ ConNF.StructSet.ofCoe (ConNF.toStructSet t₂) (↑γ) hγβ) → ConNF.toStructSet t₁ = ConNF.toStructSet t₂

theorem ConNF.MainInduction.has_singletons [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β ≤ α) (γ : ConNF.Λ) (hγβ : γ < β) :

∃ (S : ConNF.TSet ↑γ → ConNF.TSet ↑β), ∀ (t : ConNF.TSet ↑γ), ConNF.StructSet.ofCoe (ConNF.toStructSet (S t)) ↑γ ⋯ = {ConNF.toStructSet t}

noncomputable def ConNF.MainInduction.singleton_step [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β ≤ α) (γ : ConNF.Λ) (hγβ : γ < β) :

ConNF.TSet ↑γ → ConNF.TSet ↑β

Equations

ConNF.MainInduction.singleton_step α ihs h β hβ γ hγβ = ⋯.choose

Instances For

theorem ConNF.MainInduction.singleton_step_spec [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β ≤ α) (γ : ConNF.Λ) (hγβ : γ < β) (t : ConNF.TSet ↑γ) :

ConNF.StructSet.ofCoe (ConNF.toStructSet (ConNF.MainInduction.singleton_step α ihs h β hβ γ hγβ t)) ↑γ ⋯ = {ConNF.toStructSet t}

noncomputable def ConNF.MainInduction.buildStepCountingAssumptions [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) :

ConNF.CountingAssumptions

Equations

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

Instances For

theorem ConNF.MainInduction.zeroModelData_eq [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) :

ConNF.MainInduction.zeroModelData = ConNF.MainInduction.modelDataStepFn α ihs 0 ⋯

theorem ConNF.MainInduction.mk_codingFunction_le [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) :

Cardinal.mk (ConNF.CodingFunction 0) < Cardinal.mk ConNF.μ

theorem ConNF.MainInduction.mk_tSet_step [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) :

Cardinal.mk ConNF.NewTSet = Cardinal.mk ConNF.μ

noncomputable def ConNF.MainInduction.posStep [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) :

ConNF.MainInduction.Tang α (ConNF.TSet ↑α) (ConNF.Allowable ↑α) → ConNF.μ

Equations

ConNF.MainInduction.posStep α ihs h t = ConNF.Construction.pos ⋯ (t.set, t.support)

Instances For

theorem ConNF.MainInduction.posStep_injective [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) :

Function.Injective (ConNF.MainInduction.posStep α ihs h)

theorem ConNF.MainInduction.posStep_typedNearLitter [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (N : ConNF.NearLitter) (t : ConNF.MainInduction.Tang α (ConNF.TSet ↑α) (ConNF.Allowable ↑α)) :

t.set = ConNF.newTypedNearLitter N → ConNF.pos N ≤ ConNF.MainInduction.posStep α ihs h t

noncomputable def ConNF.MainInduction.buildStep [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) :

ConNF.MainInduction.IH α

Equations

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

Instances For

noncomputable def ConNF.MainInduction.buildStepFn [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β ≤ α) :

ConNF.MainInduction.IH β

Equations

ConNF.MainInduction.buildStepFn α ihs h β hβ = if hβ' : β = α then ⋯ ▸ ConNF.MainInduction.buildStep α ihs h else ihs β ⋯

Instances For

theorem ConNF.MainInduction.buildStepFn_eq [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) :

ConNF.MainInduction.buildStepFn α ihs h α ⋯ = ConNF.MainInduction.buildStep α ihs h

theorem ConNF.MainInduction.buildStepFn_lt [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β < α) :

ConNF.MainInduction.buildStepFn α ihs h β ⋯ = ihs β hβ

def ConNF.MainInduction.buildStepFn_tangle_eq_equiv [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) :

(ConNF.MainInduction.buildStepFn α ihs h α ⋯).Tangle ≃ (ConNF.MainInduction.buildStep α ihs h).Tangle

Equations

ConNF.MainInduction.buildStepFn_tangle_eq_equiv α ihs h = Equiv.cast ⋯

Instances For

def ConNF.MainInduction.buildStepFn_allowable_eq_equiv [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) :

(ConNF.MainInduction.buildStepFn α ihs h α ⋯).Allowable ≃ (ConNF.MainInduction.buildStep α ihs h).Allowable

Equations

ConNF.MainInduction.buildStepFn_allowable_eq_equiv α ihs h = Equiv.cast ⋯

Instances For

def ConNF.MainInduction.buildStepFn_tangle_lt_equiv [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β < α) :

(ConNF.MainInduction.buildStepFn α ihs h β ⋯).Tangle ≃ (ihs β hβ).Tangle

Equations

ConNF.MainInduction.buildStepFn_tangle_lt_equiv α ihs h β hβ = Equiv.cast ⋯

Instances For

def ConNF.MainInduction.buildStepFn_allowable_lt_equiv [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β < α) :

(ConNF.MainInduction.buildStepFn α ihs h β ⋯).Allowable ≃ (ihs β hβ).Allowable

Equations

ConNF.MainInduction.buildStepFn_allowable_lt_equiv α ihs h β hβ = Equiv.cast ⋯

Instances For

@[simp]

theorem ConNF.MainInduction.buildStepFn_allowable_eq_equiv_toStructPerm [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (ρ : (ConNF.MainInduction.buildStepFn α ihs h α ⋯).Allowable) :

(ConNF.MainInduction.buildStepFn α ihs h α ⋯).allowableToStructPerm ρ = (ConNF.MainInduction.buildStep α ihs h).allowableToStructPerm ((ConNF.MainInduction.buildStepFn_allowable_eq_equiv α ihs h) ρ)

@[simp]

theorem ConNF.MainInduction.buildStepFn_allowable_lt_equiv_toStructPerm [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β < α) (ρ : (ConNF.MainInduction.buildStepFn α ihs h β ⋯).Allowable) :

(ConNF.MainInduction.buildStepFn α ihs h β ⋯).allowableToStructPerm ρ = (ihs β hβ).allowableToStructPerm ((ConNF.MainInduction.buildStepFn_allowable_lt_equiv α ihs h β hβ) ρ)

@[simp]

theorem ConNF.MainInduction.buildStepFn_allowable_lt_equiv_smul' [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β < α) (ρ : (ConNF.MainInduction.buildStepFn α ihs h β ⋯).Allowable) (t : (ConNF.MainInduction.buildStepFn α ihs h β ⋯).Tangle) :

(ConNF.MainInduction.buildStepFn_tangle_lt_equiv α ihs h β hβ) (ρ • t) = (ConNF.MainInduction.buildStepFn_allowable_lt_equiv α ihs h β hβ) ρ • (ConNF.MainInduction.buildStepFn_tangle_lt_equiv α ihs h β hβ) t

@[simp]

theorem ConNF.MainInduction.buildStepFn_tangle_lt_equiv_fuzz [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β < α) (γ : ConNF.Λ) (hγ : γ < α) (hβγ : ↑β ≠ ↑γ) (t : ConNF.Tangle ↑β) :

ConNF.MainInduction.fuzz' (ConNF.MainInduction.buildStepFn α ihs h β ⋯) (ConNF.MainInduction.buildStepFn α ihs h γ ⋯) hβγ t = ConNF.fuzz hβγ ((ConNF.MainInduction.buildStepFn_tangle_lt_equiv α ihs h β hβ) t)

def ConNF.MainInduction.cons_step [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β < α) :

(ConNF.MainInduction.buildStep α ihs h).Allowable →* (ihs β hβ).Allowable

Equations

ConNF.MainInduction.cons_step α ihs h β hβ = { toFun := fun (ρ : (ConNF.MainInduction.buildStep α ihs h).Allowable) => ↑ρ ↑β, map_one' := ⋯, map_mul' := ⋯ }

Instances For

theorem ConNF.MainInduction.cons_step_spec [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β < α) (ρ : (ConNF.MainInduction.buildStep α ihs h).Allowable) :

ConNF.Tree.comp (Quiver.Hom.toPath ⋯) ((ConNF.MainInduction.buildStep α ihs h).allowableToStructPerm ρ) = (ihs β hβ).allowableToStructPerm ((ConNF.MainInduction.cons_step α ihs h β hβ) ρ)

def ConNF.MainInduction.consBot_step [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) :

(ConNF.MainInduction.buildStep α ihs h).Allowable →* ConNF.BasePerm

Equations

ConNF.MainInduction.consBot_step α ihs h = { toFun := fun (ρ : (ConNF.MainInduction.buildStep α ihs h).Allowable) => ↑ρ ⊥, map_one' := ⋯, map_mul' := ⋯ }

Instances For

theorem ConNF.MainInduction.consBot_step_spec [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (ρ : (ConNF.MainInduction.buildStep α ihs h).Allowable) :

(ConNF.MainInduction.buildStep α ihs h).allowableToStructPerm ρ (Quiver.Hom.toPath ⋯) = (ConNF.MainInduction.consBot_step α ihs h) ρ

theorem ConNF.MainInduction.pos_lt_pos_atom [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (t : (ConNF.MainInduction.buildStep α ihs h).Tangle) {A : ConNF.ExtendedIndex ↑α} {a : ConNF.Atom} :

{ path := A, value := Sum.inl a } ∈ t.support → ConNF.pos a < (ConNF.MainInduction.buildStep α ihs h).pos ((ConNF.MainInduction.buildStep α ihs h).tangleEquiv t)

theorem ConNF.MainInduction.pos_lt_pos_nearLitter [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (t : (ConNF.MainInduction.buildStep α ihs h).Tangle) {A : ConNF.ExtendedIndex ↑α} {N : ConNF.NearLitter} :

{ path := A, value := Sum.inr N } ∈ t.support → t.set ≠ (ConNF.MainInduction.buildStep α ihs h).typedNearLitter N → ConNF.pos N < (ConNF.MainInduction.buildStep α ihs h).pos ((ConNF.MainInduction.buildStep α ihs h).tangleEquiv t)

theorem ConNF.MainInduction.cons_fun_eq [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β < α) (fαβ : (ConNF.MainInduction.buildStep α ihs h).Allowable → (ihs β hβ).Allowable) (hfαβ : ∀ (ρ : (ConNF.MainInduction.buildStep α ihs h).Allowable), ConNF.Tree.comp (Quiver.Hom.toPath ⋯) ((ConNF.MainInduction.buildStep α ihs h).allowableToStructPerm ρ) = (ihs β hβ).allowableToStructPerm (fαβ ρ)) :

fαβ = ⇑(ConNF.MainInduction.cons_step α ihs h β hβ)

theorem ConNF.MainInduction.consBot_fun_eq [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (fα : (ConNF.MainInduction.buildStep α ihs h).Allowable → ConNF.BasePerm) (hfα : ∀ (ρ : (ConNF.MainInduction.buildStep α ihs h).Allowable), (ConNF.MainInduction.buildStep α ihs h).allowableToStructPerm ρ (Quiver.Hom.toPath ⋯) = fα ρ) :

fα = ⇑(ConNF.MainInduction.consBot_step α ihs h)

theorem ConNF.MainInduction.smul_fuzz [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β < α) (γ : ConNF.Λ) (hγ : γ < α) (hβγ : ↑β ≠ ↑γ) (ρ : (ConNF.MainInduction.buildStepFn α ihs h α ⋯).Allowable) (t : (ConNF.MainInduction.buildStepFn α ihs h β ⋯).Tangle) (fαβ : (ConNF.MainInduction.buildStepFn α ihs h α ⋯).Allowable → (ConNF.MainInduction.buildStepFn α ihs h β ⋯).Allowable) (hfαβ : ∀ (ρ : (ConNF.MainInduction.buildStepFn α ihs h α ⋯).Allowable), ConNF.Tree.comp (Quiver.Hom.toPath ⋯) ((ConNF.MainInduction.buildStepFn α ihs h α ⋯).allowableToStructPerm ρ) = (ConNF.MainInduction.buildStepFn α ihs h β ⋯).allowableToStructPerm (fαβ ρ)) :

(ConNF.MainInduction.buildStepFn α ihs h α ⋯).allowableToStructPerm ρ ((Quiver.Hom.toPath ⋯).cons ⋯) • ConNF.MainInduction.fuzz' (ConNF.MainInduction.buildStepFn α ihs h β ⋯) (ConNF.MainInduction.buildStepFn α ihs h γ ⋯) hβγ t = ConNF.MainInduction.fuzz' (ConNF.MainInduction.buildStepFn α ihs h β ⋯) (ConNF.MainInduction.buildStepFn α ihs h γ ⋯) hβγ (fαβ ρ • t)

theorem ConNF.MainInduction.smul_fuzz_bot [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (γ : ConNF.Λ) (hγ : γ < α) (ρ : (ConNF.MainInduction.buildStepFn α ihs h α ⋯).Allowable) (t : ConNF.Atom) :

(ConNF.MainInduction.buildStepFn α ihs h α ⋯).allowableToStructPerm ρ ((Quiver.Hom.toPath ⋯).cons ⋯) • ConNF.MainInduction.fuzz'Bot (ConNF.MainInduction.buildStepFn α ihs h γ ⋯) t = ConNF.MainInduction.fuzz'Bot (ConNF.MainInduction.buildStepFn α ihs h γ ⋯) ((ConNF.MainInduction.buildStepFn α ihs h α ⋯).allowableToStructPerm ρ (Quiver.Hom.toPath ⋯) • t)

theorem ConNF.MainInduction.allowable_of_smulFuzz_step' [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (ρs : (β : ConNF.Λ) → (hβ : β < α) → (ConNF.MainInduction.buildStepFn α ihs h β ⋯).Allowable) (π : ConNF.BasePerm) (hρs : ∀ (β : ConNF.Λ) (hβ : β < α) (γ : ConNF.Λ) (hγ : γ < α) (hβγ : ↑β ≠ ↑γ) (t : (ConNF.MainInduction.buildStepFn α ihs h β ⋯).Tangle), (ConNF.MainInduction.buildStepFn α ihs h γ ⋯).allowableToStructPerm (ρs γ hγ) (Quiver.Hom.toPath ⋯) • ConNF.MainInduction.fuzz' (ConNF.MainInduction.buildStepFn α ihs h β ⋯) (ConNF.MainInduction.buildStepFn α ihs h γ ⋯) hβγ t = ConNF.MainInduction.fuzz' (ConNF.MainInduction.buildStepFn α ihs h β ⋯) (ConNF.MainInduction.buildStepFn α ihs h γ ⋯) hβγ (ρs β hβ • t)) (hπ : ∀ (γ : ConNF.Λ) (hγ : γ < α) (t : ConNF.Atom), (ConNF.MainInduction.buildStepFn α ihs h γ ⋯).allowableToStructPerm (ρs γ hγ) (Quiver.Hom.toPath ⋯) • ConNF.MainInduction.fuzz'Bot (ConNF.MainInduction.buildStepFn α ihs h γ ⋯) t = ConNF.MainInduction.fuzz'Bot (ConNF.MainInduction.buildStepFn α ihs h γ ⋯) (π • t)) :

∃ (ρ : (ConNF.MainInduction.buildStepFn α ihs h α ⋯).Allowable), (∀ (β : ConNF.Λ) (hβ : β < α) (fαβ : (ConNF.MainInduction.buildStepFn α ihs h α ⋯).Allowable → (ConNF.MainInduction.buildStepFn α ihs h β ⋯).Allowable), (∀ (ρ : (ConNF.MainInduction.buildStepFn α ihs h α ⋯).Allowable), ConNF.Tree.comp (Quiver.Hom.toPath ⋯) ((ConNF.MainInduction.buildStepFn α ihs h α ⋯).allowableToStructPerm ρ) = (ConNF.MainInduction.buildStepFn α ihs h β ⋯).allowableToStructPerm (fαβ ρ)) → fαβ ρ = ρs β hβ) ∧ ∀ (fα : (ConNF.MainInduction.buildStepFn α ihs h α ⋯).Allowable → ConNF.BasePerm), (∀ (ρ : (ConNF.MainInduction.buildStepFn α ihs h α ⋯).Allowable), (ConNF.MainInduction.buildStepFn α ihs h α ⋯).allowableToStructPerm ρ (Quiver.Hom.toPath ⋯) = fα ρ) → fα ρ = π

theorem ConNF.MainInduction.eq_toStructSet_of_mem_step' [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β < α) (t₁ : (ConNF.MainInduction.buildStep α ihs h).TSet) (t₂ : ConNF.StructSet ↑β) (ht₂ : t₂ ∈ ConNF.StructSet.ofCoe ((ConNF.MainInduction.buildStep α ihs h).toStructSet t₁) ↑β ⋯) :

∃ (t₂' : (ihs β hβ).TSet), t₂ = (ihs β hβ).toStructSet t₂'

theorem ConNF.MainInduction.toStructSet_ext_step' [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β < α) (t₁ : (ConNF.MainInduction.buildStep α ihs h).TSet) (t₂ : (ConNF.MainInduction.buildStep α ihs h).TSet) (ht : ∀ (t : ConNF.StructSet ↑β), t ∈ ConNF.StructSet.ofCoe ((ConNF.MainInduction.buildStep α ihs h).toStructSet t₁) ↑β ⋯ ↔ t ∈ ConNF.StructSet.ofCoe ((ConNF.MainInduction.buildStep α ihs h).toStructSet t₂) ↑β ⋯) :

(ConNF.MainInduction.buildStep α ihs h).toStructSet t₁ = (ConNF.MainInduction.buildStep α ihs h).toStructSet t₂

noncomputable def ConNF.MainInduction.singleton_step' [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β < α) :

(ihs β hβ).TSet → (ConNF.MainInduction.buildStep α ihs h).TSet

Equations

ConNF.MainInduction.singleton_step' α ihs h β hβ = ConNF.newSingleton ↑β

Instances For

theorem ConNF.MainInduction.singleton_step'_spec [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) (β : ConNF.Λ) (hβ : β < α) (t : (ihs β hβ).TSet) :

ConNF.StructSet.ofCoe ((ConNF.MainInduction.buildStep α ihs h).toStructSet (ConNF.MainInduction.singleton_step' α ihs h β hβ t)) ↑β ⋯ = {(ihs β hβ).toStructSet t}

theorem ConNF.MainInduction.buildStep_prop [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IH β) (h : ∀ (β : ConNF.Λ) (hβ : β < α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => ihs γ ⋯) :

ConNF.MainInduction.IHProp α (ConNF.MainInduction.buildStepFn α ihs h)

structure ConNF.MainInduction.IHCumul [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) :

Type (u + 1)

ih : (β : ConNF.Λ) → β ≤ α → ConNF.MainInduction.IH β
prop : ∀ (β : ConNF.Λ) (hβ : β ≤ α), ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => self.ih γ ⋯
ih_eq : ∀ (β : ConNF.Λ) (hβ : β ≤ α), self.ih β hβ = ConNF.MainInduction.buildStep β (fun (γ : ConNF.Λ) (hγ : γ < β) => self.ih γ ⋯) ⋯

Instances For

theorem ConNF.MainInduction.IHCumul.prop [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} (self : ConNF.MainInduction.IHCumul α) (β : ConNF.Λ) (hβ : β ≤ α) :

ConNF.MainInduction.IHProp β fun (γ : ConNF.Λ) (hγ : γ ≤ β) => self.ih γ ⋯

theorem ConNF.MainInduction.IHCumul.ih_eq [ConNF.Params] [ConNF.BasePositions] {α : ConNF.Λ} (self : ConNF.MainInduction.IHCumul α) (β : ConNF.Λ) (hβ : β ≤ α) :

self.ih β hβ = ConNF.MainInduction.buildStep β (fun (γ : ConNF.Λ) (hγ : γ < β) => self.ih γ ⋯) ⋯

theorem ConNF.MainInduction.ihs_eq [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IHCumul β) (β : ConNF.Λ) (hβ : β < α) (γ : ConNF.Λ) (hγ : γ < α) (δ : ConNF.Λ) (hδβ : δ ≤ β) (hδγ : δ ≤ γ) :

(ihs β hβ).ih δ hδβ = (ihs γ hγ).ih δ hδγ

noncomputable def ConNF.MainInduction.buildCumulStep [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) (ihs : (β : ConNF.Λ) → β < α → ConNF.MainInduction.IHCumul β) :

ConNF.MainInduction.IHCumul α

Equations

ConNF.MainInduction.buildCumulStep α ihs = { ih := ConNF.MainInduction.buildStepFn α (fun (β : ConNF.Λ) (hβ : β < α) => (ihs β hβ).ih β ⋯) ⋯, prop := ⋯, ih_eq := ⋯ }

Instances For

noncomputable def ConNF.MainInduction.buildCumul [ConNF.Params] [ConNF.BasePositions] (α : ConNF.Λ) :

ConNF.MainInduction.IHCumul α

Equations

ConNF.MainInduction.buildCumul = ⋯.fix ConNF.MainInduction.buildCumulStep

Instances For