inductive Acc {α : Sort u} (r : α → α → Prop) : α → Prop

• intro: ∀ {α : Sort u} {r : α → α → Prop} (x : α), (∀ (y : α), r y x → Acc r y) → Acc r x

@[inline, reducible]

noncomputable abbrev Acc.ndrec {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1} (m : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) {a : α} (n : Acc r a) : C a

Equations

• Acc.ndrec m n = Acc.rec m n

@[inline, reducible]

noncomputable abbrev Acc.ndrecOn {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1} {a : α} (n : Acc r a) (m : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) : C a

Equations

• Acc.ndrecOn n m = Acc.rec m n

def Acc.inv {α : Sort u} {r : α → α → Prop} {x : α} {y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y

Equations

• (_ : Acc r y) = (_ : Acc r y)

inductive WellFounded {α : Sort u} (r : α → α → Prop) : Prop

• intro: ∀ {α : Sort u} {r : α → α → Prop}, (∀ (a : α), Acc r a) → WellFounded r

class WellFoundedRelation (α : Sort u) : Sort (max 1 u)

• rel : α → α → Prop
• wf : WellFounded WellFoundedRelation.rel

def WellFounded.apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a

Equations

• (_ : Acc r a) = (_ : Acc r a)

theorem WellFounded.recursion {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r) {C : α → Sort v} (a : α) (h : (x : α) → ((y : α) → r y x → C y) → C x) : C a

theorem WellFounded.induction {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r) {C : α → Prop} (a : α) (h : ∀ (x : α), (∀ (y : α), r y x → C y) → C x) : C a

noncomputable def WellFounded.fixF {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) (a : Acc r x) : C x

Equations

• WellFounded.fixF F x a = Acc.rec (fun (x₁ : α) (h : ∀ (y : α), r y x₁ → Acc r y) (ih : (y : α) → r y x₁ → C y) => F x₁ ih) a

def WellFounded.fixFEq {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) (acx : Acc r x) : WellFounded.fixF F x acx = F x fun (y : α) (p : r y x) => WellFounded.fixF F y (_ : Acc (fun (y x : α) => r y x) y)

Equations

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

noncomputable def WellFounded.fix {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) : C x

Equations

• WellFounded.fix hwf F x = WellFounded.fixF F x (_ : Acc r x)

theorem WellFounded.fix_eq {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) : WellFounded.fix hwf F x = F x fun (y : α) (x : r y x) => WellFounded.fix hwf F y

def emptyWf {α : Sort u} : WellFoundedRelation α

Equations

• emptyWf = { rel := emptyRelation, wf := (_ : WellFounded emptyRelation) }

def Subrelation.accessible {α : Sort u} {r : α → α → Prop} {q : α → α → Prop} {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a

Equations

• (_ : Acc q a) = (_ : Acc q a)

def Subrelation.wf {α : Sort u} {r : α → α → Prop} {q : α → α → Prop} (h₁ : Subrelation q r) (h₂ : WellFounded r) : WellFounded q

Equations

• (_ : WellFounded q) = (_ : WellFounded q)

def InvImage.accessible {α : Sort u} {β : Sort v} {r : β → β → Prop} {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a

Equations

• (_ : Acc (InvImage r f) a) = (_ : Acc (InvImage r f) a)

def InvImage.wf {α : Sort u} {β : Sort v} {r : β → β → Prop} (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f)

Equations

• (_ : WellFounded (InvImage r f)) = (_ : WellFounded (InvImage r f))

@[reducible]

def invImage {α : Sort u_1} {β : Sort u_2} (f : α → β) (h : WellFoundedRelation β) : WellFoundedRelation α

Equations

• invImage f h = { rel := InvImage WellFoundedRelation.rel f, wf := (_ : WellFounded (InvImage WellFoundedRelation.rel f)) }

def TC.accessible {α : Sort u} {r : α → α → Prop} {z : α} (ac : Acc r z) : Acc (TC r) z

Equations

• (_ : Acc (TC r) z) = (_ : Acc (TC r) z)

def TC.wf {α : Sort u} {r : α → α → Prop} (h : WellFounded r) : WellFounded (TC r)

Equations

• (_ : WellFounded (TC r)) = (_ : WellFounded (TC r))

def Nat.lt_wfRel : WellFoundedRelation Nat

Equations

• Nat.lt_wfRel = { rel := Nat.lt, wf := Nat.lt_wfRel.proof_1 }

theorem Nat.strongInductionOn {motive : Nat → Sort u} (n : Nat) (ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n) : motive n

theorem Nat.caseStrongInductionOn {motive : Nat → Sort u} (a : Nat) (zero : motive 0) (ind : (n : Nat) → ((m : Nat) → m ≤ n → motive m) → motive (Nat.succ n)) : motive a

@[inline, reducible]

abbrev measure {α : Sort u} (f : α → Nat) : WellFoundedRelation α

Equations

• measure f = invImage f Nat.lt_wfRel

@[inline, reducible]

abbrev sizeOfWFRel {α : Sort u} [SizeOf α] : WellFoundedRelation α

Equations

• sizeOfWFRel = measure sizeOf

instance instWellFoundedRelation {α : Sort u_1} [SizeOf α] : WellFoundedRelation α

Equations

• instWellFoundedRelation = sizeOfWFRel

inductive Prod.Lex {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) : α × β → α × β → Prop

• left: ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} (b₁ : β) {a₂ : α} (b₂ : β), ra a₁ a₂ → Prod.Lex ra rb (a₁, b₁) (a₂, b₂)
• right: ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a : α) {b₁ b₂ : β}, rb b₁ b₂ → Prod.Lex ra rb (a, b₁) (a, b₂)

def Prod.Lex.right' {β : Type v} (rb : β → β → Prop) {a₂ : Nat} {b₂ : β} {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂)

Equations

• (_ : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂)) = (_ : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂))

inductive Prod.RProd {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) : α × β → α × β → Prop

• intro: ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} {b₁ : β} {a₂ : α} {b₂ : β}, ra a₁ a₂ → rb b₁ b₂ → Prod.RProd ra rb (a₁, b₁) (a₂, b₂)

def Prod.lexAccessible {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {a : α} (aca : Acc ra a) (acb : ∀ (b : β), Acc rb b) (b : β) : Acc (Prod.Lex ra rb) (a, b)

Equations

• (_ : Acc (Prod.Lex ra rb) (a, b)) = (_ : Acc (Prod.Lex ra rb) (a, b))

@[reducible]

def Prod.lex {α : Type u} {β : Type v} (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) : WellFoundedRelation (α × β)

Equations

• Prod.lex ha hb = { rel := Prod.Lex WellFoundedRelation.rel WellFoundedRelation.rel, wf := (_ : WellFounded (Prod.Lex WellFoundedRelation.rel WellFoundedRelation.rel)) }

instance Prod.instWellFoundedRelationProd {α : Type u} {β : Type v} [ha : WellFoundedRelation α] [hb : WellFoundedRelation β] : WellFoundedRelation (α × β)

Equations

• Prod.instWellFoundedRelationProd = Prod.lex ha hb

def Prod.RProdSubLex {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a : α × β) (b : α × β) (h : Prod.RProd ra rb a b) : Prod.Lex ra rb a b

Equations

• (_ : Prod.Lex ra rb a b) = (_ : Prod.Lex ra rb a b)

def Prod.rprod {α : Type u} {β : Type v} (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) : WellFoundedRelation (α × β)

Equations

• Prod.rprod ha hb = { rel := Prod.RProd WellFoundedRelation.rel WellFoundedRelation.rel, wf := (_ : WellFounded (Prod.RProd WellFoundedRelation.rel WellFoundedRelation.rel)) }

inductive PSigma.Lex {α : Sort u} {β : α → Sort v} (r : α → α → Prop) (s : (a : α) → β a → β a → Prop) : PSigma β → PSigma β → Prop

• left: ∀ {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} {a₁ : α} (b₁ : β a₁) {a₂ : α} (b₂ : β a₂), r a₁ a₂ → PSigma.Lex r s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }
• right: ∀ {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} (a : α) {b₁ b₂ : β a}, s a b₁ b₂ → PSigma.Lex r s { fst := a, snd := b₁ } { fst := a, snd := b₂ }

