Theorem: LO.FirstOrder.UFormula.nrelL_finArrow_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 μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
hb : Primrec₂ b
he : Primrec₂ e
⊢ Primrec fun p =>
    UTerm.bind (shiftb (b p.1.1.1.1) p.1.1.1.2.1) (fun x => UTerm.bShifts p.1.1.1.2.1 (e p.1.1.1.1 x)) p.2
Tactic:
apply UTerm.bind_primrec_param
  (to₂ <| Primrec.ite
    (nat_lt.comp snd (fst.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst))
    (UTerm.bvar_primrec.comp snd)
    (UTerm.bShifts_primrec.comp
          (fst.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst)
          (hb.comp
            (fst.comp $ fst.comp $ fst.comp $ fst.comp fst)
            (nat_sub.comp snd (fst.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst)))))
  (by apply UTerm.bShifts_primrec.comp
        (fst.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst)
        (he.comp (fst.comp $ fst.comp $ fst.comp $ fst.comp fst) snd))
  snd
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 μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
hb : Primrec₂ b
he : Primrec₂ e
⊢ Primrec₂ fun x x_1 => UTerm.bShifts x.1.1.1.2.1 (e x.1.1.1.1 x_1)
Tactic:
apply UTerm.bShifts_primrec.comp
  (fst.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst)
  (he.comp (fst.comp $ fst.comp $ fst.comp $ fst.comp fst) snd)
State after:
no goals