internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Rew.free_comp_fix
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 : ℕ
⊢ free (fix &x) = &x
Tactic:
cases x <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.fix_comp_free
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.comp fix free = Rew.id
Tactic:
ext x <;> simp[comp_app]
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)
⊢ fix (free #x) = #x
Theorem: LO.FirstOrder.Rew.fix_comp_free
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)
⊢ fix (free #x) = #x
Tactic:
{ cases x using Fin.lastCases <;> simp }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.fix_comp_free
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)
⊢ fix (free #x) = #x
Tactic:
cases x using Fin.lastCases <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.bShift_free_eq_shift
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.comp free bShift = shift
Tactic:
ext x <;> simp[comp_app]
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 0
⊢ free #x.succ = #x
Theorem: LO.FirstOrder.Rew.bShift_free_eq_shift
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 0
⊢ free #x.succ = #x
Tactic:
{ exact Fin.elim0 x }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.bShift_free_eq_shift
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 0
⊢ free #x.succ = #x
Tactic:
exact Fin.elim0 x
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.bShift_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₂
v : Fin n₁ → Semiterm L ξ₂ n₂
⊢ bShift.comp (substs v) = substs (⇑bShift ∘ v)
Tactic:
ext x <;> simp[comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.shift_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₂
v : Fin n₁ → SyntacticSemiterm L n₂
⊢ Rew.comp shift (substs v) = (substs (⇑shift ∘ v)).comp shift
Tactic:
ext x <;> simp[comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.shift_comp_substs1
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 : SyntacticSemiterm L n₂
⊢ Rew.comp shift (substs ![t]) = (substs ![shift t]).comp shift
Tactic:
ext x <;> simp[comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.rewrite_comp_emb
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₂
o : Type v₁
e : IsEmpty o
f : ξ₂ → Semiterm L ξ₃ n
⊢ (rewrite f).comp emb = emb
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₂
o : Type v₁
e : IsEmpty o
f : ξ₂ → Semiterm L ξ₃ n
x : o
⊢ (rewrite f) (emb &x) = emb &x
Theorem: LO.FirstOrder.Rew.rewrite_comp_emb
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₂
o : Type v₁
e : IsEmpty o
f : ξ₂ → Semiterm L ξ₃ n
x : o
⊢ (rewrite f) (emb &x) = emb &x
Tactic:
{ exact IsEmpty.elim e x }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.rewrite_comp_emb
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₂
o : Type v₁
e : IsEmpty o
f : ξ₂ → Semiterm L ξ₃ n
x : o
⊢ (rewrite f) (emb &x) = emb &x
Tactic:
exact IsEmpty.elim e x
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.shift_comp_emb
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₂
o : Type v₁
e : IsEmpty o
⊢ Rew.comp shift emb = emb
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₂
o : Type v₁
e : IsEmpty o
x : o
⊢ shift (emb &x) = emb &x
Theorem: LO.FirstOrder.Rew.shift_comp_emb
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₂
o : Type v₁
e : IsEmpty o
x : o
⊢ shift (emb &x) = emb &x
Tactic:
{ exact IsEmpty.elim e x }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.shift_comp_emb
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₂
o : Type v₁
e : IsEmpty o
x : o
⊢ shift (emb &x) = emb &x
Tactic:
exact IsEmpty.elim e x
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.rewrite_comp_free_eq_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₂
t : SyntacticTerm L
⊢ (rewrite (t :>ₙ fvar)).comp free = substs ![t]
Tactic:
ext x <;> simp[comp_app, Fin.eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.rewrite_comp_shift_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₂
t : SyntacticTerm L
⊢ (rewrite (t :>ₙ fvar)).comp shift = Rew.id
Tactic:
ext x <;> simp[comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.substs_mbar_zero_comp_shift_eq_free
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₂
⊢ (substs ![&0]).comp shift = free
Tactic:
ext x <;> simp[comp_app, Fin.eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.substs_comp_bShift_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₂
v : Fin 1 → Semiterm L ξ 0
⊢ (substs v).comp bShift = Rew.id
Tactic:
ext x <;> simp[comp_app]
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₂
v : Fin 1 → Semiterm L ξ 0
x : Fin 0
⊢ v x.succ = #x
Theorem: LO.FirstOrder.Rew.substs_comp_bShift_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₂
v : Fin 1 → Semiterm L ξ 0
x : Fin 0
⊢ v x.succ = #x
Tactic:
exact Fin.elim0 x
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.free_comp_substs_eq_substs_comp_shift
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₂
Lf : Language
n' : ℕ
w : Fin n' → SyntacticSemiterm Lf (n + 1)
⊢ Rew.comp free (substs w) = (substs (⇑free ∘ w)).comp shift
Tactic:
ext x <;> simp[comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.rewriteMap_comp_rewriteMap
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₂
f : ξ₁ → ξ₂
g : ξ₂ → ξ₃
⊢ (rewriteMap g).comp (rewriteMap f) = rewriteMap (g ∘ f)
Tactic:
ext x <;> simp [comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.fix_free_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 : SyntacticSemiterm L (n + 1)
⊢ fix (free t) = t
Tactic:
simp[←comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.free_fix_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 : SyntacticSemiterm L n
⊢ free (fix t) = t
Tactic:
simp[←comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.free_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 : SyntacticSemiterm L 0
⊢ free (bShift t) = shift t
Tactic:
simp[←comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.substs_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 ξ 0
v : Fin 1 → Semiterm L ξ 0
⊢ (substs v) (bShift t) = t
Tactic:
simp[←comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.rewrite_comp_fix_eq_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₂
t : Semiterm L ℕ 0
⊢ (rewrite (t :>ₙ fun x => &x)).comp free = substs ![t]
Tactic:
ext x <;> simp[comp_app, Fin.eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_shift
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₂
ω : SyntacticRew L n₁ n₂
⊢ Rew.q shift = shift
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₂
ω : SyntacticRew L n₁ n₂
x : Fin (n + 1)
⊢ (Rew.q shift) #x = shift #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₂
ω : SyntacticRew L n₁ n₂
x : ℕ
⊢ (Rew.q shift) &x = shift &x
Theorem: LO.FirstOrder.Rew.q_shift
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₂
ω : SyntacticRew L n₁ n₂
x : Fin (n + 1)
⊢ (Rew.q shift) #x = shift #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₂
ω : SyntacticRew L n₁ n₂
x : ℕ
⊢ (Rew.q shift) &x = shift &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₂
ω : SyntacticRew L n₁ n₂
x : ℕ
⊢ (Rew.q shift) &x = shift &x
Theorem: LO.FirstOrder.Rew.q_shift
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₂
ω : SyntacticRew L n₁ n₂
x : ℕ
⊢ (Rew.q shift) &x = shift &x
Tactic:
{ simp }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_shift
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₂
ω : SyntacticRew L n₁ n₂
x : Fin (n + 1)
⊢ (Rew.q shift) #x = shift #x
Tactic:
cases x using Fin.cases <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_shift
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₂
ω : SyntacticRew L n₁ n₂
x : ℕ
⊢ (Rew.q shift) &x = shift &x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_free
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₂
ω : SyntacticRew L n₁ n₂
⊢ Rew.q free = free
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₂
ω : SyntacticRew L n₁ n₂
x : Fin (n + 1 + 1)
⊢ (Rew.q free) #x = free #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₂
ω : SyntacticRew L n₁ n₂
x : ℕ
⊢ (Rew.q free) &x = free &x
Theorem: LO.FirstOrder.Rew.q_free
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₂
ω : SyntacticRew L n₁ n₂
x : Fin (n + 1 + 1)
⊢ (Rew.q free) #x = free #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₂
ω : SyntacticRew L n₁ n₂
x : ℕ
⊢ (Rew.q free) &x = free &x
Tactic:
{ cases' x using Fin.cases with x <;> simp; { cases x using Fin.lastCases <;> simp[Fin.succ_castSucc] } }
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₂
ω : SyntacticRew L n₁ n₂
x : ℕ
⊢ (Rew.q free) &x = free &x
Theorem: LO.FirstOrder.Rew.q_free
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₂
ω : SyntacticRew L n₁ n₂
x : ℕ
⊢ (Rew.q free) &x = free &x
Tactic:
{ simp }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_free
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₂
ω : SyntacticRew L n₁ n₂
x : Fin (n + 1 + 1)
⊢ (Rew.q free) #x = free #x
Tactic:
cases' x using Fin.cases with x <;> simp
Proof state after:
case hb.succ
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₂
ω : SyntacticRew L n₁ n₂
x : Fin (n + 1)
⊢ bShift (free #x) = free #x.succ
Theorem: LO.FirstOrder.Rew.q_free
Proof state before:
case hb.succ
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₂
ω : SyntacticRew L n₁ n₂
x : Fin (n + 1)
⊢ bShift (free #x) = free #x.succ
Tactic:
{ cases x using Fin.lastCases <;> simp[Fin.succ_castSucc] }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_free
Proof state before:
case hb.succ
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₂
ω : SyntacticRew L n₁ n₂
x : Fin (n + 1)
⊢ bShift (free #x) = free #x.succ
Tactic:
cases x using Fin.lastCases <;> simp[Fin.succ_castSucc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_free
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₂
ω : SyntacticRew L n₁ n₂
x : ℕ
⊢ (Rew.q free) &x = free &x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_fix
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₂
ω : SyntacticRew L n₁ n₂
⊢ Rew.q fix = fix
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₂
ω : SyntacticRew L n₁ n₂
x : Fin (n + 1)
⊢ (Rew.q fix) #x = fix #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₂
ω : SyntacticRew L n₁ n₂
x : ℕ
⊢ (Rew.q fix) &x = fix &x
Theorem: LO.FirstOrder.Rew.q_fix
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₂
ω : SyntacticRew L n₁ n₂
x : Fin (n + 1)
⊢ (Rew.q fix) #x = fix #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₂
ω : SyntacticRew L n₁ n₂
x : ℕ
⊢ (Rew.q fix) &x = fix &x
Tactic:
{ cases x using Fin.cases <;> simp[Fin.succ_castSucc] }
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₂
ω : SyntacticRew L n₁ n₂
x : ℕ
⊢ (Rew.q fix) &x = fix &x
Theorem: LO.FirstOrder.Rew.q_fix
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₂
ω : SyntacticRew L n₁ n₂
x : ℕ
⊢ (Rew.q fix) &x = fix &x
Tactic:
{ cases x <;> simp }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_fix
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₂
ω : SyntacticRew L n₁ n₂
x : Fin (n + 1)
⊢ (Rew.q fix) #x = fix #x
Tactic:
cases x using Fin.cases <;> simp[Fin.succ_castSucc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_fix
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₂
ω : SyntacticRew L n₁ n₂
x : ℕ
⊢ (Rew.q fix) &x = fix &x
Tactic:
cases x <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.substs_bv
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₂
m : ℕ
t : Semiterm L ξ n
v : Fin n → Semiterm L ξ m
⊢ ((substs v) t).bv = t.bv.biUnion fun i => (v i).bv
Tactic:
induction t <;> simp [Rew.func, Semiterm.bv_func, Finset.biUnion_biUnion, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.substs_positive
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₂
m : ℕ
t : Semiterm L ξ n
v : Fin n → Semiterm L ξ (m + 1)
⊢ ((substs v) t).Positive ↔ ∀ i ∈ t.bv, (v i).Positive
Tactic:
simp [Semiterm.Positive, substs_bv]
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₂
m : ℕ
t : Semiterm L ξ n
v : Fin n → Semiterm L ξ (m + 1)
⊢ (∀ (x : Fin (m + 1)), ∀ x_1 ∈ t.bv, x ∈ (v x_1).bv → 0 < x) ↔ ∀ i ∈ t.bv, ∀ x ∈ (v i).bv, 0 < x
Theorem: LO.FirstOrder.Rew.substs_positive
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₂
m : ℕ
t : Semiterm L ξ n
v : Fin n → Semiterm L ξ (m + 1)
⊢ (∀ (x : Fin (m + 1)), ∀ x_1 ∈ t.bv, x ∈ (v x_1).bv → 0 < x) ↔ ∀ i ∈ t.bv, ∀ x ∈ (v i).bv, 0 < x
Tactic:
exact ⟨fun H i hi x hx ↦ H x i hi hx, fun H x i hi hx ↦ H i hi x hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.embSubsts_bv
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₂
m : ℕ
t : Semiterm L Empty n
v : Fin n → Semiterm L ξ m
⊢ ((embSubsts v) t).bv = t.bv.biUnion fun i => (v i).bv
Tactic:
induction t <;> simp [Rew.func, Semiterm.bv_func, Finset.biUnion_biUnion, *]
Proof state after:
case fvar
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₂
m : ℕ
v : Fin n → Semiterm L ξ m
a✝ : Empty
⊢ ((embSubsts v) &a✝).bv = ∅
Theorem: LO.FirstOrder.Rew.embSubsts_bv
Proof state before:
case fvar
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₂
m : ℕ
v : Fin n → Semiterm L ξ m
a✝ : Empty
⊢ ((embSubsts v) &a✝).bv = ∅
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.embSubsts_positive
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₂
m : ℕ
t : Semiterm L Empty n
v : Fin n → Semiterm L ξ (m + 1)
⊢ ((embSubsts v) t).Positive ↔ ∀ i ∈ t.bv, (v i).Positive
Tactic:
simp [Semiterm.Positive, embSubsts_bv]
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₂
m : ℕ
t : Semiterm L Empty n
v : Fin n → Semiterm L ξ (m + 1)
⊢ (∀ (x : Fin (m + 1)), ∀ x_1 ∈ t.bv, x ∈ (v x_1).bv → 0 < x) ↔ ∀ i ∈ t.bv, ∀ x ∈ (v i).bv, 0 < x