Theorems · Definition · logic and foundations

Nat.RecursiveIn.below.casesOn

∀ {O : Set (ℕ →. ℕ)} {motive : (a : ℕ →. ℕ) → Nat.RecursiveIn O a → Prop}
  {motive_1 : {a : ℕ →. ℕ} → (t : Nat.RecursiveIn O a) → Nat.RecursiveIn.below t → Prop} {a : ℕ →. ℕ}
  {t : Nat.RecursiveIn O a} (t_1 : Nat.RecursiveIn.below t),
  motive_1 ⋯ ⋯ →
    motive_1 ⋯ ⋯ →
      motive_1 ⋯ ⋯ →
        motive_1 ⋯ ⋯ →
          (∀ (g : ℕ →. ℕ) (a : g ∈ O), motive_1 ⋯ ⋯) →
            (∀ {f h : ℕ →. ℕ} (hf : Nat.RecursiveIn O f) (hh : Nat.RecursiveIn O h) (ih : Nat.RecursiveIn.below hf)
                (hf_ih : motive f hf) (ih_1 : Nat.RecursiveIn.below hh) (hh_ih : motive h hh), motive_1 ⋯ ⋯) →
              (∀ {f h : ℕ →. ℕ} (hf : Nat.RecursiveIn O f) (hh : Nat.RecursiveIn O h) (ih : Nat.RecursiveIn.below hf)
                  (hf_ih : motive f hf) (ih_1 : Nat.RecursiveIn.below hh) (hh_ih : motive h hh), motive_1 ⋯ ⋯) →
                (∀ {f h : ℕ →. ℕ} (hf : Nat.RecursiveIn O f) (hh : Nat.RecursiveIn O h) (ih : Nat.RecursiveIn.below hf)
                    (hf_ih : motive f hf) (ih_1 : Nat.RecursiveIn.below hh) (hh_ih : motive h hh), motive_1 ⋯ ⋯) →
                  (∀ {f : ℕ →. ℕ} (hf : Nat.RecursiveIn O f) (ih : Nat.RecursiveIn.below hf) (hf_ih : motive f hf),
                      motive_1 ⋯ ⋯) →
                    motive_1 t t_1

Defined in

Mathlib.Computability.RecursiveIn

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext