internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Rew.substs_zero
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
n' : ℕ
w✝ : Fin n → Semiterm L ξ n'
w : Fin 0 → Term L ξ
⊢ substs w = Rew.id
Tactic:
ext x <;> simp
Proof state after:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
n' : ℕ
w✝ : Fin n → Semiterm L ξ n'
w : Fin 0 → Term L ξ
x : Fin 0
⊢ w x = #x
Theorem: LO.FirstOrder.Rew.substs_zero
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
n' : ℕ
w✝ : Fin n → Semiterm L ξ n'
w : Fin 0 → Term L ξ
x : Fin 0
⊢ w x = #x
Tactic:
{ exact Fin.elim0 x }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.substs_zero
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
n' : ℕ
w✝ : Fin n → Semiterm L ξ n'
w : Fin 0 → Term L ξ
x : Fin 0
⊢ w x = #x
Tactic:
exact Fin.elim0 x
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.substs_comp_substs
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
n' : ℕ
w✝ : Fin n → Semiterm L ξ n'
l k : ℕ
v : Fin l → Semiterm L ξ k
w : Fin k → Semiterm L ξ n
⊢ (substs w).comp (substs v) = substs (⇑(substs w) ∘ v)
Tactic:
ext <;> simp[comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.substs_eq_id
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
n' : ℕ
w : Fin n → Semiterm L ξ n'
⊢ substs bvar = Rew.id
Tactic:
ext <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.castLe_eq_id
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
h : n ≤ n
⊢ castLE h = Rew.id
Tactic:
ext <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.embSubsts_bvar
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
w : Fin k → Semiterm L ξ n
x : Fin k
⊢ (embSubsts w) #x = w x
Tactic:
simp[embSubsts]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.embSubsts_zero
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
w✝ : Fin k → Semiterm L ξ n
w : Fin 0 → Term L ξ
⊢ embSubsts w = emb
Tactic:
ext x <;> try simp
Proof state after:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
w✝ : Fin k → Semiterm L ξ n
w : Fin 0 → Term L ξ
x : Fin 0
⊢ w x = #x

case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
w✝ : Fin k → Semiterm L ξ n
w : Fin 0 → Term L ξ
x : Empty
⊢ (embSubsts w) &x = emb &x
Theorem: LO.FirstOrder.Rew.embSubsts_zero
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
w✝ : Fin k → Semiterm L ξ n
w : Fin 0 → Term L ξ
x : Fin 0
⊢ (embSubsts w) #x = emb #x
Tactic:
simp
Proof state after:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
w✝ : Fin k → Semiterm L ξ n
w : Fin 0 → Term L ξ
x : Fin 0
⊢ w x = #x
Theorem: LO.FirstOrder.Rew.embSubsts_zero
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
w✝ : Fin k → Semiterm L ξ n
w : Fin 0 → Term L ξ
x : Fin 0
⊢ w x = #x
Tactic:
exact Fin.elim0 x
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.embSubsts_zero
Proof state before:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
w✝ : Fin k → Semiterm L ξ n
w : Fin 0 → Term L ξ
x : Empty
⊢ (embSubsts w) &x = emb &x
Tactic:
exact Empty.elim x
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.substs_comp_embSubsts
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
w✝ : Fin k → Semiterm L ξ n
l : ℕ
v : Fin l → Semiterm L ξ k
w : Fin k → Semiterm L ξ n
⊢ (substs w).comp (embSubsts v) = embSubsts (⇑(substs w) ∘ v)
Tactic:
ext x <;> simp[comp_app]
Proof state after:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
w✝ : Fin k → Semiterm L ξ n
l : ℕ
v : Fin l → Semiterm L ξ k
w : Fin k → Semiterm L ξ n
x : Empty
⊢ (substs w) ((embSubsts v) &x) = (embSubsts (⇑(substs w) ∘ v)) &x
Theorem: LO.FirstOrder.Rew.substs_comp_embSubsts
Proof state before:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
w✝ : Fin k → Semiterm L ξ n
l : ℕ
v : Fin l → Semiterm L ξ k
w : Fin k → Semiterm L ξ n
x : Empty
⊢ (substs w) ((embSubsts v) &x) = (embSubsts (⇑(substs w) ∘ v)) &x
Tactic:
exact Empty.elim x
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.embSubsts_eq_id
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
w : Fin k → Semiterm L ξ n
⊢ embSubsts bvar = emb
Tactic:
ext x <;> try simp
Proof state after:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
w : Fin k → Semiterm L ξ n
x : Empty
⊢ (embSubsts bvar) &x = emb &x
Theorem: LO.FirstOrder.Rew.embSubsts_eq_id
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
w : Fin k → Semiterm L ξ n
x : Fin n
⊢ (embSubsts bvar) #x = emb #x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.embSubsts_eq_id
Proof state before:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
w : Fin k → Semiterm L ξ n
x : Empty
⊢ (embSubsts bvar) &x = emb &x
Tactic:
exact Empty.elim x
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_bvar_zero
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
⊢ ω.q #0 = #0
Tactic:
simp[Rew.q]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_bvar_succ
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
i : Fin n₁
⊢ ω.q #i.succ = bShift (ω #i)
Tactic:
simp[Rew.q]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_fvar
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
x : ξ₁
⊢ ω.q &x = bShift (ω &x)
Tactic:
simp[Rew.q]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_comp_bShift
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
⊢ ω.q.comp bShift = bShift.comp ω
Tactic:
ext x <;> simp[comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_comp_bShift_app
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Semiterm L ξ₁ n₁
⊢ ω.q (bShift t) = bShift (ω t)
Tactic:
have := ext' (ω.q_comp_bShift) t
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Semiterm L ξ₁ n₁
this : (ω.q.comp bShift) t = (bShift.comp ω) t
⊢ ω.q (bShift t) = bShift (ω t)
Theorem: LO.FirstOrder.Rew.q_comp_bShift_app
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Semiterm L ξ₁ n₁
this : (ω.q.comp bShift) t = (bShift.comp ω) t
⊢ ω.q (bShift t) = bShift (ω t)
Tactic:
simpa only [comp_app] using this
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_id
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
⊢ Rew.id.q = Rew.id
Tactic:
ext x
Proof state after:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
x : Fin (n + 1)
⊢ Rew.id.q #x = Rew.id #x

case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
x : ξ
⊢ Rew.id.q &x = Rew.id &x
Theorem: LO.FirstOrder.Rew.q_id
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
x : Fin (n + 1)
⊢ Rew.id.q #x = Rew.id #x

case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
x : ξ
⊢ Rew.id.q &x = Rew.id &x
Tactic:
{ cases x using Fin.cases <;> simp }
Proof state after:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
x : ξ
⊢ Rew.id.q &x = Rew.id &x
Theorem: LO.FirstOrder.Rew.q_id
Proof state before:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
x : ξ
⊢ Rew.id.q &x = Rew.id &x
Tactic:
{ simp }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_id
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
x : Fin (n + 1)
⊢ Rew.id.q #x = Rew.id #x
Tactic:
cases x using Fin.cases <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_id
Proof state before:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
x : ξ
⊢ Rew.id.q &x = Rew.id &x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_eq_zero_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Semiterm L ξ₁ (n₁ + 1)
⊢ ω.q t = #0 ↔ t = #0
Tactic:
cases t <;> simp [Rew.func]
Proof state after:
case bvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
a✝ : Fin (n₁ + 1)
⊢ ω.q #a✝ = #0 ↔ a✝ = 0
Theorem: LO.FirstOrder.Rew.q_eq_zero_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
i : Fin (n₁ + 1)
⊢ ω.q #i = #0 ↔ i = 0
Tactic:
case bvar i =>
  cases i using Fin.cases <;> simp [Fin.succ_ne_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_eq_zero_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
i : Fin (n₁ + 1)
⊢ ω.q #i = #0 ↔ i = 0
Tactic:
cases i using Fin.cases <;> simp [Fin.succ_ne_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Semiterm L ξ₁ (n₁ + 1)
⊢ (ω.q t).Positive ↔ t.Positive
Tactic:
induction t <;> simp [Rew.func, *]
Proof state after:
case bvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
a✝ : Fin (n₁ + 1)
⊢ (ω.q #a✝).Positive ↔ 0 < a✝
Theorem: LO.FirstOrder.Rew.q_positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
x : Fin (n₁ + 1)
⊢ (ω.q #x).Positive ↔ 0 < x
Tactic:
case bvar x =>
  cases x using Fin.cases <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
x : Fin (n₁ + 1)
⊢ (ω.q #x).Positive ↔ 0 < x
Tactic:
cases x using Fin.cases <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.qpow_id
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
⊢ Rew.id.qpow k = Rew.id
Tactic:
induction k <;> simp[*]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_comp
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
⊢ (ω₂.comp ω₁).q = ω₂.q.comp ω₁.q
Tactic:
ext x
Proof state after:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
x : Fin (n₁ + 1)
⊢ (ω₂.comp ω₁).q #x = (ω₂.q.comp ω₁.q) #x

case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
x : ξ₁
⊢ (ω₂.comp ω₁).q &x = (ω₂.q.comp ω₁.q) &x
Theorem: LO.FirstOrder.Rew.q_comp
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
x : Fin (n₁ + 1)
⊢ (ω₂.comp ω₁).q #x = (ω₂.q.comp ω₁.q) #x

case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
x : ξ₁
⊢ (ω₂.comp ω₁).q &x = (ω₂.q.comp ω₁.q) &x
Tactic:
{ cases x using Fin.cases <;> simp[comp_app] }
Proof state after:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
x : ξ₁
⊢ (ω₂.comp ω₁).q &x = (ω₂.q.comp ω₁.q) &x
Theorem: LO.FirstOrder.Rew.q_comp
Proof state before:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
x : ξ₁
⊢ (ω₂.comp ω₁).q &x = (ω₂.q.comp ω₁.q) &x
Tactic:
{ simp[comp_app] }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_comp
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
x : Fin (n₁ + 1)
⊢ (ω₂.comp ω₁).q #x = (ω₂.q.comp ω₁.q) #x
Tactic:
cases x using Fin.cases <;> simp[comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_comp
Proof state before:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
x : ξ₁
⊢ (ω₂.comp ω₁).q &x = (ω₂.q.comp ω₁.q) &x
Tactic:
simp[comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.qpow_comp
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
⊢ (ω₂.comp ω₁).qpow k = (ω₂.qpow k).comp (ω₁.qpow k)
Tactic:
induction k <;> simp[*, q_comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_bind
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
⊢ (bind b e).q = bind (#0 :> ⇑bShift ∘ b) (⇑bShift ∘ e)
Tactic:
ext x
Proof state after:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
x : Fin (n₁ + 1)
⊢ (bind b e).q #x = (bind (#0 :> ⇑bShift ∘ b) (⇑bShift ∘ e)) #x

case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
x : ξ₁
⊢ (bind b e).q &x = (bind (#0 :> ⇑bShift ∘ b) (⇑bShift ∘ e)) &x
Theorem: LO.FirstOrder.Rew.q_bind
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
x : Fin (n₁ + 1)
⊢ (bind b e).q #x = (bind (#0 :> ⇑bShift ∘ b) (⇑bShift ∘ e)) #x

case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
x : ξ₁
⊢ (bind b e).q &x = (bind (#0 :> ⇑bShift ∘ b) (⇑bShift ∘ e)) &x
Tactic:
{ cases x using Fin.cases <;> simp }
Proof state after:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
x : ξ₁
⊢ (bind b e).q &x = (bind (#0 :> ⇑bShift ∘ b) (⇑bShift ∘ e)) &x
Theorem: LO.FirstOrder.Rew.q_bind
Proof state before:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
x : ξ₁
⊢ (bind b e).q &x = (bind (#0 :> ⇑bShift ∘ b) (⇑bShift ∘ e)) &x
Tactic:
{ simp }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_bind
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
x : Fin (n₁ + 1)
⊢ (bind b e).q #x = (bind (#0 :> ⇑bShift ∘ b) (⇑bShift ∘ e)) #x
Tactic:
cases x using Fin.cases <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_bind
Proof state before:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
x : ξ₁
⊢ (bind b e).q &x = (bind (#0 :> ⇑bShift ∘ b) (⇑bShift ∘ e)) &x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_map
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
⊢ (map b e).q = map (0 :> Fin.succ ∘ b) e
Tactic:
ext x
Proof state after:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
x : Fin (n₁ + 1)
⊢ (map b e).q #x = (map (0 :> Fin.succ ∘ b) e) #x

case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
x : ξ₁
⊢ (map b e).q &x = (map (0 :> Fin.succ ∘ b) e) &x
Theorem: LO.FirstOrder.Rew.q_map
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
x : Fin (n₁ + 1)
⊢ (map b e).q #x = (map (0 :> Fin.succ ∘ b) e) #x

case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
x : ξ₁
⊢ (map b e).q &x = (map (0 :> Fin.succ ∘ b) e) &x
Tactic:
{ cases x using Fin.cases <;> simp }
Proof state after:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
x : ξ₁
⊢ (map b e).q &x = (map (0 :> Fin.succ ∘ b) e) &x