Theorems · Definition · logic and foundations

Nat.RecursiveIn.recOn

∀ {O : Set (ℕ →. ℕ)} {motive : (a : ℕ →. ℕ) → Nat.RecursiveIn O a → Prop} {a : ℕ →. ℕ} (t : Nat.RecursiveIn O a),
  motive (fun x => 0) ⋯ →
    motive ↑Nat.succ ⋯ →
      motive (fun n => ↑(some (Nat.unpair n).1)) ⋯ →
        motive (fun n => ↑(some (Nat.unpair n).2)) ⋯ →
          (∀ (g : ℕ →. ℕ) (a : g ∈ O), motive g ⋯) →
            (∀ {f h : ℕ →. ℕ} (hf : Nat.RecursiveIn O f) (hh : Nat.RecursiveIn O h),
                motive f hf → motive h hh → motive (fun n => Nat.pair <$> f n <*> h n) ⋯) →
              (∀ {f h : ℕ →. ℕ} (hf : Nat.RecursiveIn O f) (hh : Nat.RecursiveIn O h),
                  motive f hf → motive h hh → motive (fun n => h n >>= f) ⋯) →
                (∀ {f h : ℕ →. ℕ} (hf : Nat.RecursiveIn O f) (hh : Nat.RecursiveIn O h),
                    motive f hf →
                      motive h hh →
                        motive
                          (fun p =>
                            match Nat.unpair p with
                            | (a, n) =>
                              Nat.rec (f a)
                                (fun y IH => do
                                  let i ← IH
                                  h (Nat.pair a (Nat.pair y i)))
                                n)
                          ⋯) →
                  (∀ {f : ℕ →. ℕ} (hf : Nat.RecursiveIn O f),
                      motive f hf →
                        motive (fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a n)) ⋯) →
                    motive a t

Defined in

Mathlib.Computability.RecursiveIn

Cited by

0 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext