Rewriting System #

term/formula morphisms such as Rewritings, substitutions, and embeddings are handled by the structure LO.FirstOrder.Rew.

LO.FirstOrder.Rew.rewrite f is a Rewriting of the free variables occurring in the term by f : ξ₁ → Semiterm L ξ₂ n.
LO.FirstOrder.Rew.substs v is a substitution of the bounded variables occurring in the term by v : Fin n → Semiterm L ξ n'.
LO.FirstOrder.Rew.bShift is a transformation of the bounded variables occurring in the term by #x ↦ #(Fin.succ x).
LO.FirstOrder.Rew.shift is a transformation of the free variables occurring in the term by &x ↦ &(x + 1).
LO.FirstOrder.Rew.emb is a embedding of the term with no free variables.

Rewritings LO.FirstOrder.Rew is naturally converted to formula Rewritings by LO.FirstOrder.Rew.hom.

source

theorem Finset.biUnion_eq_empty {β : Type u_1} {α : Type u_2} [DecidableEq β] {s : Finset α} {f : α → Finset β} :

s.biUnion f = ∅ ↔ ∀ i ∈ s, f i = ∅

source

def LO.FirstOrder.Semiformula.rewAux {L : Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} ⦃n₁ n₂ : ℕ⦄ (ω : Rew L ξ₁ n₁ ξ₂ n₂) :

Semiformula L ξ₁ n₁ → Semiformula L ξ₂ n₂

Equations

LO.FirstOrder.Semiformula.rewAux ω LO.FirstOrder.Semiformula.verum = ⊤
LO.FirstOrder.Semiformula.rewAux ω LO.FirstOrder.Semiformula.falsum = ⊥
LO.FirstOrder.Semiformula.rewAux ω (LO.FirstOrder.Semiformula.rel r v) = LO.FirstOrder.Semiformula.rel r (⇑ω ∘ v)
LO.FirstOrder.Semiformula.rewAux ω (LO.FirstOrder.Semiformula.nrel r v) = LO.FirstOrder.Semiformula.nrel r (⇑ω ∘ v)
LO.FirstOrder.Semiformula.rewAux ω (φ.and ψ) = LO.FirstOrder.Semiformula.rewAux ω φ ⋏ LO.FirstOrder.Semiformula.rewAux ω ψ
LO.FirstOrder.Semiformula.rewAux ω (φ.or ψ) = LO.FirstOrder.Semiformula.rewAux ω φ ⋎ LO.FirstOrder.Semiformula.rewAux ω ψ
LO.FirstOrder.Semiformula.rewAux ω φ.all = ∀' LO.FirstOrder.Semiformula.rewAux ω.q φ
LO.FirstOrder.Semiformula.rewAux ω φ.ex = ∃' LO.FirstOrder.Semiformula.rewAux ω.q φ

source

theorem LO.FirstOrder.Semiformula.rewAux_neg {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (φ : Semiformula L ξ₁ n₁) :

rewAux ω (∼φ) = ∼rewAux ω φ

source

theorem LO.FirstOrder.Semiformula.ext_rewAux' {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂} (h : ω₁ = ω₂) (φ : Semiformula L ξ₁ n₁) :

rewAux ω₁ φ = rewAux ω₂ φ

source

def LO.FirstOrder.Semiformula.rew {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) :

Semiformula L ξ₁ n₁ →ˡᶜ Semiformula L ξ₂ n₂

Equations

LO.FirstOrder.Semiformula.rew ω = { toTr := LO.FirstOrder.Semiformula.rewAux ω, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }

source

instance LO.FirstOrder.Semiformula.instRewriting {L : Language} {ξ : Type u_2} {ζ : Type u_3} :

Rewriting L ξ (Semiformula L ξ) ζ (Semiformula L ζ)

Equations

LO.FirstOrder.Semiformula.instRewriting = { app := fun {n₁ n₂ : ℕ} => LO.FirstOrder.Semiformula.rew, app_all := ⋯, app_ex := ⋯ }

source

theorem LO.FirstOrder.Semiformula.rew_rel {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ₁ n₁) :

(Rewriting.app ω) (rel r v) = rel r fun (i : Fin k) => ω (v i)

source

theorem LO.FirstOrder.Semiformula.rew_nrel {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ₁ n₁) :

(Rewriting.app ω) (nrel r v) = nrel r fun (i : Fin k) => ω (v i)

source

theorem LO.FirstOrder.Semiformula.rew_rel' {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (rel r v) = rel r (⇑ω ∘ v)

source

theorem LO.FirstOrder.Semiformula.nrel' {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (nrel r v) = nrel r (⇑ω ∘ v)

source

@[simp]

theorem LO.FirstOrder.Semiformula.rew_rel0 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 0} {v : Fin 0 → Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (rel r v) = rel r ![]

source

@[simp]

theorem LO.FirstOrder.Semiformula.rew_rel1 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 1} {t : Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (rel r ![t]) = rel r ![ω t]

source

@[simp]

theorem LO.FirstOrder.Semiformula.rew_rel2 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 2} {t₁ t₂ : Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (rel r ![t₁, t₂]) = rel r ![ω t₁, ω t₂]

source

@[simp]

theorem LO.FirstOrder.Semiformula.rew_rel3 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 3} {t₁ t₂ t₃ : Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (rel r ![t₁, t₂, t₃]) = rel r ![ω t₁, ω t₂, ω t₃]

source

@[simp]

theorem LO.FirstOrder.Semiformula.rew_nrel0 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 0} {v : Fin 0 → Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (nrel r v) = nrel r ![]

source

@[simp]

theorem LO.FirstOrder.Semiformula.rew_nrel1 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 1} {t : Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (nrel r ![t]) = nrel r ![ω t]

source

@[simp]

theorem LO.FirstOrder.Semiformula.rew_nrel2 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 2} {t₁ t₂ : Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (nrel r ![t₁, t₂]) = nrel r ![ω t₁, ω t₂]

source

@[simp]

theorem LO.FirstOrder.Semiformula.rew_nrel3 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 3} {t₁ t₂ t₃ : Semiterm L ξ₁ n₁} :

