Documentation

Init.WF

inductive Acc {α : Sort u} (r : ααProp) :
αProp
  • intro: ∀ {α : Sort u} {r : ααProp} (x : α), (∀ (y : α), r y xAcc r y)Acc r x
Instances For
    @[inline, reducible]
    noncomputable abbrev Acc.ndrec {α : Sort u2} {r : ααProp} {C : αSort u1} (m : (x : α) → (∀ (y : α), r y xAcc r y)((y : α) → r y xC y)C x) {a : α} (n : Acc r a) :
    C a
    Equations
    Instances For
      @[inline, reducible]
      noncomputable abbrev Acc.ndrecOn {α : Sort u2} {r : ααProp} {C : αSort u1} {a : α} (n : Acc r a) (m : (x : α) → (∀ (y : α), r y xAcc r y)((y : α) → r y xC y)C x) :
      C a
      Equations
      Instances For
        def Acc.inv {α : Sort u} {r : ααProp} {x : α} {y : α} (h₁ : Acc r x) (h₂ : r y x) :
        Acc r y
        Equations
        Instances For
          inductive WellFounded {α : Sort u} (r : ααProp) :
          Instances For
            class WellFoundedRelation (α : Sort u) :
            Sort (max 1 u)
            Instances
              def WellFounded.apply {α : Sort u} {r : ααProp} (wf : WellFounded r) (a : α) :
              Acc r a
              Equations
              Instances For
                theorem WellFounded.recursion {α : Sort u} {r : ααProp} (hwf : WellFounded r) {C : αSort v} (a : α) (h : (x : α) → ((y : α) → r y xC y)C x) :
                C a
                theorem WellFounded.induction {α : Sort u} {r : ααProp} (hwf : WellFounded r) {C : αProp} (a : α) (h : ∀ (x : α), (∀ (y : α), r y xC y)C x) :
                C a
                noncomputable def WellFounded.fixF {α : Sort u} {r : ααProp} {C : αSort v} (F : (x : α) → ((y : α) → r y xC 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
                Instances For
                  def WellFounded.fixFEq {α : Sort u} {r : ααProp} {C : αSort v} (F : (x : α) → ((y : α) → r y xC 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.
                  Instances For
                    noncomputable def WellFounded.fix {α : Sort u} {C : αSort v} {r : ααProp} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y xC y)C x) (x : α) :
                    C x
                    Equations
                    Instances For
                      theorem WellFounded.fix_eq {α : Sort u} {C : αSort v} {r : ααProp} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y xC y)C x) (x : α) :
                      WellFounded.fix hwf F x = F x fun (y : α) (x : r y x) => WellFounded.fix hwf F y
                      Equations
                      • emptyWf = { rel := emptyRelation, wf := (_ : WellFounded emptyRelation) }
                      Instances For
                        def Subrelation.accessible {α : Sort u} {r : ααProp} {q : ααProp} {a : α} (h₁ : Subrelation q r) (ac : Acc r a) :
                        Acc q a
                        Equations
                        Instances For
                          def Subrelation.wf {α : Sort u} {r : ααProp} {q : ααProp} (h₁ : Subrelation q r) (h₂ : WellFounded r) :
                          Equations
                          Instances For
                            def InvImage.accessible {α : Sort u} {β : Sort v} {r : ββProp} {a : α} (f : αβ) (ac : Acc r (f a)) :
                            Acc (InvImage r f) a
                            Equations
                            Instances For
                              def InvImage.wf {α : Sort u} {β : Sort v} {r : ββProp} (f : αβ) (h : WellFounded r) :
                              Equations
                              Instances For
                                @[reducible]
                                def invImage {α : Sort u_1} {β : Sort u_2} (f : αβ) (h : WellFoundedRelation β) :
                                Equations
                                Instances For
                                  def TC.accessible {α : Sort u} {r : ααProp} {z : α} (ac : Acc r z) :
                                  Acc (TC r) z
                                  Equations
                                  Instances For
                                    def TC.wf {α : Sort u} {r : ααProp} (h : WellFounded r) :
                                    Equations
                                    Instances For
                                      theorem Nat.strongInductionOn {motive : NatSort u} (n : Nat) (ind : (n : Nat) → ((m : Nat) → m < nmotive m)motive n) :
                                      motive n
                                      theorem Nat.caseStrongInductionOn {motive : NatSort u} (a : Nat) (zero : motive 0) (ind : (n : Nat) → ((m : Nat) → m nmotive m)motive (Nat.succ n)) :
                                      motive a
                                      @[inline, reducible]
                                      abbrev measure {α : Sort u} (f : αNat) :
                                      Equations
                                      Instances For
                                        @[inline, reducible]
                                        abbrev sizeOfWFRel {α : Sort u} [SizeOf α] :
                                        Equations
                                        Instances For
                                          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₂)
                                          Instances For
                                            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
                                            Instances For
                                              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₂)
                                              Instances For
                                                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
                                                Instances For
                                                  @[reducible]
                                                  def Prod.lex {α : Type u} {β : Type v} (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) :
                                                  Equations
                                                  Instances For
                                                    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
                                                    Instances For
                                                      def Prod.rprod {α : Type u} {β : Type v} (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) :
                                                      Equations
                                                      Instances For
                                                        inductive PSigma.Lex {α : Sort u} {β : αSort v} (r : ααProp) (s : (a : α) → β aβ aProp) :
                                                        PSigma βPSigma βProp
                                                        • left: ∀ {α : Sort u} {β : αSort v} {r : ααProp} {s : (a : α) → β aβ aProp} {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β aProp} (a : α) {b₁ b₂ : β a}, s a b₁ b₂PSigma.Lex r s { fst := a, snd := b₁ } { fst := a, snd := b₂ }
                                                        Instances For
                                                          def PSigma.lexAccessible {α : Sort u} {β : αSort v} {r : ααProp} {s : (a : α) → β aβ aProp} {a : α} (aca : Acc r a) (acb : ∀ (a : α), WellFounded (s a)) (b : β a) :
                                                          Acc (PSigma.Lex r s) { fst := a, snd := b }
                                                          Equations
                                                          Instances For
                                                            @[reducible]
                                                            def PSigma.lex {α : Sort u} {β : αSort v} (ha : WellFoundedRelation α) (hb : (a : α) → WellFoundedRelation (β a)) :
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              instance PSigma.instWellFoundedRelationPSigma {α : Sort u} {β : αSort v} [ha : WellFoundedRelation α] [hb : (a : α) → WellFoundedRelation (β a)] :
                                                              Equations
                                                              • PSigma.instWellFoundedRelationPSigma = PSigma.lex ha hb
                                                              def PSigma.lexNdep {α : Sort u} {β : Sort v} (r : ααProp) (s : ββProp) :
                                                              (_ : α) ×' β(_ : α) ×' βProp
                                                              Equations
                                                              Instances For
                                                                def PSigma.lexNdepWf {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} (ha : WellFounded r) (hb : WellFounded s) :
                                                                Equations
                                                                Instances For
                                                                  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₂ }
                                                                  Instances For
                                                                    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
                                                                    Instances For
                                                                      def PSigma.revLex {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} (ha : WellFounded r) (hb : WellFounded s) :
                                                                      Equations
                                                                      Instances For
                                                                        def PSigma.SkipLeft (α : Type u) {β : Type v} (s : ββProp) :
                                                                        (_ : α) ×' β(_ : α) ×' βProp
                                                                        Equations
                                                                        Instances For
                                                                          def PSigma.skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) :
                                                                          WellFoundedRelation ((_ : α) ×' β)
                                                                          Equations
                                                                          Instances For
                                                                            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₂ })
                                                                            Instances For