def Thesis.TwoLabel.SingleComponent.d0_of_on_main_road {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) (hcr : Thesis.cofinal_reduction main_road) {a : { b : α // C.p b }} (hmem : a ∈ main_road.elems) : ↑(Thesis.RewriteDistance.dX a main_road.elems ⋯) = 0

Equations

• ⋯ = ⋯

def Thesis.TwoLabel.SingleComponent.step_minimizing {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) (hcr : Thesis.cofinal_reduction main_road) [LinearOrder α] (a b : C.Subtype) : Prop

Equations

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

def Thesis.TwoLabel.SingleComponent.C' {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) (hcr : Thesis.cofinal_reduction main_road) [LinearOrder α] : Thesis.ARS C.Subtype (Fin 2)

Equations

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

theorem Thesis.TwoLabel.SingleComponent.C'.reduction_equivalent {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) (hcr : Thesis.cofinal_reduction main_road) [LinearOrder α] (b c : C.Subtype) : C.ars.union_rel b c ↔ (Thesis.TwoLabel.SingleComponent.C' main_road hcr).union_rel b c

Lemma 4.9(i): our labeled ARS is reduction-equivalent to C.ars.

theorem Thesis.TwoLabel.SingleComponent.steps_on_main_road {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) (hcr : Thesis.cofinal_reduction main_road) [LinearOrder α] {n k : ℕ} (hk : ↑n + ↑k < N + 1) : ((Thesis.TwoLabel.SingleComponent.C' main_road hcr).rel 0)∗ (f n) (f (n + k))

Equivalent to steps_along_hseq in Prop 14.2.30.

theorem Thesis.TwoLabel.SingleComponent.main_road_join {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) (hcr : Thesis.cofinal_reduction main_road) (a b : C.Subtype) [LinearOrder α] (ha : a ∈ main_road.elems) (hb : b ∈ main_road.elems) : ∃ (d : C.Subtype), ((Thesis.TwoLabel.SingleComponent.C' main_road hcr).rel 0)∗ a d ∧ ((Thesis.TwoLabel.SingleComponent.C' main_road hcr).rel 0)∗ b d

Lemma 4.9(ii); if a, b ∈ M, ∃d, a ->>_0 d ∧ b ->>_0 d.

theorem Thesis.TwoLabel.SingleComponent.zero_step_unique {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) {hacyclic : main_road.acyclic} (hcr : Thesis.cofinal_reduction main_road) [LinearOrder α] {a b b' : C.Subtype} : (Thesis.TwoLabel.SingleComponent.C' main_road hcr).rel 0 a b ∧ (Thesis.TwoLabel.SingleComponent.C' main_road hcr).rel 0 a b' → b = b'

Lemma 4.9 (iii): There is at most one b s.t. a ->₀ b.

theorem Thesis.TwoLabel.SingleComponent.exists_distance_decreasing_step {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) (hcr : Thesis.cofinal_reduction main_road) [LinearOrder α] [WellFoundedLT α] (a : C.Subtype) (ha : a ∉ main_road.elems) : ∃ (b : C.Subtype), (Thesis.TwoLabel.SingleComponent.C' main_road hcr).rel 0 a b ∧ ↑(Thesis.RewriteDistance.dX a main_road.elems ⋯) = ↑(Thesis.RewriteDistance.dX b main_road.elems ⋯) + 1

theorem Thesis.TwoLabel.SingleComponent.main_road_reduction {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) (hcr : Thesis.cofinal_reduction main_road) [LinearOrder α] [WellFoundedLT α] (a : C.Subtype) : ∃ m ∈ main_road.elems, ((Thesis.TwoLabel.SingleComponent.C' main_road hcr).rel 0)∗ a m

Lemma 4.9 (v): Every element a reduces to some element in the main road using only 0-steps.

theorem Thesis.TwoLabel.SingleComponent.C'.stronger_decreasing {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) {hacyclic : main_road.acyclic} (hcr : Thesis.cofinal_reduction main_road) [LinearOrder α] [WellFoundedLT α] : Thesis.stronger_decreasing (Thesis.TwoLabel.SingleComponent.C' main_road hcr)

theorem Thesis.TwoLabel.SingleComponent.C'.locally_decreasing {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) {hacyclic : main_road.acyclic} (hcr : Thesis.cofinal_reduction main_road) [LinearOrder α] [WellFoundedLT α] : Thesis.locally_decreasing (Thesis.TwoLabel.SingleComponent.C' main_road hcr)

theorem Thesis.TwoLabel.dcr₂_component {α I : Type} (A : Thesis.ARS α I) (hcp : Thesis.cofinality_property A) (C : Thesis.Component A) : Thesis.DCRn 2 C.ars

If A has the cofinality property, any component of A is DCR₂.

def Thesis.TwoLabel.MultiComponent.cp_dcr₂_ars {α I : Type} {A : Thesis.ARS α I} [hlo : LinearOrder α] (hcp : Thesis.cofinality_property_conv A) : Thesis.ARS α (Fin 2)

Equations

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

def Thesis.TwoLabel.MultiComponent.reduction_equivalent {α I : Type} {A : Thesis.ARS α I} [hlo : LinearOrder α] (hcp : Thesis.cofinality_property_conv A) {a b : α} : A.union_rel a b ↔ (Thesis.TwoLabel.MultiComponent.cp_dcr₂_ars hcp).union_rel a b

Equations

• ⋯ = ⋯

def Thesis.TwoLabel.MultiComponent.locally_decreasing {α I : Type} {A : Thesis.ARS α I} [hlo : LinearOrder α] [hwf : WellFoundedLT α] (hcp : Thesis.cofinality_property_conv A) : Thesis.locally_decreasing (Thesis.TwoLabel.MultiComponent.cp_dcr₂_ars hcp)

Equations

• ⋯ = ⋯

def Thesis.TwoLabel.cp_dcr₂ {α I : Type} (A : Thesis.ARS α I) (hcp : Thesis.cofinality_property A) : Thesis.DCRn 2 A

Any ARS with the cofinality property is DCR₂

Equations

• ⋯ = ⋯

def Thesis.TwoLabel.dcr₂_complete {α I : Type} [Countable α] (A : Thesis.ARS α I) (hc : Thesis.confluent A.union_rel) : Thesis.DCRn 2 A

DCR₂ is a complete method for proving confluence of countable ARSs.

Equations

• ⋯ = ⋯