(Rewriting.app ω) (nrel r ![t₁, t₂, t₃]) = nrel r ![ω t₁, ω t₂, ω t₃]

source

instance LO.FirstOrder.Semiformula.instReflectiveRewriting {L : Language} {ξ : Type u_2} :

ReflectiveRewriting L ξ (Semiformula L ξ)

source

instance LO.FirstOrder.Semiformula.instTransitiveRewriting {L : Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {ξ₃ : Type u_4} :

TransitiveRewriting L ξ₁ (Semiformula L ξ₁) ξ₂ (Semiformula L ξ₂) ξ₃ (Semiformula L ξ₃)

source

instance LO.FirstOrder.Semiformula.instInjMapRewriting {L : Language} {ξ : Type u_2} {ζ : Type u_3} :

InjMapRewriting L ξ (Semiformula L ξ) ζ (Semiformula L ζ)

source

instance LO.FirstOrder.Semiformula.instLawfulSyntacticRewritingSyntacticSemiformula {L : Language} :

LawfulSyntacticRewriting L (SyntacticSemiformula L)

source

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_rew {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (φ : Semiformula L ξ₁ n₁) :

((Rewriting.app ω) φ).complexity = φ.complexity

source

@[simp]

theorem LO.FirstOrder.Semiformula.eq_top_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} :

(Rewriting.app ω) φ = ⊤ ↔ φ = ⊤

source

@[simp]

theorem LO.FirstOrder.Semiformula.eq_bot_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} :

(Rewriting.app ω) φ = ⊥ ↔ φ = ⊥

source

theorem LO.FirstOrder.Semiformula.eq_rel_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ξ₂ n₂} :

(Rewriting.app ω) φ = rel r v ↔ ∃ (v' : Fin k → Semiterm L ξ₁ n₁), ⇑ω ∘ v' = v ∧ φ = rel r v'

source

theorem LO.FirstOrder.Semiformula.eq_nrel_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ξ₂ n₂} :

(Rewriting.app ω) φ = nrel r v ↔ ∃ (v' : Fin k → Semiterm L ξ₁ n₁), ⇑ω ∘ v' = v ∧ φ = nrel r v'

source

@[simp]

theorem LO.FirstOrder.Semiformula.eq_and_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : Semiformula L ξ₂ n₂} :

(Rewriting.app ω) φ = ψ₁ ⋏ ψ₂ ↔ ∃ (φ₁ : Semiformula L ξ₁ n₁) (φ₂ : Semiformula L ξ₁ n₁), (Rewriting.app ω) φ₁ = ψ₁ ∧ (Rewriting.app ω) φ₂ = ψ₂ ∧ φ = φ₁ ⋏ φ₂

source

@[simp]

theorem LO.FirstOrder.Semiformula.eq_or_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : Semiformula L ξ₂ n₂} :

