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

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

@[inline]

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]

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.inv = @Acc.inv.proof_1

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 rel

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

Equations

• @WellFounded.apply = @WellFounded.apply.proof_1

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 ih => 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 => WellFounded.fixF F y (_ : Acc (fun y x => r y x) y)

Equations

• @WellFounded.fixFEq = @WellFounded.fixFEq.proof_1

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 => 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

• @Subrelation.accessible = @Subrelation.accessible.proof_1

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

Equations

• @Subrelation.wf = @Subrelation.wf.proof_1

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

Equations

• @InvImage.accessible = @InvImage.accessible.proof_1

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

Equations

• @InvImage.wf = @InvImage.wf.proof_1

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

• @TC.accessible = @TC.accessible.proof_1

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

Equations

• @TC.wf = @TC.wf.proof_1

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

def Measure {α : Sort u} : (α → Nat) → α → α → Prop

Equations

• Measure = InvImage fun a b => a < b

@[inline]

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

Equations

• measure f = invImage f Nat.lt_wfRel

def SizeOfRef (α : Sort u) [inst : SizeOf α] : α → α → Prop

Equations

• SizeOfRef α = Measure sizeOf

@[inline]

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

Equations

• sizeOfWFRel = measure sizeOf

instance instWellFoundedRelation {α : Sort u_1} [inst : 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.right' = @Prod.Lex.right'.proof_1

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} (aca : ∀ (a : α), Acc ra a) (acb : ∀ (b : β), Acc rb b) (a : α) (b : β) : Acc (Prod.Lex ra rb) (a, b)

Equations

• @Prod.lexAccessible = @Prod.lexAccessible.proof_1

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.RProdSubLex = @Prod.RProdSubLex.proof_1

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

• @PSigma.lexAccessible = @PSigma.lexAccessible.proof_1

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

• @PSigma.lexNdepWf = @PSigma.lexNdepWf.proof_1

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

• @PSigma.revLexAccessible = @PSigma.revLexAccessible.proof_1

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

Equations

• @PSigma.revLex = @PSigma.revLex.proof_1

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.mkSkipLeft = @PSigma.mkSkipLeft.proof_1