LeanPool.FormalizationOfBoundedArithmetic.Syntax #

source

def FirstOrder.Language.BoundedFormula.iSup' {L : Language} {α β : Type u} {n : ℕ} [enum : IsEnum β] (f : β → L.BoundedFormula α n) :

L.BoundedFormula α n

Computable finite supremum over an explicitly enumerated type.

Equations

FirstOrder.Language.BoundedFormula.iSup' f = List.foldr (fun (x1 x2 : L.BoundedFormula α n) => x1 ⊔ x2) ⊥ (List.map f IsEnum.toList)

Instances For

source

def FirstOrder.Language.BoundedFormula.iInf' {L : Language} {α β : Type u} {n : ℕ} [enum : IsEnum β] (f : β → L.BoundedFormula α n) :

L.BoundedFormula α n

Computable finite infimum over an explicitly enumerated type.

Equations

FirstOrder.Language.BoundedFormula.iInf' f = List.foldr (fun (x1 x2 : L.BoundedFormula α n) => x1 ⊓ x2) ⊤ (List.map f IsEnum.toList)

Instances For

source

def FirstOrder.Language.Formula.iAlls' {L : Language} {α β : Type u} [enum : IsEnum β] (φ : L.Formula (α ⊕ β)) :

L.Formula α

Computable finite universal closure over an explicitly enumerated type.

Equations

φ.iAlls' = (FirstOrder.Language.BoundedFormula.relabel (fun (a : α ⊕ β) => Sum.map id IsEnum.toIdx a) φ).alls

Instances For

source

def FirstOrder.Language.Formula.iExs' {L : Language} {α β : Type u} [enum : IsEnum β] (φ : L.Formula (α ⊕ β)) :

L.Formula α

Computable finite existential closure over an explicitly enumerated type.

Equations

φ.iExs' = (FirstOrder.Language.BoundedFormula.relabel (fun (a : α ⊕ β) => Sum.map id IsEnum.toIdx a) φ).exs

Instances For

source

def FirstOrder.Language.Formula.iExsUnique' {L : Language} {α β : Type u} [enum : IsEnum β] (φ : L.Formula (α ⊕ β)) :

L.Formula α

Computable finite unique-existence formula over an explicitly enumerated type.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def FirstOrder.Language.Formula.iSup' {L : Language} {α β : Type u} [enum : IsEnum α] (f : α → L.Formula β) :

L.Formula β

Computable finite supremum for formulas over an explicitly enumerated type.

Equations

FirstOrder.Language.Formula.iSup' f = FirstOrder.Language.BoundedFormula.iSup' f

Instances For

source

def FirstOrder.Language.Formula.iInf' {L : Language} {α β : Type u} [enum : IsEnum α] (f : α → L.Formula β) :

L.Formula β

Computable finite infimum for formulas over an explicitly enumerated type.

Equations

FirstOrder.Language.Formula.iInf' f = FirstOrder.Language.BoundedFormula.iInf' f

Instances For

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.falsum {L : Language} {α : Type u_1} {β : Type u_2} (g : α ≃ β) {k : ℕ} :

(relabelEquiv g) BoundedFormula.falsum = BoundedFormula.falsum

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.imp {L : Language} {α : Type u_1} {β : Type u_2} (g : α ≃ β) {k : ℕ} (φ ψ : L.BoundedFormula α k) :

(relabelEquiv g) (φ.imp ψ) = ((relabelEquiv g) φ).imp ((relabelEquiv g) ψ)

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.not {L : Language} {α : Type u_1} {β : Type u_2} (g : α ≃ β) {k : ℕ} (φ : L.BoundedFormula α k) :

(relabelEquiv g) φ.not = ((relabelEquiv g) φ).not

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.nf {L : Language} {α : Type u_1} {β : Type u_2} (g : α ≃ β) {k : ℕ} (φ ψ : L.BoundedFormula α k) :

(relabelEquiv g) (φ ⊓ ψ) = (relabelEquiv g) φ ⊓ (relabelEquiv g) ψ

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.sup {L : Language} {α : Type u_1} {β : Type u_2} (g : α ≃ β) {k : ℕ} (φ ψ : L.BoundedFormula α k) :

(relabelEquiv g) (φ ⊔ ψ) = (relabelEquiv g) φ ⊔ (relabelEquiv g) ψ

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.rel {L : Language} {a : Type u_3} {b : Type u_4} {n : ℕ} (g : a ≃ b) {k : ℕ} {R : L.Relations k} {ts : Fin k → L.Term (a ⊕ Fin n)} :