(Rewriting.app ω) φ = ψ₁ ⋎ ψ₂ ↔ ∃ (φ₁ : Semiformula L ξ₁ n₁) (φ₂ : Semiformula L ξ₁ n₁), (Rewriting.app ω) φ₁ = ψ₁ ∧ (Rewriting.app ω) φ₂ = ψ₂ ∧ φ = φ₁ ⋎ φ₂

source

theorem LO.FirstOrder.Semiformula.eq_all_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ : Semiformula L ξ₂ (n₂ + 1)} :

(Rewriting.app ω) φ = ∀' ψ ↔ ∃ (φ' : Semiformula L ξ₁ (n₁ + 1)), (Rewriting.app ω.q) φ' = ψ ∧ φ = ∀' φ'

source

theorem LO.FirstOrder.Semiformula.eq_ex_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ : Semiformula L ξ₂ (n₂ + 1)} :

(Rewriting.app ω) φ = ∃' ψ ↔ ∃ (φ' : Semiformula L ξ₁ (n₁ + 1)), (Rewriting.app ω.q) φ' = ψ ∧ φ = ∃' φ'

source

@[simp]

theorem LO.FirstOrder.Semiformula.eq_neg_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : Semiformula L ξ₂ n₂} :

(Rewriting.app ω) φ = ψ₁ ➝ ψ₂ ↔ ∃ (φ₁ : Semiformula L ξ₁ n₁) (φ₂ : Semiformula L ξ₁ n₁), (Rewriting.app ω) φ₁ = ψ₁ ∧ (Rewriting.app ω) φ₂ = ψ₂ ∧ φ = φ₁ ➝ φ₂

source

theorem LO.FirstOrder.Semiformula.eq_ball_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : Semiformula L ξ₂ (n₂ + 1)} :

((Rewriting.app ω) φ = ∀[ψ₁] ψ₂) ↔ ∃ (φ₁ : Semiformula L ξ₁ (n₁ + 1)) (φ₂ : Semiformula L ξ₁ (n₁ + 1)), (Rewriting.app ω.q) φ₁ = ψ₁ ∧ (Rewriting.app ω.q) φ₂ = ψ₂ ∧ φ = ∀[φ₁] φ₂

source

theorem LO.FirstOrder.Semiformula.eq_bex_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : Semiformula L ξ₂ (n₂ + 1)} :

((Rewriting.app ω) φ = ∃[ψ₁] ψ₂) ↔ ∃ (φ₁ : Semiformula L ξ₁ (n₁ + 1)) (φ₂ : Semiformula L ξ₁ (n₁ + 1)), (Rewriting.app ω.q) φ₁ = ψ₁ ∧ (Rewriting.app ω.q) φ₂ = ψ₂ ∧ φ = ∃[φ₁] φ₂

source

instance LO.FirstOrder.Semiformula.instCoeSemisentenceSyntacticSemiformula {L : Language} {n : ℕ} :

Coe (Semisentence L n) (SyntacticSemiformula L n)

Equations

LO.FirstOrder.Semiformula.instCoeSemisentenceSyntacticSemiformula = { coe := LO.FirstOrder.Rewriting.embedding }

source

@[simp]

theorem LO.FirstOrder.Semiformula.coe_inj {L : Language} {n : ℕ} (σ π : Semisentence L n) :

↑σ = ↑π ↔ σ = π

source

theorem LO.FirstOrder.Semiformula.coe_substitute_eq_substitute_coe {L : Language} {k n : ℕ} (φ : Semisentence L k) (v : Fin k → Semiterm L Empty n) :

↑(φ ⇜ v) = ↑φ ⇜ fun (i : Fin k) => Rew.emb (v i)

source

theorem LO.FirstOrder.Semiformula.coe_substs_eq_substs_coe₁ {L : Language} {n : ℕ} (φ : Semisentence L 1) (t : Semiterm L Empty n) :

↑(φ/[t]) = ↑φ/[Rew.emb t]

source

@[irreducible]

def LO.FirstOrder.Semiformula.formulaRec {L : Language} {C : SyntacticFormula L → Sort u_2} (verum : C ⊤) (falsum : C ⊥) (rel : {l : ℕ} → (r : L.Rel l) → (v : Fin l → SyntacticTerm L) → C (rel r v)) (nrel : {l : ℕ} → (r : L.Rel l) → (v : Fin l → SyntacticTerm L) → C (nrel r v)) (and : (φ ψ : SyntacticFormula L) → C φ → C ψ → C (φ ⋏ ψ)) (or : (φ ψ : SyntacticFormula L) → C φ → C ψ → C (φ ⋎ ψ)) (all : (φ : SyntacticSemiformula L 1) → C (Rewriting.free φ) → C (∀' φ)) (ex : (φ : SyntacticSemiformula L 1) → C (Rewriting.free φ) → C (∃' φ)) (φ : SyntacticFormula L) :

C φ

Equations

One or more equations did not get rendered due to their size.
LO.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex LO.FirstOrder.Semiformula.verum = verum
LO.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex LO.FirstOrder.Semiformula.falsum = falsum
LO.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex (LO.FirstOrder.Semiformula.rel r v) = rel r v
LO.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex (LO.FirstOrder.Semiformula.nrel r v) = nrel r v

source

theorem LO.FirstOrder.Semiformula.fvar?_rew {ξ₁ : Type u_1} {ξ₂ : Type u_2} {L : Language} {n₁ n₂ : ℕ} [DecidableEq ξ₁] [DecidableEq ξ₂] {φ : Semiformula L ξ₁ n₁} {ω : Rew L ξ₁ n₁ ξ₂ n₂} {x : ξ₂} (h : ((Rewriting.app ω) φ).FVar? x) :

(∃ (i : Fin n₁), (ω (Semiterm.bvar i)).FVar? x) ∨ ∃ (z : ξ₁), φ.FVar? z ∧ (ω (Semiterm.fvar z)).FVar? x

source

@[simp]

theorem LO.FirstOrder.Semiformula.freeVariables_emb {ξ : Type u_2} {L : Language} {n : ℕ} [DecidableEq ξ] {ο : Type u_1} [IsEmpty ο] (φ : Semiformula L ο n) :

(↑φ).freeVariables = ∅

source

theorem LO.FirstOrder.Semiformula.rew_eq_of_funEqOn {ξ₁ : Type u_1} {L : Language} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} [DecidableEq ξ₁] {ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂} {φ : Semiformula L ξ₁ n₁} (hb : ∀ (x : Fin n₁), ω₁ (Semiterm.bvar x) = ω₂ (Semiterm.bvar x)) (hf : Function.funEqOn φ.FVar? (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)) :

(Rewriting.app ω₁) φ = (Rewriting.app ω₂) φ

source

theorem LO.FirstOrder.Semiformula.rew_eq_of_funEqOn₀ {ξ₁ : Type u_1} {L : Language} {ξ₂ : Type u_3} {n₂ : ℕ} [DecidableEq ξ₁] {ω₁ ω₂ : Rew L ξ₁ 0 ξ₂ n₂} {φ : Semiformula L ξ₁ 0} (hf : Function.funEqOn φ.FVar? (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)) :

(Rewriting.app ω₁) φ = (Rewriting.app ω₂) φ

source

theorem LO.FirstOrder.Semiformula.rew_eq_self_of {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] {ω : Rew L ξ n ξ n} {φ : Semiformula L ξ n} (hb : ∀ (x : Fin n), ω (Semiterm.bvar x) = Semiterm.bvar x) (hf : ∀ (x : ξ), φ.FVar? x → ω (Semiterm.fvar x) = Semiterm.fvar x) :

(Rewriting.app ω) φ = φ

source

@[simp]

theorem LO.FirstOrder.Semiformula.ex_ne_subst {L : Language} {ξ : Type u_2} (φ : Semiformula L ξ 1) (t : Semiterm L ξ 0) :

φ/[t] ≠ ∃' φ

source

@[simp]

theorem LO.FirstOrder.Semiformula.fvSup_sentence {L : Language} {n : ℕ} (σ : Semisentence L n) :

(↑σ).fvSup = 0

source

@[simp]

theorem LO.FirstOrder.Semiformula.substs_comp_fixitr_eq_map {L : Language} (φ : SyntacticFormula L) (f : ℕ → SyntacticTerm L) :

((Rewriting.app (Rew.fixitr 0 (fvSup φ))) φ ⇜ fun (x : Fin (0 + fvSup φ)) => f ↑x) = (Rewriting.app (Rew.rewrite f)) φ

source

@[simp]

theorem LO.FirstOrder.Semiformula.substs_comp_fixitr {L : Language} (φ : SyntacticFormula L) :

((Rewriting.app (Rew.fixitr 0 (fvSup φ))) φ ⇜ fun (x : Fin (0 + fvSup φ)) => Semiterm.fvar ↑x) = φ

source

def LO.FirstOrder.Semiformula.close {L : Language} (φ : SyntacticFormula L) :

SyntacticFormula L

Equations

LO.FirstOrder.Semiformula.close φ = ∀* (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.fixitr 0 (LO.FirstOrder.Semiformula.fvSup φ))) φ

source

def LO.FirstOrder.«term∀∀_» :

Lean.ParserDescr

Equations

LO.FirstOrder.«term∀∀_» = Lean.ParserDescr.node `LO.FirstOrder.«term∀∀_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀∀") (Lean.ParserDescr.cat `term 1024))

source

@[simp]

theorem LO.FirstOrder.Semiformula.rew_close {L : Language} (φ : SyntacticFormula L) (ω : SyntacticRew L 0 0) :

(Rewriting.app ω) (close φ) = close φ

source

theorem LO.FirstOrder.Semiformula.close_eq_self_of {L : Language} (φ : SyntacticFormula L) (h : freeVariables φ = ∅) :

close φ = φ

source

@[simp]

theorem LO.FirstOrder.Semiformula.fvarList_close {L : Language} (φ : SyntacticFormula L) :

freeVariables (close φ) = ∅

source

@[simp]

theorem LO.FirstOrder.Semiformula.close_close_eq_close {L : Language} (φ : SyntacticFormula L) :

close (close φ) = close φ

source

def LO.FirstOrder.Semiformula.toEmpty {ξ : Type u_1} {L : Language} [DecidableEq ξ] {n : ℕ} (φ : Semiformula L ξ n) :

φ.freeVariables = ∅ → Semisentence L n

Equations

(LO.FirstOrder.Semiformula.rel R v).toEmpty h = LO.FirstOrder.Semiformula.rel R fun (i : Fin arity) => (v i).toEmpty ⋯
(LO.FirstOrder.Semiformula.nrel R v).toEmpty h = LO.FirstOrder.Semiformula.nrel R fun (i : Fin arity) => (v i).toEmpty ⋯
LO.FirstOrder.Semiformula.verum.toEmpty x_2 = ⊤
LO.FirstOrder.Semiformula.falsum.toEmpty x_2 = ⊥
(φ.and ψ).toEmpty h = φ.toEmpty ⋯ ⋏ ψ.toEmpty ⋯
(φ.or ψ).toEmpty h = φ.toEmpty ⋯ ⋎ ψ.toEmpty ⋯
φ.all.toEmpty h = ∀' φ.toEmpty h
φ.ex.toEmpty h = ∃' φ.toEmpty h

source

@[simp]

theorem LO.FirstOrder.Semiformula.emb_toEmpty {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ n) (hp : φ.freeVariables = ∅) :

↑(φ.toEmpty hp) = φ

source

@[simp]

theorem LO.FirstOrder.Semiformula.toEmpty_verum {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] :

⊤.toEmpty ⋯ = ⊤

source

@[simp]

theorem LO.FirstOrder.Semiformula.toEmpty_falsum {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] :

⊥.toEmpty ⋯ = ⊥

source

@[simp]

theorem LO.FirstOrder.Semiformula.toEmpty_and {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ ψ : Semiformula L ξ n) (h : (φ ⋏ ψ).freeVariables = ∅) :

(φ ⋏ ψ).toEmpty h = φ.toEmpty ⋯ ⋏ ψ.toEmpty ⋯

source

@[simp]

theorem LO.FirstOrder.Semiformula.toEmpty_or {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ ψ : Semiformula L ξ n) (h : (φ ⋎ ψ).freeVariables = ∅) :

(φ ⋎ ψ).toEmpty h = φ.toEmpty ⋯ ⋎ ψ.toEmpty ⋯

source

@[simp]

