@[reducible, inline]

abbrev Thesis.reduction_seq {α : Type u_1} (r : Rel α α) (N : ℕ∞) (f : ℕ → α) : Prop

A generic reduction sequence, which is finite if N ≠ ⊤ and infinite otherwise.

Equations

• Thesis.reduction_seq r N f = ∀ (n : ℕ), ↑n < N → r (f n) (f (n + 1))

@[simp]

theorem Thesis.reduction_seq_top_iff {α : Type u_1} {r : Rel α α} {f : ℕ → α} : Thesis.reduction_seq r ⊤ f ↔ ∀ (n : ℕ), r (f n) (f (n + 1))

@[simp]

theorem Thesis.reduction_seq_coe_iff {α : Type u_1} {r : Rel α α} {f : ℕ → α} {N : ℕ} : Thesis.reduction_seq r (↑N) f ↔ ∀ n < N, r (f n) (f (n + 1))

theorem Thesis.reduction_seq.inf_step {α : Type u_1} {r : Rel α α} {f : ℕ → α} (hseq : Thesis.reduction_seq r ⊤ f) (n : ℕ) : r (f n) (f (n + 1))

In an infinite reduction sequence, we can take a step from any n to n + 1.

theorem Thesis.reduction_seq.refl {α : Type u_1} {r : Rel α α} {f : ℕ → α} : Thesis.reduction_seq r 0 f

Any function is a length-0 reduction sequence, containing only f 0.

theorem Thesis.reduction_seq.from_reflTrans {α : Type u_1} {r : Rel α α} {a b : α} (hrt : r∗ a b) : ∃ (N : ℕ) (f : ℕ → α), Thesis.reduction_seq r (↑N) f ∧ f 0 = a ∧ f N = b

theorem Thesis.reduction_seq.trans {α : Type u_1} {r : Rel α α} {N : ℕ∞} {f : ℕ → α} (hseq : Thesis.reduction_seq r N f) (n m : ℕ) (hm : ↑m < N + 1) (hn : n < m) : r⁺ (f n) (f m)

In a generic reduction sequence reduction_seq r N f, f m is a reduct of f n, assuming n < m < N + 1.

theorem Thesis.reduction_seq.reflTrans {α : Type u_1} {r : Rel α α} {N : ℕ∞} {f : ℕ → α} (hseq : Thesis.reduction_seq r N f) (n m : ℕ) (hm : ↑m < N + 1) (hn : n ≤ m) : r∗ (f n) (f m)

def Thesis.reduction_seq.elems {α : Type u_1} {r : Rel α α} {N : ℕ∞} {f : ℕ → α} (hseq : Thesis.reduction_seq r N f) : Set α

Equations

• hseq.elems = f '' {x : ℕ | ↑x < N + 1}

def Thesis.reduction_seq.start {α : Type u_1} {r : Rel α α} {N : ℕ∞} {f : ℕ → α} (hseq : Thesis.reduction_seq r N f) : α

The start of a reduction sequence is the first element of f, i.e. f 0. Note that this always holds; a reduction sequence must contain at least one element; there is no such thing as an empty reduction sequence with no elements.

Equations

• hseq.start = f 0

def Thesis.reduction_seq.end {α : Type u_1} {r : Rel α α} {f : ℕ → α} (N : ℕ) (hseq : Thesis.reduction_seq r (↑N) f) : α

Assuming N is a natural number, i.e. not infinite, hseq.end is the last element of hseq, i.e. f N.

Equations

• Thesis.reduction_seq.end N hseq = f N

def Thesis.reduction_seq.contains {α : Type u_1} {r : Rel α α} {N : ℕ∞} {f : ℕ → α} (hseq : Thesis.reduction_seq r N f) (a b : α) : Prop

Equations

• hseq.contains a b = ∃ (n : ℕ), f n = a ∧ f (n + 1) = b ∧ ↑n < N

theorem Thesis.reduction_seq.contains_step {α : Type u_1} {r : Rel α α} {N : ℕ∞} {f : ℕ → α} (hseq : Thesis.reduction_seq r N f) {a b : α} (hab : hseq.contains a b) : r a b

def Thesis.fun_aux {α : Type u_1} (N : ℕ) (f g : ℕ → α) : ℕ → α

Equations

• Thesis.fun_aux N f g n = if n ≤ N then f n else g (n - N)

