Theorem: LO.FirstOrder.UFormula.depth_primrec (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec depth
Tactic:
have := elim_primrec (L := L) (μ := μ) 0 0 (const 0) (const 0) (succ.comp₂ nat_max) (succ.comp₂ nat_max) succ succ
State after:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this :
  Primrec
    (elim 0 0 (fun {k} f v => 0) (fun {k} f v => 0) (fun a b => (max a b).succ) (fun a b => (max a b).succ) Nat.succ
      Nat.succ)
⊢ Primrec depth

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this :
  Primrec
    (elim 0 0 (fun {k} f v => 0) (fun {k} f v => 0) (fun a b => (max a b).succ) (fun a b => (max a b).succ) Nat.succ
      Nat.succ)
⊢ Primrec depth
Tactic:
exact this.of_eq <| fun p => by induction p <;> simp[elim, depth, *]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this :
  Primrec
    (elim 0 0 (fun {k} f v => 0) (fun {k} f v => 0) (fun a b => (max a b).succ) (fun a b => (max a b).succ) Nat.succ
      Nat.succ)
p : UFormula L μ
⊢ elim 0 0 (fun {k} f v => 0) (fun {k} f v => 0) (fun a b => (max a b).succ) (fun a b => (max a b).succ) Nat.succ
      Nat.succ p =
    p.depth
Tactic:
induction p <;> simp[elim, depth, *]
State after:
no goals