def PSigma.lexAccessible {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} {a : α} (aca : Acc r a) (acb : ∀ (a : α), WellFounded (s a)) (b : β a) : Acc (PSigma.Lex r s) { fst := a, snd := b }

Equations

• (_ : Acc (PSigma.Lex r s) { fst := a, snd := b }) = (_ : Acc (PSigma.Lex r s) { fst := a, snd := b })

@[reducible]

def PSigma.lex {α : Sort u} {β : α → Sort v} (ha : WellFoundedRelation α) (hb : (a : α) → WellFoundedRelation (β a)) : WellFoundedRelation (PSigma β)

Equations

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

instance PSigma.instWellFoundedRelationPSigma {α : Sort u} {β : α → Sort v} [ha : WellFoundedRelation α] [hb : (a : α) → WellFoundedRelation (β a)] : WellFoundedRelation (PSigma β)

Equations

• PSigma.instWellFoundedRelationPSigma = PSigma.lex ha hb

def PSigma.lexNdep {α : Sort u} {β : Sort v} (r : α → α → Prop) (s : β → β → Prop) : (_ : α) ×' β → (_ : α) ×' β → Prop

Equations

• PSigma.lexNdep r s = PSigma.Lex r fun (x : α) => s

def PSigma.lexNdepWf {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (PSigma.lexNdep r s)

Equations

• (_ : WellFounded (PSigma.lexNdep r s)) = (_ : WellFounded (PSigma.lexNdep r s))

inductive PSigma.RevLex {α : Sort u} {β : Sort v} (r : α → α → Prop) (s : β → β → Prop) : (_ : α) ×' β → (_ : α) ×' β → Prop

• left: ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} {a₁ a₂ : α} (b : β), r a₁ a₂ → PSigma.RevLex r s { fst := a₁, snd := b } { fst := a₂, snd := b }
• right: ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂ → PSigma.RevLex r s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }

def PSigma.revLexAccessible {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} {b : β} (acb : Acc s b) (aca : ∀ (a : α), Acc r a) (a : α) : Acc (PSigma.RevLex r s) { fst := a, snd := b }

Equations

• (_ : ∀ (a : α), Acc (PSigma.RevLex r s) { fst := a, snd := b }) = (_ : ∀ (a : α), Acc (PSigma.RevLex r s) { fst := a, snd := b })

def PSigma.revLex {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (PSigma.RevLex r s)

Equations

• (_ : WellFounded (PSigma.RevLex r s)) = (_ : WellFounded (PSigma.RevLex r s))

def PSigma.SkipLeft (α : Type u) {β : Type v} (s : β → β → Prop) : (_ : α) ×' β → (_ : α) ×' β → Prop

Equations

• PSigma.SkipLeft α s = PSigma.RevLex emptyRelation s

def PSigma.skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) : WellFoundedRelation ((_ : α) ×' β)

Equations

• PSigma.skipLeft α hb = { rel := PSigma.SkipLeft α WellFoundedRelation.rel, wf := (_ : WellFounded (PSigma.RevLex emptyRelation WellFoundedRelation.rel)) }

def PSigma.mkSkipLeft {α : Type u} {β : Type v} {b₁ : β} {b₂ : β} {s : β → β → Prop} (a₁ : α) (a₂ : α) (h : s b₁ b₂) : PSigma.SkipLeft α s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }

Equations

• (_ : PSigma.SkipLeft α s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }) = (_ : PSigma.RevLex emptyRelation s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ })