Theorem: LO.FirstOrder.UTerm.bv_primrec (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
⊢ Primrec bv
Tactic:
have : Primrec (elim (L := L) (μ := μ) Nat.succ (fun _ => 0) fun {k} _ v => (List.ofFn v).sup) :=
  elim_primrec Primrec.succ (Primrec.const 0) ((list_sup nat_max).comp₂ Primrec₂.right)
State after:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this : Primrec (elim Nat.succ (fun x => 0) fun {k} x v => (List.ofFn v).sup)
⊢ Primrec bv

State before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this : Primrec (elim Nat.succ (fun x => 0) fun {k} x v => (List.ofFn v).sup)
⊢ Primrec bv
Tactic:
exact this.of_eq (fun t => by
  induction t <;> simp[elim, bv, *]
  { simp[List.sup_ofFn] })
State after:
no goals

State before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this : Primrec (elim Nat.succ (fun x => 0) fun {k} x v => (List.ofFn v).sup)
t : UTerm L μ
⊢ elim Nat.succ (fun x => 0) (fun {k} x v => (List.ofFn v).sup) t = t.bv
Tactic:
induction t <;> simp[elim, bv, *]
State after:
case func
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this : Primrec (elim Nat.succ (fun x => 0) fun {k} x v => (List.ofFn v).sup)
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ
a_ih✝ : ∀ (a : Fin arity✝), elim Nat.succ (fun x => 0) (fun {k} x v => (List.ofFn v).sup) (a✝ a) = (a✝ a).bv
⊢ (List.ofFn fun i => (a✝ i).bv).sup = Finset.univ.sup fun i => (a✝ i).bv

State before:
case func
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this : Primrec (elim Nat.succ (fun x => 0) fun {k} x v => (List.ofFn v).sup)
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ
a_ih✝ : ∀ (a : Fin arity✝), elim Nat.succ (fun x => 0) (fun {k} x v => (List.ofFn v).sup) (a✝ a) = (a✝ a).bv
⊢ (List.ofFn fun i => (a✝ i).bv).sup = Finset.univ.sup fun i => (a✝ i).bv
Tactic:
{ simp[List.sup_ofFn] }
State after:
no goals

State before:
case func
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this : Primrec (elim Nat.succ (fun x => 0) fun {k} x v => (List.ofFn v).sup)
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ
a_ih✝ : ∀ (a : Fin arity✝), elim Nat.succ (fun x => 0) (fun {k} x v => (List.ofFn v).sup) (a✝ a) = (a✝ a).bv
⊢ (List.ofFn fun i => (a✝ i).bv).sup = Finset.univ.sup fun i => (a✝ i).bv
Tactic:
simp[List.sup_ofFn]
State after:
no goals