Theorem: LO.FirstOrder.Semiformula.bind_primrec (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
⊢ Primrec fun x => (Rew.bind (b x) (e x)).hom (p x)
Tactic:
letI : ∀ n, Primcodable { t : UTerm L μ₁ // t.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp UTerm.bv_primrec (Primrec.const n))
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => (Rew.bind (b x) (e x)).hom (p x)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => (Rew.bind (b x) (e x)).hom (p x)
Tactic:
letI : ∀ n, Primcodable { t : UTerm L μ₂ // t.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp UTerm.bv_primrec (Primrec.const n))
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => (Rew.bind (b x) (e x)).hom (p x)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => (Rew.bind (b x) (e x)).hom (p x)
Tactic:
letI : ∀ n , Primcodable { p : UFormula L μ₁ // p.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp bv_primrec (Primrec.const n))
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => (Rew.bind (b x) (e x)).hom (p x)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => (Rew.bind (b x) (e x)).hom (p x)
Tactic:
have : Primrec (fun z =>
    UFormula.bind (fun x => if hx : x < n₁ then subtEquiv (b z ⟨x, hx⟩) else default)
      (fun x => subtEquiv $ e z x) (subfEquiv (p z))
    : σ → UFormula L μ₂) :=
  UFormula.bind_primrec_param (Semiterm.brew_primrec hb)
    (subtype_val.comp₂ $ of_equiv.comp₂ $ he.comp₂ Primrec₂.left Primrec₂.right)
    (subtype_val.comp $ of_equiv.comp hp)
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this✝² : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this :
  Primrec fun z =>
    UFormula.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e z x)))
      ↑(subfEquiv (p z))
⊢ Primrec fun x => (Rew.bind (b x) (e x)).hom (p x)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this✝² : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this :
  Primrec fun z =>
    UFormula.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e z x)))
      ↑(subfEquiv (p z))
⊢ Primrec fun x => (Rew.bind (b x) (e x)).hom (p x)
Tactic:
exact encode_iff.mp <| (Primrec.encode.comp this).of_eq <| by
  intro x
  simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq, subfEquiv_bind_eq_bind]
State after:
no goals

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this✝² : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this :
  Primrec fun z =>
    UFormula.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e z x)))
      ↑(subfEquiv (p z))
⊢ ∀ (n : σ),
    encode
        (UFormula.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b n ⟨x, hx⟩)) else default)
          (fun x => ↑(subtEquiv (e n x))) ↑(subfEquiv (p n))) =
      encode ((Rew.bind (b n) (e n)).hom (p n))
Tactic:
intro x
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this✝² : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this :
  Primrec fun z =>
    UFormula.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e z x)))
      ↑(subfEquiv (p z))
x : σ
⊢ encode
      (UFormula.bind (fun x_1 => if hx : x_1 < n₁ then ↑(subtEquiv (b x ⟨x_1, hx⟩)) else default)
        (fun x_1 => ↑(subtEquiv (e x x_1))) ↑(subfEquiv (p x))) =
    encode ((Rew.bind (b x) (e x)).hom (p x))

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this✝² : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this :
  Primrec fun z =>
    UFormula.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e z x)))
      ↑(subfEquiv (p z))
x : σ
⊢ encode
      (UFormula.bind (fun x_1 => if hx : x_1 < n₁ then ↑(subtEquiv (b x ⟨x_1, hx⟩)) else default)
        (fun x_1 => ↑(subtEquiv (e x x_1))) ↑(subfEquiv (p x))) =
    encode ((Rew.bind (b x) (e x)).hom (p x))
Tactic:
simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq, subfEquiv_bind_eq_bind]
State after:
no goals