def Thesis.reduction_seq.concat {α : Type u_1} {r : Rel α α} {N₁ : ℕ} {N₂ : ℕ∞} {f g : ℕ → α} (hseq : Thesis.reduction_seq r (↑N₁) f) (hseq' : Thesis.reduction_seq r N₂ g) (hend : f N₁ = g 0) : Thesis.reduction_seq r (↑N₁ + N₂) (Thesis.fun_aux N₁ f g)

Equations

• ⋯ = ⋯

def Thesis.reduction_seq.tail {α : Type u_1} {r : Rel α α} {N : ℕ∞} {f : ℕ → α} (hseq : Thesis.reduction_seq r N f) : Thesis.reduction_seq r (N - 1) fun (n : ℕ) => f (n + 1)

Equations

• ⋯ = ⋯

def Thesis.reduction_seq.flatten {α : Type u_1} {r : Rel α α} {f : ℕ → α} {N : ℕ} (hseq : Thesis.reduction_seq r∗ (↑N) f) : ∃ (N' : ℕ) (f' : ℕ → α) (hseq' : Thesis.reduction_seq r (↑N') f'), hseq.start = hseq'.start ∧ Thesis.reduction_seq.end N hseq = Thesis.reduction_seq.end N' hseq'

Equations

• ⋯ = ⋯

def Thesis.steps_reversed {α : Type u_1} : List (α × α) → List (α × α)

Equations

• Thesis.steps_reversed [] = []
• Thesis.steps_reversed (x_1 :: xs) = Thesis.steps_reversed xs ++ [(x_1.2, x_1.1)]

theorem Thesis.steps_reversed_append {α : Type u_1} {xs ys : List (α × α)} : Thesis.steps_reversed (xs ++ ys) = Thesis.steps_reversed ys ++ Thesis.steps_reversed xs

theorem Thesis.steps_reversed_mem {α : Type u_1} {s : α × α} (ss : List (α × α)) (hs : s ∈ ss) : (s.2, s.1) ∈ Thesis.steps_reversed ss

theorem Thesis.steps_reversed_add {α : Type u_1} {s : α × α} (ss : List (α × α)) : Thesis.steps_reversed (ss ++ [s]) = (s.2, s.1) :: Thesis.steps_reversed ss

@[simp]

theorem Thesis.steps_reversed_reversed {α : Type u_1} (ss : List (α × α)) : Thesis.steps_reversed (Thesis.steps_reversed ss) = ss

inductive Thesis.ReductionSeq {α : Type u_1} (r : Rel α α) : α → α → List (α × α) → Prop

ReductionSeq r x y ss represents a reduction sequence, taking reduction steps as given in ss from x to y.

An empty reduction sequence is represented by ReductionSeq.refl, allowing a reduction from x to x in 0 steps. Using ReductionSeq.head, a single step r a b can be prepended to an existing reduction sequence.

• refl: ∀ {α : Type u_1} {r : Rel α α} {x : α}, Thesis.ReductionSeq r x x []
• head: ∀ {α : Type u_1} {r : Rel α α} {x y z : α} {ss : List (α × α)}, r x y → Thesis.ReductionSeq r y z ss → Thesis.ReductionSeq r x z ((x, y) :: ss)

def Thesis.ReductionSeq.elems {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} : Thesis.ReductionSeq r x y ss → List α

Equations

• x.elems = x✝ :: List.map Prod.snd ss

def Thesis.ReductionSeq.elems' {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} : Thesis.ReductionSeq r x y ss → List α

Equations

• x.elems' = List.map Prod.fst ss ++ [y]

theorem Thesis.ReductionSeq.elems_eq_elems' {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} (hseq : Thesis.ReductionSeq r x y ss) : hseq.elems = hseq.elems'

theorem Thesis.ReductionSeq.y_elem {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} (hseq : Thesis.ReductionSeq r x y ss) : y ∈ hseq.elems

theorem Thesis.ReductionSeq.tail {α : Type u_1} {r : Rel α α} {x y z : α} {ss : List (α × α)} (hr : Thesis.ReductionSeq r x y ss) (hstep : r y z) : Thesis.ReductionSeq r x z (ss ++ [(y, z)])

theorem Thesis.ReductionSeq.concat {α : Type u_1} {r : Rel α α} {x y z : α} {ss ss' : List (α × α)} (h₁ : Thesis.ReductionSeq r x y ss) (h₂ : Thesis.ReductionSeq r y z ss') : Thesis.ReductionSeq r x z (ss ++ ss')

theorem Thesis.ReductionSeq.mem_concat {α : Type u_1} {r : Rel α α} {x y z : α} {ss ss' : List (α × α)} (hseq : Thesis.ReductionSeq r x y ss) (hseq' : Thesis.ReductionSeq r y z ss') (x✝ : α) : x✝ ∈ ⋯.elems ↔ x✝ ∈ hseq.elems ∨ x✝ ∈ hseq'.elems

If a is an element of a concatenated sequence, it must be a member of one of the two subsequences.

theorem Thesis.ReductionSeq.exists_iff_rel_star {α : Type u_1} {r : Rel α α} {x y : α} : r∗ x y ↔ ∃ (ss : List (α × α)), Thesis.ReductionSeq r x y ss

A reduction sequence exists iff there is a reflexive-transitive reduction step.

theorem Thesis.ReductionSeq.to_reduction_seq {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} (hseq : Thesis.ReductionSeq r x y ss) : ∃ (N : ℕ) (f : ℕ → α), Thesis.reduction_seq r (↑N) f ∧ (∀ x_1 ∈ hseq.elems, ∃ n < N + 1, f n = x_1) ∧ f 0 = x

theorem Thesis.ReductionSeq.of_reduction_seq {α : Type u_1} {r : Rel α α} (N : ℕ) (f : ℕ → α) (hrs : Thesis.reduction_seq r (↑N) f) : ∃ (ss : List (α × α)) (hseq : Thesis.ReductionSeq r (f 0) (f N) ss), ∀ n ≤ N, f n ∈ hseq.elems

theorem Thesis.ReductionSeq.to_reflTrans {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} (hseq : Thesis.ReductionSeq r x y ss) : r∗ x y

theorem Thesis.ReductionSeq.flatten {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} (hseq : Thesis.ReductionSeq r∗ x y ss) : ∃ (ss' : List (α × α)) (hseq' : Thesis.ReductionSeq r x y ss'), ∀ a ∈ hseq.elems, a ∈ hseq'.elems

A reflexive-transitive reduction sequence a₀ ->* a₁ ->* ... ->* aₙ can be 'flattened' (by analogy to a nested list) to a regular reduction sequence a₀ -> ... -> a₁ -> ... -> aₙ which contains all elements of the original sequence.

theorem Thesis.ReductionSeq.get_step {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} (hseq : Thesis.ReductionSeq r x y ss) (s : α × α) (hs : s ∈ ss) : r s.1 s.2

@[simp]

theorem Thesis.ReductionSeq.empty_iff {α : Type u_1} {r : Rel α α} {x y : α} : Thesis.ReductionSeq r x y [] ↔ x = y

theorem Thesis.ReductionSeq.last {α : Type u_1} {r : Rel α α} {x y : α} {ss' : List (α × α)} {b : α × α} (hseq : Thesis.ReductionSeq r x y (ss' ++ [b])) : b.2 = y

def Thesis.ReductionSeq.has_peak {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} (hseq : Thesis.ReductionSeq (SymmGen r) x y ss) : Prop

Equations

• hseq.has_peak = ∃ (n : ℕ) (h : n < ss.length - 1), r ss[n].2 ss[n].1 ∧ r ss[n + 1].1 ss[n + 1].2

theorem Thesis.ReductionSeq.step_start_stop {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} (hseq : Thesis.ReductionSeq r x y ss) (n : ℕ) (hn : n < ss.length - 1) : ss[n].2 = ss[n + 1].1

theorem Thesis.ReductionSeq.take {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} (hseq : Thesis.ReductionSeq r x y ss) (n : ℕ) (hn : n ≤ ss.length) : Thesis.ReductionSeq r x hseq.elems[n] (List.take n ss)

theorem Thesis.ReductionSeq.drop {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} (hseq : Thesis.ReductionSeq r x y ss) (n : ℕ) (hn : n ≤ ss.length) : Thesis.ReductionSeq r hseq.elems[n] y (List.drop n ss)

theorem Thesis.ReductionSeq.to_symmgen {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} (hseq : Thesis.ReductionSeq r x y ss) : Thesis.ReductionSeq (SymmGen r) x y ss

theorem Thesis.ReductionSeq.symmgen_reverse {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} (hseq : Thesis.ReductionSeq (SymmGen r) x y ss) : Thesis.ReductionSeq (SymmGen r) y x (Thesis.steps_reversed ss)

theorem Thesis.ReductionSeq.exists_iff_rel_conv {α : Type u_1} {r : Rel α α} {x y : α} : r≡ x y ↔ ∃ (ss : List (α × α)), Thesis.ReductionSeq (SymmGen r) x y ss

theorem Thesis.ReductionSeq.no_peak_cases {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} (hseq : Thesis.ReductionSeq (SymmGen r) x y ss) (hnp : ¬hseq.has_peak) : Thesis.ReductionSeq r x y ss ∨ Thesis.ReductionSeq r y x (Thesis.steps_reversed ss) ∨ ∃ (ss₁ : List (α × α)) (ss₂ : List (α × α)), ss = ss₁ ++ ss₂ ∧ ss₁ ≠ [] ∧ ss₂ ≠ [] ∧ ∃ (z : α), Thesis.ReductionSeq r x z ss₁ ∧ Thesis.ReductionSeq r y z (Thesis.steps_reversed ss₂)

theorem Thesis.ReductionSeq.reduct_of_not_peak {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} (hseq : Thesis.ReductionSeq (SymmGen r) x y ss) (hnp : ¬hseq.has_peak) : ∃ (d : α), r∗ x d ∧ r∗ y d