Theorem: LO.FirstOrder.UFormula.bindqG_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
⊢ ∀ (n : ((σ × ℕ × UFormula L μ₁) × List (UFormula L μ₂)) × (k : ℕ) × L.Rel k × (Fin k → UTerm L μ₁)),
    relL ⟨n.2.fst, n.2.snd.1⟩
        (List.map
          (fun t => UTerm.bind (shiftb (b n.1.1.1) n.1.1.2.1) (fun x => UTerm.bShifts n.1.1.2.1 (e n.1.1.1 x)) t)
          (List.ofFn n.2.snd.2)) =
      some
        (rel n.2.snd.1 fun i =>
          UTerm.bind (shiftb (b n.1.1.1) n.1.1.2.1) (fun x => UTerm.bShifts n.1.1.2.1 (e n.1.1.1 x)) (n.2.snd.2 i))
Tactic:
rintro ⟨⟨⟨x, m, p⟩, l⟩, ⟨k, r, v⟩⟩
State after:
case mk.mk.mk.mk.mk.mk
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
l : List (UFormula L μ₂)
x : σ
m : ℕ
p : UFormula L μ₁
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
⊢ relL ⟨(((x, m, p), l), ⟨k, (r, v)⟩).2.fst, (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.1⟩
      (List.map
        (fun t =>
          UTerm.bind (shiftb (b (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1) (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1)
            (fun x_1 => UTerm.bShifts (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1 (e (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1 x_1))
            t)
        (List.ofFn (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.2)) =
    some
      (rel (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.1 fun i =>
        UTerm.bind (shiftb (b (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1) (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1)
          (fun x_1 => UTerm.bShifts (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1 (e (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1 x_1))
          ((((x, m, p), l), ⟨k, (r, v)⟩).2.snd.2 i))

State before:
case mk.mk.mk.mk.mk.mk
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
l : List (UFormula L μ₂)
x : σ
m : ℕ
p : UFormula L μ₁
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
⊢ relL ⟨(((x, m, p), l), ⟨k, (r, v)⟩).2.fst, (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.1⟩
      (List.map
        (fun t =>
          UTerm.bind (shiftb (b (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1) (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1)
            (fun x_1 => UTerm.bShifts (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1 (e (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1 x_1))
            t)
        (List.ofFn (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.2)) =
    some
      (rel (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.1 fun i =>
        UTerm.bind (shiftb (b (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1) (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1)
          (fun x_1 => UTerm.bShifts (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1 (e (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1 x_1))
          ((((x, m, p), l), ⟨k, (r, v)⟩).2.snd.2 i))
Tactic:
simp[relL]
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
⊢ ∀ (n : ((σ × ℕ × UFormula L μ₁) × List (UFormula L μ₂)) × (k : ℕ) × L.Rel k × (Fin k → UTerm L μ₁)),
    nrelL ⟨n.2.fst, n.2.snd.1⟩
        (List.map
          (fun t => UTerm.bind (shiftb (b n.1.1.1) n.1.1.2.1) (fun x => UTerm.bShifts n.1.1.2.1 (e n.1.1.1 x)) t)
          (List.ofFn n.2.snd.2)) =
      some
        (nrel n.2.snd.1 fun i =>
          UTerm.bind (shiftb (b n.1.1.1) n.1.1.2.1) (fun x => UTerm.bShifts n.1.1.2.1 (e n.1.1.1 x)) (n.2.snd.2 i))
Tactic:
rintro ⟨⟨⟨x, m, p⟩, l⟩, ⟨k, r, v⟩⟩
State after:
case mk.mk.mk.mk.mk.mk
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
l : List (UFormula L μ₂)
x : σ
m : ℕ
p : UFormula L μ₁
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
⊢ nrelL ⟨(((x, m, p), l), ⟨k, (r, v)⟩).2.fst, (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.1⟩
      (List.map
        (fun t =>
          UTerm.bind (shiftb (b (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1) (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1)
            (fun x_1 => UTerm.bShifts (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1 (e (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1 x_1))
            t)
        (List.ofFn (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.2)) =
    some
      (nrel (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.1 fun i =>
        UTerm.bind (shiftb (b (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1) (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1)
          (fun x_1 => UTerm.bShifts (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1 (e (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1 x_1))
          ((((x, m, p), l), ⟨k, (r, v)⟩).2.snd.2 i))

State before:
case mk.mk.mk.mk.mk.mk
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
l : List (UFormula L μ₂)
x : σ
m : ℕ
p : UFormula L μ₁
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
⊢ nrelL ⟨(((x, m, p), l), ⟨k, (r, v)⟩).2.fst, (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.1⟩
      (List.map
        (fun t =>
          UTerm.bind (shiftb (b (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1) (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1)
            (fun x_1 => UTerm.bShifts (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1 (e (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1 x_1))
            t)
        (List.ofFn (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.2)) =
    some
      (nrel (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.1 fun i =>
        UTerm.bind (shiftb (b (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1) (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1)
          (fun x_1 => UTerm.bShifts (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1 (e (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1 x_1))
          ((((x, m, p), l), ⟨k, (r, v)⟩).2.snd.2 i))
Tactic:
simp[nrelL]
State after:
no goals