def Acc.SeqCnd {α : Type u_1} (r : α → α → Prop) (x y : α) : Prop

Equations

• Acc.SeqCnd r x y = (r y x ∧ ¬Acc r y)

noncomputable def Acc.seqNext {α : Type u_1} (r : α → α → Prop) (x : α) : α

Equations

• Acc.seqNext r x = (choose? (Acc.SeqCnd r x)).getD x

noncomputable def Acc.mkSeq {α : Type u_1} (r : α → α → Prop) (x : α) (n : ℕ) : α

Equations

• Acc.mkSeq r x 0 = x
• Acc.mkSeq r x n_2.succ = Acc.seqNext r (Acc.mkSeq r x n_2)

theorem Acc.not_linearOrder_imp_wellFounded : ¬∀ {α : Type} [inst : LinearOrder α], WellFounded fun (xs ys : List α) => xs < ys

@[simp]

theorem Acc.mkSeq_zero {α : Type u_1} {r : α → α → Prop} {x : α} : mkSeq r x 0 = x

theorem Acc.acc_iff {α : Type u_1} {r : α → α → Prop} {x : α} : Acc r x ↔ ∀ ⦃y : α⦄, r y x → Acc r y

theorem Acc.not_acc_iff {α : Type u_1} {r : α → α → Prop} {x : α} : ¬Acc r x ↔ ∃ (y : α), r y x ∧ ¬Acc r y

theorem Acc.not_acc_iff_seqCnd {α : Type u_1} {r : α → α → Prop} {x : α} : ¬Acc r x ↔ ∃ (y : α), SeqCnd r x y

theorem Acc.not_acc_iff_seqNext {α : Type u_1} {r : α → α → Prop} {x : α} : ¬Acc r x ↔ SeqCnd r x (seqNext r x)

theorem Acc.exi_seq_of_not_acc {α : Type u_1} {r : α → α → Prop} {x : α} (h : ¬Acc r x) : ∃ (a : ℕ → α), r (a 0) x ∧ ∀ (n : ℕ), r (a (n + 1)) (a n)

theorem Acc.acc_of_not_seq {α : Type u_1} {r : α → α → Prop} {x : α} (h : ∀ (a : ℕ → α), r (a 0) x → ∃ (n : ℕ), ¬r (a (n + 1)) (a n)) : Acc r x

theorem Acc.acc_iff_not_seq' {α : Type u_1} {r : α → α → Prop} {x : α} : Acc r x ↔ ¬∃ (a : ℕ → α), r (a 0) x ∧ ∀ (n : ℕ), r (a (n + 1)) (a n)

theorem Acc.acc_iff_not_seq {α : Type u_1} {r : α → α → Prop} {x : α} : Acc r x ↔ ∀ (a : ℕ → α), r (a 0) x → ∃ (n : ℕ), ¬r (a (n + 1)) (a n)