(relabelEquiv g) (BoundedFormula.rel R ts) = BoundedFormula.rel R fun (i : Fin k) => Term.relabel (Sum.map (⇑g) id) (ts i)

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.eq {L : Language} {a : Type u_3} {b : Type u_4} {n : ℕ} (g : a ≃ b) {t1 t2 : L.Term (a ⊕ Fin n)} :

(relabelEquiv g) (t1.bdEqual t2) = (Term.relabel (Sum.map (⇑g) id) t1).bdEqual (Term.relabel (Sum.map (⇑g) id) t2)

source

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.bdEqual {L : Language} {a : Type u_3} {b : Type u_4} {n : ℕ} (g : a ≃ b) {t1 t2 : L.Term (a ⊕ Fin n)} :

(relabelEquiv g) (t1.bdEqual t2) = (Term.relabel (Sum.map (⇑g) id) t1).bdEqual (Term.relabel (Sum.map (⇑g) id) t2)

source

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.comp_inv {L : Language} {α : Type u_3} {β : Type u_4} {m : ℕ} {φ : L.BoundedFormula α m} (f : α ≃ β) :

(relabelEquiv f.symm) ((relabelEquiv f) φ) = φ

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabel.sup {L : Language} {α : Type u_3} {β : Type u_4} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} (φ ψ : L.BoundedFormula α k) :

relabel g (φ ⊔ ψ) = relabel g φ ⊔ relabel g ψ

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabel.inf {L : Language} {α : Type u_3} {β : Type u_4} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} (φ ψ : L.BoundedFormula α k) :

relabel g (φ ⊓ ψ) = relabel g φ ⊓ relabel g ψ

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.all {L : Language} {α : Type u_1} {β : Type u_2} (g : α ≃ β) {k : ℕ} (φ : L.BoundedFormula α (k + 1)) :

(relabelEquiv g) φ.all = ((relabelEquiv g) φ).all

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.ex {L : Language} {α : Type u_1} {β : Type u_2} (g : α ≃ β) {k : ℕ} (φ : L.BoundedFormula α (k + 1)) :

(relabelEquiv g) φ.ex = ((relabelEquiv g) φ).ex

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.alls {L : Language} {α : Type u_1} {β : Type u_2} (g : α ≃ β) {k : ℕ} (φ : L.BoundedFormula α k) :

(relabelEquiv g) φ.alls = ((relabelEquiv g) φ).alls

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.exs {L : Language} {α : Type u_1} {β : Type u_2} (g : α ≃ β) {k : ℕ} (φ : L.BoundedFormula α k) :

(relabelEquiv g) φ.exs = ((relabelEquiv g) φ).exs

source

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.relabelAux_sumCongr {α β : Type u} {γ : Type u_1} [enum : IsEnum β] (g : α ≃ γ) (k : ℕ) (x : (α ⊕ β) ⊕ Fin k) :

(g.sumCongr (_root_.Equiv.refl (Fin (IsEnum.size β + k)))) (relabelAux (fun (a : α ⊕ β) => Sum.map id IsEnum.toIdx a) k x) = relabelAux (fun (a : γ ⊕ β) => Sum.map id IsEnum.toIdx a) k (((g.sumCongr (_root_.Equiv.refl β)).sumCongr (_root_.Equiv.refl (Fin k))) x)

source

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.relabel_relabelSum {L : Language} {α β : Type u} {γ : Type u_1} [enum : IsEnum β] (g : α ≃ γ) {k : ℕ} (φ : L.BoundedFormula (α ⊕ β) k) :

(relabelEquiv g) (relabel (fun (a : α ⊕ β) => Sum.map id IsEnum.toIdx a) φ) = relabel (fun (a : γ ⊕ β) => Sum.map id IsEnum.toIdx a) ((relabelEquiv (g.sumCongr (_root_.Equiv.refl β))) φ)

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.iExs' {L : Language} {α β γ : Type u_1} [henum : IsEnum β] (g : α ≃ γ) (φ : L.Formula (α ⊕ β)) :

(relabelEquiv g) φ.iExs' = Formula.iExs' ((relabelEquiv (g.sumCongr (_root_.Equiv.refl β))) φ)

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.iAlls' {L : Language} {α β γ : Type u_1} [henum : IsEnum β] (g : α ≃ γ) (φ : L.Formula (α ⊕ β)) :

(relabelEquiv g) φ.iAlls' = Formula.iAlls' ((relabelEquiv (g.sumCongr (_root_.Equiv.refl β))) φ)

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.relabelEquiv.inf {L : Language} {α : Type u_3} {β : Type u_4} (g : α ≃ β) {k : ℕ} (φ ψ : L.BoundedFormula α k) :

(relabelEquiv g) (φ ⊓ ψ) = (relabelEquiv g) φ ⊓ (relabelEquiv g) ψ