internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiformula.neg_primrec
Proof 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
n : ℕ
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).neg
p : Semiformula L μ n
⊢ encode (↑(subfEquiv p)).neg = encode (~p)
Tactic:
simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq, subfEquiv_neg_eq_neg_subfEquiv]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.bv_subtEquiv
Proof 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
n : ℕ
p : Semiformula L μ n
⊢ (↑(subfEquiv p)).bv ≤ n
Tactic:
induction p <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.subfEquiv_bind_eq_bind
Proof 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
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
p : Semiformula L μ₁ n₁
⊢ ↑(subfEquiv ((Rew.bind b e).hom p)) =
    UFormula.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(subfEquiv p)
Tactic:
induction p using rec' generalizing n₂ μ₂ e <;>
  simp [Semiterm.subtEquiv_bind_eq_bind, bindq, Rew.rel, Rew.nrel, UFormula.bind,
    ofSubterm_eq_subtEquiv, ofSubformula_eq_subfEquiv, *]
Proof state after:
case hall
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
n₁ : ℕ
μ₁ : Type u_3
n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (n✝ + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p✝)) =
      UFormula.bind (fun x => if hx : x < n✝ + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p✝)
μ₂ : Type u_2
n₂ : ℕ
b : Fin n✝ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ↑(subfEquiv ((Rew.bind b e).q.hom p✝)) =
    bindq (fun x => if hx : x < n✝ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x))) 1
      ↑(subfEquiv p✝)

case hex
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
n₁ : ℕ
μ₁ : Type u_3
n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (n✝ + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p✝)) =
      UFormula.bind (fun x => if hx : x < n✝ + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p✝)
μ₂ : Type u_2
n₂ : ℕ
b : Fin n✝ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ↑(subfEquiv ((Rew.bind b e).q.hom p✝)) =
    bindq (fun x => if hx : x < n✝ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x))) 1
      ↑(subfEquiv p✝)
Theorem: LO.FirstOrder.Semiformula.subfEquiv_bind_eq_bind
Proof 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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ↑(subfEquiv ((Rew.bind b e).q.hom p)) =
    bindq (fun x => if hx : x < k then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x))) 1
      ↑(subfEquiv p)
Tactic:
simp[Rew.q_bind, ih, bindq_eq_bind]
Proof 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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default)
      (fun x => ↑(subtEquiv (Rew.bShift (e x)))) ↑(subfEquiv p) =
    UFormula.bind (shiftb (fun x => if hx : x < k then ↑(subtEquiv (b ⟨x, hx⟩)) else default) 1)
      (fun x => bShifts 1 ↑(subtEquiv (e x))) ↑(subfEquiv p)
Theorem: LO.FirstOrder.Semiformula.subfEquiv_bind_eq_bind
Proof 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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default)
      (fun x => ↑(subtEquiv (Rew.bShift (e x)))) ↑(subfEquiv p) =
    UFormula.bind (shiftb (fun x => if hx : x < k then ↑(subtEquiv (b ⟨x, hx⟩)) else default) 1)
      (fun x => bShifts 1 ↑(subtEquiv (e x))) ↑(subfEquiv p)
Tactic:
apply UFormula.bind_eq_bind_of_eq
Proof state after:
case hb
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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ∀ x < (↑(subfEquiv p)).bv,
    (if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default) =
      shiftb (fun x => if hx : x < k then ↑(subtEquiv (b ⟨x, hx⟩)) else default) 1 x

case he
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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ∀ (x : μ₁), ↑(subtEquiv (Rew.bShift (e x))) = bShifts 1 ↑(subtEquiv (e x))
Theorem: LO.FirstOrder.Semiformula.subfEquiv_bind_eq_bind
Proof state before:
case hb
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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ∀ x < (↑(subfEquiv p)).bv,
    (if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default) =
      shiftb (fun x => if hx : x < k then ↑(subtEquiv (b ⟨x, hx⟩)) else default) 1 x
Tactic:
intro x hx
Proof state after:
case hb
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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x < (↑(subfEquiv p)).bv
⊢ (if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default) =
    shiftb (fun x => if hx : x < k then ↑(subtEquiv (b ⟨x, hx⟩)) else default) 1 x
Theorem: LO.FirstOrder.Semiformula.subfEquiv_bind_eq_bind
Proof state before:
case hb
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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x < (↑(subfEquiv p)).bv
⊢ (if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default) =
    shiftb (fun x => if hx : x < k then ↑(subtEquiv (b ⟨x, hx⟩)) else default) 1 x
Tactic:
simp[shiftb]
Proof state after:
case hb
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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x < (↑(subfEquiv p)).bv
⊢ (if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default) =
    if x = 0 then bvar x else bShifts 1 (if hx : x - 1 < k then ↑(subtEquiv (b ⟨x - 1, hx⟩)) else default)
Theorem: LO.FirstOrder.Semiformula.subfEquiv_bind_eq_bind
Proof state before:
case hb
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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x < (↑(subfEquiv p)).bv
⊢ (if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default) =
    if x = 0 then bvar x else bShifts 1 (if hx : x - 1 < k then ↑(subtEquiv (b ⟨x - 1, hx⟩)) else default)
Tactic:
cases' x with x <;> simp[Nat.succ_eq_add_one]
Proof state after:
case hb.succ
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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x + 1 < (↑(subfEquiv p)).bv
⊢ (if h : x < k then ↑(subtEquiv (Rew.bShift (b ⟨x, ⋯⟩))) else default) =
    bShifts 1 (if h : x < k then ↑(subtEquiv (b ⟨x, ⋯⟩)) else default)
Theorem: LO.FirstOrder.Semiformula.subfEquiv_bind_eq_bind
Proof state before:
case hb.succ
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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x + 1 < (↑(subfEquiv p)).bv
⊢ (if h : x < k then ↑(subtEquiv (Rew.bShift (b ⟨x, ⋯⟩))) else default) =
    bShifts 1 (if h : x < k then ↑(subtEquiv (b ⟨x, ⋯⟩)) else default)
Tactic:
have : x < k := Nat.succ_lt_succ_iff.mp (lt_of_lt_of_le hx (bv_subtEquiv p))
Proof state after:
case hb.succ
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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x + 1 < (↑(subfEquiv p)).bv
this : x < k
⊢ (if h : x < k then ↑(subtEquiv (Rew.bShift (b ⟨x, ⋯⟩))) else default) =
    bShifts 1 (if h : x < k then ↑(subtEquiv (b ⟨x, ⋯⟩)) else default)
Theorem: LO.FirstOrder.Semiformula.subfEquiv_bind_eq_bind
Proof state before:
case hb.succ
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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x + 1 < (↑(subfEquiv p)).bv
this : x < k
⊢ (if h : x < k then ↑(subtEquiv (Rew.bShift (b ⟨x, ⋯⟩))) else default) =
    bShifts 1 (if h : x < k then ↑(subtEquiv (b ⟨x, ⋯⟩)) else default)
Tactic:
simp[this, Semiterm.subtEquiv_bShift_eq_bShift]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.subfEquiv_bind_eq_bind
Proof state before:
case he
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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ∀ (x : μ₁), ↑(subtEquiv (Rew.bShift (e x))) = bShifts 1 ↑(subtEquiv (e x))
Tactic:
intro x
Proof state after:
case he
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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : μ₁
⊢ ↑(subtEquiv (Rew.bShift (e x))) = bShifts 1 ↑(subtEquiv (e x))
Theorem: LO.FirstOrder.Semiformula.subfEquiv_bind_eq_bind
Proof state before:
case he
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
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : μ₁
⊢ ↑(subtEquiv (Rew.bShift (e x))) = bShifts 1 ↑(subtEquiv (e x))
Tactic:
exact Semiterm.subtEquiv_bShift_eq_bShift (e x)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.bind_primrec
Proof 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))
Proof 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)
Theorem: LO.FirstOrder.Semiformula.bind_primrec
Proof 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))
Proof 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)
Theorem: LO.FirstOrder.Semiformula.bind_primrec
Proof 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))
Proof 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)