theorem LO.FirstOrder.Semiformula.toEmpty_all {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ (n + 1)) (h : (∀' φ).freeVariables = ∅) :

(∀' φ).toEmpty h = ∀' φ.toEmpty h

source

@[simp]

theorem LO.FirstOrder.Semiformula.toEmpty_ex {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ (n + 1)) (h : (∃' φ).freeVariables = ∅) :

(∃' φ).toEmpty h = ∃' φ.toEmpty h

source

def LO.FirstOrder.Semiformula.close₀ {L : Language} (φ : SyntacticFormula L) :

Sentence L

Equations

LO.FirstOrder.Semiformula.close₀ φ = LO.FirstOrder.Semiformula.toEmpty (LO.FirstOrder.Semiformula.close φ) ⋯

source

def LO.FirstOrder.«term∀∀₀_» :

Lean.ParserDescr

Equations

LO.FirstOrder.«term∀∀₀_» = Lean.ParserDescr.node `LO.FirstOrder.«term∀∀₀_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀∀₀") (Lean.ParserDescr.cat `term 1024))

source

theorem LO.FirstOrder.Semiformula.lMap_bind {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {ξ₁ : Type u_3} (b : Fin n₁ → Semiterm L₁ ξ₂ n₂) (e : ξ₁ → Semiterm L₁ ξ₂ n₂) (φ : Semiformula L₁ ξ₁ n₁) :

(lMap Φ) ((Rewriting.app (Rew.bind b e)) φ) = (Rewriting.app (Rew.bind (Semiterm.lMap Φ ∘ b) (Semiterm.lMap Φ ∘ e))) ((lMap Φ) φ)

source

theorem LO.FirstOrder.Semiformula.lMap_map {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n₁ n₂ : ℕ} {ξ₁ : Type u_2} {ξ₂ : Type u_3} (b : Fin n₁ → Fin n₂) (e : ξ₁ → ξ₂) (φ : Semiformula L₁ ξ₁ n₁) :

(lMap Φ) ((Rewriting.app (Rew.map b e)) φ) = (Rewriting.app (Rew.map b e)) ((lMap Φ) φ)

source

theorem LO.FirstOrder.Semiformula.lMap_rewrite {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n : ℕ} (f : ξ₁ → Semiterm L₁ ξ₂ n) (φ : Semiformula L₁ ξ₁ n) :

(lMap Φ) ((Rewriting.app (Rew.rewrite f)) φ) = (Rewriting.app (Rew.rewrite (Semiterm.lMap Φ ∘ f))) ((lMap Φ) φ)

source

theorem LO.FirstOrder.Semiformula.lMap_substs {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {Φ : L₁.Hom L₂} {k n : ℕ} (w : Fin k → Semiterm L₁ ξ n) (φ : Semiformula L₁ ξ k) :

(lMap Φ) (φ ⇜ w) = (lMap Φ) φ ⇜ (Semiterm.lMap Φ ∘ w)

source

theorem LO.FirstOrder.Semiformula.lMap_shift {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n : ℕ} (φ : SyntacticSemiformula L₁ n) :

(lMap Φ) ((Rewriting.app Rew.shift) φ) = (Rewriting.app Rew.shift) ((lMap Φ) φ)

source

theorem LO.FirstOrder.Semiformula.lMap_free {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n : ℕ} (φ : SyntacticSemiformula L₁ (n + 1)) :

(lMap Φ) ((Rewriting.app Rew.free) φ) = (Rewriting.app Rew.free) ((lMap Φ) φ)

source

theorem LO.FirstOrder.Semiformula.lMap_fix {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n : ℕ} (φ : SyntacticSemiformula L₁ n) :

(lMap Φ) ((Rewriting.app Rew.fix) φ) = (Rewriting.app Rew.fix) ((lMap Φ) φ)

source

theorem LO.FirstOrder.Semiformula.lMap_emb {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {Φ : L₁.Hom L₂} {n : ℕ} {ο : Type u_2} [IsEmpty ο] (φ : Semiformula L₁ ο n) :

(lMap Φ) ↑φ = ↑((lMap Φ) φ)

source

theorem LO.FirstOrder.Semiformula.lMap_toS {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n : ℕ} (φ : Semiformula L₁ (Fin n) 0) :

(lMap Φ) ((Rewriting.app Rew.toS) φ) = (Rewriting.app Rew.toS) ((lMap Φ) φ)

source

theorem LO.FirstOrder.Semiformula.lMap_rewriteMap {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {ξ₁ : Type u_2} {n : ℕ} {ξ₂ : Type u_3} (φ : Semiformula L₁ ξ₁ n) (f : ξ₁ → ξ₂) :

(lMap Φ) ((Rewriting.app (Rew.rewriteMap f)) φ) = (Rewriting.app (Rew.rewriteMap f)) ((lMap Φ) φ)

source

@[simp]

theorem LO.FirstOrder.Semiformula.rew_open_iff {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} {ω : Rew L ξ₁ n₁ ξ₂ n₂} {φ : Semiformula L ξ₁ n₁} :

((Rewriting.app ω) φ).Open ↔ φ.Open

Documentation

Foundation.FirstOrder.Basic.Syntax.Rew

Rewriting System #