Theorem: LO.FirstOrder.Semiterm.castLE_primrec (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
h : n₁ ≤ n₂
⊢ Primrec ⇑(Rew.castLE h)
Tactic:
rw[Rew.eq_bind (Rew.castLE h)]
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
h : n₁ ≤ n₂
⊢ Primrec ⇑(Rew.bind (⇑(Rew.castLE h) ∘ bvar) (⇑(Rew.castLE h) ∘ fvar))

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
h : n₁ ≤ n₂
⊢ Primrec ⇑(Rew.bind (⇑(Rew.castLE h) ∘ bvar) (⇑(Rew.castLE h) ∘ fvar))
Tactic:
simp[Function.comp]
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
h : n₁ ≤ n₂
⊢ Primrec ⇑(Rew.bind (fun x => #(Fin.castLE h x)) fun x => &x)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
h : n₁ ≤ n₂
⊢ Primrec ⇑(Rew.bind (fun x => #(Fin.castLE h x)) fun x => &x)
Tactic:
exact bind_primrec (const _) (Semiterm.fvar_primrec.comp snd) Primrec.id
State after:
no goals