internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.UFormula.inversion_primrec
Proof 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 μ
this : Primrec fun x => (((equivW L μ) x).inversion.1, List.map (⇑(equivW L μ).symm) ((equivW L μ) x).inversion.2)
p : UFormula L μ
⊢ fintypeArrowEquivFinArrow (fun x => (equivW L μ) p) 0 = (equivW L μ) p
Tactic:
exact fintypeArrowEquivFinArrow_app _ _
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.inversion_primrec
Proof 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 μ
this : Primrec fun x => (((equivW L μ) x).inversion.1, List.map (⇑(equivW L μ).symm) ((equivW L μ) x).inversion.2)
a✝ : UFormula L μ
⊢ (equivW L μ).symm (fintypeArrowEquivFinArrow (fun x => (equivW L μ) a✝) 0) = a✝
Tactic:
rw[Equiv.symm_apply_eq]
Proof state after:
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 μ
this : Primrec fun x => (((equivW L μ) x).inversion.1, List.map (⇑(equivW L μ).symm) ((equivW L μ) x).inversion.2)
a✝ : UFormula L μ
⊢ fintypeArrowEquivFinArrow (fun x => (equivW L μ) a✝) 0 = (equivW L μ) a✝
Theorem: LO.FirstOrder.UFormula.inversion_primrec
Proof 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 μ
this : Primrec fun x => (((equivW L μ) x).inversion.1, List.map (⇑(equivW L μ).symm) ((equivW L μ) x).inversion.2)
a✝ : UFormula L μ
⊢ fintypeArrowEquivFinArrow (fun x => (equivW L μ) a✝) 0 = (equivW L μ) a✝
Tactic:
exact fintypeArrowEquivFinArrow_app _ _
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.ofFn_dep_FinArrow_primrec
Proof 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 σ
this : Primrec fun a => (encode a).unpair.2.unpair.2.unpair.2
⊢ Primrec fun a => encode (List.ofFn a.2.snd.2)
Tactic:
simp[←encode_finArrow]
Proof state after:
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 σ
this : Primrec fun a => (encode a).unpair.2.unpair.2.unpair.2
⊢ Primrec fun a => encode a.2.snd.2
Theorem: LO.FirstOrder.UFormula.ofFn_dep_FinArrow_primrec
Proof 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 σ
this : Primrec fun a => (encode a).unpair.2.unpair.2.unpair.2
⊢ Primrec fun a => encode a.2.snd.2
Tactic:
exact this.of_eq <| by rintro ⟨⟨⟨x, m, p⟩, l⟩, ⟨k, r, v⟩⟩; simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.ofFn_dep_FinArrow_primrec
Proof 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 σ
this : Primrec fun a => (encode a).unpair.2.unpair.2.unpair.2
⊢ ∀ (n : ((σ × ℕ × UFormula L μ₁) × List (UFormula L μ₂)) × (k : ℕ) × L.Rel k × (Fin k → UTerm L μ₁)),
    (encode n).unpair.2.unpair.2.unpair.2 = encode n.2.snd.2
Tactic:
rintro ⟨⟨⟨x, m, p⟩, l⟩, ⟨k, r, v⟩⟩
Proof 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 σ
this : Primrec fun a => (encode a).unpair.2.unpair.2.unpair.2
l : List (UFormula L μ₂)
x : σ
m : ℕ
p : UFormula L μ₁
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
⊢ (encode (((x, m, p), l), ⟨k, (r, v)⟩)).unpair.2.unpair.2.unpair.2 = encode (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.2
Theorem: LO.FirstOrder.UFormula.ofFn_dep_FinArrow_primrec
Proof 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 σ
this : Primrec fun a => (encode a).unpair.2.unpair.2.unpair.2
l : List (UFormula L μ₂)
x : σ
m : ℕ
p : UFormula L μ₁
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
⊢ (encode (((x, m, p), l), ⟨k, (r, v)⟩)).unpair.2.unpair.2.unpair.2 = encode (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.relL_finArrow_primrec
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.relL_finArrow_primrec
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.nrelL_finArrow_primrec
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.nrelL_finArrow_primrec
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bindqG_primrec
Proof 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⟩⟩
Proof 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))
Theorem: LO.FirstOrder.UFormula.bindqG_primrec
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bindqG_primrec
Proof 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⟩⟩
Proof 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))
Theorem: LO.FirstOrder.UFormula.bindqG_primrec
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof 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 μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
⊢ ∀ (b b' : σ × ℕ × UFormula L μ₁), b' ∈ LO.FirstOrder.UFormula.bindqL b → b'.2.2.depth < b.2.2.depth
Tactic:
rintro ⟨x₁, m₁, p₁⟩ ⟨x₂, m₂, p₂⟩
Proof state after:
case 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 μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
p₁ : UFormula L μ₁
x₂ : σ
m₂ : ℕ
p₂ : UFormula L μ₁
⊢ (x₂, m₂, p₂) ∈ LO.FirstOrder.UFormula.bindqL (x₁, m₁, p₁) → (x₂, m₂, p₂).2.2.depth < (x₁, m₁, p₁).2.2.depth
Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof state before:
case 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 μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
p₁ : UFormula L μ₁
x₂ : σ
m₂ : ℕ
p₂ : UFormula L μ₁
⊢ (x₂, m₂, p₂) ∈ LO.FirstOrder.UFormula.bindqL (x₁, m₁, p₁) → (x₂, m₂, p₂).2.2.depth < (x₁, m₁, p₁).2.2.depth
Tactic:
simp[bindqL]
Proof state after:
case 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 μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
p₁ : UFormula L μ₁
x₂ : σ
m₂ : ℕ
p₂ : UFormula L μ₁
⊢ (x₂, m₂, p₂) ∈
      Sum.rec (fun val => [])
        (fun val =>
          Sum.rec (fun val => [])
            (fun val =>
              Sum.rec (fun val => List.map (fun x => (x₁, m₁, x)) p₁.inversion.2)
                (fun val => List.map (fun x => (x₁, m₁ + 1, x)) p₁.inversion.2) val)
            val)
        p₁.inversion.1.2 →
    p₂.depth < p₁.depth
Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof 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 μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝¹ a✝ : UFormula L μ₁
⊢ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝¹ ∨ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝ → p₂.depth < (a✝¹.and a✝).depth
Tactic:
case and => rintro (⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩) <;> simp[depth, Nat.lt_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof 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 μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝¹ a✝ : UFormula L μ₁
⊢ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝¹ ∨ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝ → p₂.depth < (a✝¹.or a✝).depth
Tactic:
case or => rintro (⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩) <;> simp[depth, Nat.lt_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof 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 μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝ : UFormula L μ₁
⊢ x₂ = x₁ → m₂ = m₁ + 1 → p₂ = a✝ → p₂.depth < a✝.all.depth
Tactic:
case all => rintro rfl rfl rfl; simp[depth]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof 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 μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝ : UFormula L μ₁
⊢ x₂ = x₁ → m₂ = m₁ + 1 → p₂ = a✝ → p₂.depth < a✝.ex.depth
Tactic:
case ex => rintro rfl rfl rfl; simp[depth]
Proof state after:
no goals