Supporting results for pointwise provable equality.

structure PointwiseComposition.FFL.FirstOrder.Semiterm.Operator (L : Language) (n : ℕ) : Type u_1

Data and laws for Operator in FFL.FirstOrder.Semiterm.

• term : ClosedSemiterm L n

  The term construction in FFL.FirstOrder.Semiterm.Operator.

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiterm.Const (L : Language) : Type u

The Const construction in FFL.FirstOrder.Semiterm.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiterm.Const L = PointwiseComposition.FFL.FirstOrder.Semiterm.Operator L 0

def PointwiseComposition.FFL.FirstOrder.Semiterm.fn {L : Language} {k : ℕ} (f : L.Func k) : Operator L k

The fn construction in FFL.FirstOrder.Semiterm.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.equiv {L : Language} {n : ℕ} : Operator L n ≃ ClosedSemiterm L n

The equiv construction in FFL.FirstOrder.Semiterm.Operator.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.operator {L : Language} {ξ : Type u_2} {n arity : ℕ} (o : Operator L arity) (v : Fin arity → Semiterm L ξ n) : Semiterm L ξ n

The operator construction in FFL.FirstOrder.Semiterm.Operator.

Equations

• o.operator v = (PointwiseComposition.FFL.FirstOrder.Rew.subst v) (PointwiseComposition.FFL.FirstOrder.Rew.emb o.term)

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.const {L : Language} {ξ : Type u_2} {n : ℕ} (c : Const L) : Semiterm L ξ n

The const construction in FFL.FirstOrder.Semiterm.Operator.

Equations

• ↑c = PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.operator c ![]

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.instCoeConst {L : Language} {ξ : Type u_2} {n : ℕ} : Coe (Const L) (Semiterm L ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.instCoeConst = { coe := PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.const }

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.comp {L : Language} {k l : ℕ} (o : Operator L k) (w : Fin k → Operator L l) : Operator L l

The comp construction in FFL.FirstOrder.Semiterm.Operator.

Equations

• o.comp w = { term := o.operator fun (x : Fin k) => (w x).term }

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.operator_comp {L : Language} {k l : ℕ} {ξ : Type u_1} {n : ℕ} (o : Operator L k) (w : Fin k → Operator L l) (v : Fin l → Semiterm L ξ n) : (o.comp w).operator v = o.operator fun (x : Fin k) => (w x).operator v

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.bvar {L : Language} {n : ℕ} (x : Fin n) : Operator L n

The bvar construction in FFL.FirstOrder.Semiterm.Operator.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.bvar x = { term := PointwiseComposition.FFL.FirstOrder.Semiterm.bvar x }

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.operator_bvar {L : Language} {k : ℕ} {ξ : Type u_1} {n : ℕ} (x : Fin k) (v : Fin k → Semiterm L ξ n) : (bvar x).operator v = v x

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.bv_operator {L : Language} {ξ : Type u_1} {n k : ℕ} (o : Operator L k) (v : Fin k → Semiterm L ξ (n + 1)) : (o.operator v).bv = (bv o.term).biUnion fun (i : Fin k) => (v i).bv

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.positive_operator_iff {L : Language} {ξ : Type u_1} {n k : ℕ} {o : Operator L k} {v : Fin k → Semiterm L ξ (n + 1)} : (o.operator v).Positive ↔ ∀ i ∈ bv o.term, (v i).Positive

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.positive_const {L : Language} {ξ : Type u_1} {n : ℕ} (c : Const L) : (↑c).Positive

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.foldr {L : Language} {k : ℕ} (f : Operator L 2) (z : Operator L k) : List (Operator L k) → Operator L k

The foldr construction in FFL.FirstOrder.Semiterm.Operator.

Equations

• f.foldr z [] = z
• f.foldr z (o :: os) = f.comp ![f.foldr z os, o]

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.foldr_nil {L : Language} {k : ℕ} (f : Operator L 2) (z : Operator L k) : f.foldr z [] = z

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.operator_foldr_cons {L : Language} {k : ℕ} {ξ : Type u_1} {n : ℕ} (f : Operator L 2) (z o : Operator L k) (os : List (Operator L k)) (v : Fin k → Semiterm L ξ n) : (f.foldr z (o :: os)).operator v = f.operator ![(f.foldr z os).operator v, o.operator v]

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.iterr {L : Language} (f : Operator L 2) (z : Const L) (n : ℕ) : Operator L n

The iterr construction in FFL.FirstOrder.Semiterm.Operator.

Equations

• f.iterr z 0 = z
• f.iterr z n.succ = f.foldr (PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.bvar 0) (List.ofFn fun (x : Fin n) => PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.bvar x.succ)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.iterr_zero {L : Language} (f : Operator L 2) (z : Const L) : f.iterr z 0 = z

class PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.Zero (L : Language) : Type u_1

Data and laws for Zero in FFL.FirstOrder.Semiterm.Operator.

• zero : Const L

  The zero construction in FFL.FirstOrder.Semiterm.Operator.Zero.

class PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.One (L : Language) : Type u_1

Data and laws for One in FFL.FirstOrder.Semiterm.Operator.

• one : Const L

  The one construction in FFL.FirstOrder.Semiterm.Operator.One.

class PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.Add (L : Language) : Type u_1

Data and laws for Add in FFL.FirstOrder.Semiterm.Operator.

• add : Operator L 2

  The add construction in FFL.FirstOrder.Semiterm.Operator.Add.

class PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.Mul (L : Language) : Type u_1

Data and laws for Mul in FFL.FirstOrder.Semiterm.Operator.

• mul : Operator L 2

  The mul construction in FFL.FirstOrder.Semiterm.Operator.Mul.

class PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.Exp (L : Language) : Type u_1

Data and laws for Exp in FFL.FirstOrder.Semiterm.Operator.

• exp : Operator L 1

  The exp construction in FFL.FirstOrder.Semiterm.Operator.Exp.

class PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.Sub (L : Language) : Type u_1

Data and laws for Sub in FFL.FirstOrder.Semiterm.Operator.

• sub : Operator L 2

  The sub construction in FFL.FirstOrder.Semiterm.Operator.Sub.

class PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.Div (L : Language) : Type u_1

Data and laws for Div in FFL.FirstOrder.Semiterm.Operator.

• div : Operator L 2

  The div construction in FFL.FirstOrder.Semiterm.Operator.Div.

class PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.Star (L : Language) : Type u_1

Data and laws for Star in FFL.FirstOrder.Semiterm.Operator.

• star : Const L

  The star construction in FFL.FirstOrder.Semiterm.Operator.Star.

class PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.GödelNumber (L : Language) (α : Type u_1) : Type (max u_1 u_2)

Data and laws for Gödel Number in FFL.FirstOrder.Semiterm.Operator.

• gödelNumber : α → Const L

  The gödel Number construction in FFL.FirstOrder.Semiterm.Operator.GödelNumber.

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.«termOp(0)» : Lean.ParserDescr

The «term Op(0)» construction in FFL.FirstOrder.Semiterm.Operator.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.«termOp(0)[_]» : Lean.ParserDescr

The «term Op(0)[ ]» construction in FFL.FirstOrder.Semiterm.Operator.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.«termOp(1)» : Lean.ParserDescr

The «term Op(1)» construction in FFL.FirstOrder.Semiterm.Operator.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.«termOp(1)[_]» : Lean.ParserDescr

The «term Op(1)[ ]» construction in FFL.FirstOrder.Semiterm.Operator.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.«termOp(+)» : Lean.ParserDescr

The «term Op(+)» construction in FFL.FirstOrder.Semiterm.Operator.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.«termOp(+)[_]» : Lean.ParserDescr

The «term Op(+)[ ]» construction in FFL.FirstOrder.Semiterm.Operator.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.«termOp(*)» : Lean.ParserDescr

The «term Op(*)» construction in FFL.FirstOrder.Semiterm.Operator.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.«termOp(*)[_]» : Lean.ParserDescr

The «term Op(*)[ ]» construction in FFL.FirstOrder.Semiterm.Operator.

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.instZeroOfZero {L : Language} [L.Zero] : Operator.Zero L

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.instOneOfOne {L : Language} [L.One] : Operator.One L

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.instAddOfAdd {L : Language} [L.Add] : Operator.Add L

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.instMulOfMul {L : Language} [L.Mul] : Operator.Mul L

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.instExpOfExp {L : Language} [L.Exp] : Operator.Exp L

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.instStarOfStar {L : Language} [L.Star] : Operator.Star L

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.Zero.term_eq {L : Language} [L.Zero] : op(0).term = func Language.Zero.zero ![]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.One.term_eq {L : Language} [L.One] : op(1).term = func Language.One.one ![]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.Add.term_eq {L : Language} [L.Add] : op(+).term = func Language.Add.add Semiterm.bvar

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.Mul.term_eq {L : Language} [L.Mul] : op(*).term = func Language.Mul.mul Semiterm.bvar

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.Exp.term_eq {L : Language} [L.Exp] : exp.term = func Language.Exp.exp Semiterm.bvar

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.Star.term_eq {L : Language} [L.Star] : star.term = func Language.Star.star ![]

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.numeral (L : Language) [Operator.Zero L] [Operator.One L] [Operator.Add L] : ℕ → Const L

The numeral construction in FFL.FirstOrder.Semiterm.Operator.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.numeral L 0 = op(0)
• PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.numeral L n.succ = op(+).foldr op(1) (List.replicate n op(1))

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.numeral_zero {L : Language} [hz : Operator.Zero L] [ho : Operator.One L] [ha : Operator.Add L] : numeral L 0 = op(0)

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.numeral_one {L : Language} [hz : Operator.Zero L] [ho : Operator.One L] [ha : Operator.Add L] : numeral L 1 = op(1)

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.numeral_succ {L : Language} [hz : Operator.Zero L] [ho : Operator.One L] [ha : Operator.Add L] {z : ℕ} : z ≠ 0 → numeral L (z + 1) = op(+).comp ![numeral L z, op(1)]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.numeral_add_two {L : Language} [hz : Operator.Zero L] [ho : Operator.One L] [ha : Operator.Add L] {z : ℕ} : numeral L (z + 2) = op(+).comp ![numeral L (z + 1), op(1)]

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.encode (L : Language) [Operator.Zero L] [Operator.One L] [Operator.Add L] {α : Type u_1} [Encodable α] (a : α) : Const L

The encode construction in FFL.FirstOrder.Semiterm.Operator.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.encode L a = PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.numeral L (Encodable.encode a)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.Add.positive_iff {L : Language} {ξ : Type u_1} {n : ℕ} [L.Add] (t u : Semiterm L ξ (n + 1)) : (op(+).operator ![t, u]).Positive ↔ t.Positive ∧ u.Positive

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.Mul.positive_iff {L : Language} {ξ : Type u_1} {n : ℕ} [L.Mul] (t u : Semiterm L ξ (n + 1)) : (op(*).operator ![t, u]).Positive ↔ t.Positive ∧ u.Positive

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.Exp.positive_iff {L : Language} {ξ : Type u_1} {n : ℕ} [L.Exp] (t : Semiterm L ξ (n + 1)) : (exp.operator ![t]).Positive ↔ t.Positive

def PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.npow (L : Language) [Operator.One L] [Operator.Mul L] (n : ℕ) : Operator L 1

The npow construction in FFL.FirstOrder.Semiterm.Operator.

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.npow_zero {L : Language} [Operator.One L] [Operator.Mul L] : npow L 0 = comp op(1) ![]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.npow_succ {L : Language} [Operator.One L] [Operator.Mul L] {n : ℕ} : npow L (n + 1) = op(*).comp ![npow L n, bvar 0]

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.npow_positive_iff {L : Language} {ξ : Type u_1} {n : ℕ} [Operator.One L] [L.Mul] (t : Semiterm L ξ (n + 1)) (k : ℕ) : ((npow L k).operator ![t]).Positive ↔ k = 0 ∨ t.Positive

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.GödelNumber.gödelNumber' {L : Language} {α : Type u_2} [GödelNumber L α] {ξ : Type u_3} {n : ℕ} (a : α) : Semiterm L ξ n

The gödel Number' construction in FFL.FirstOrder.Semiterm.Operator.GödelNumber.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.GödelNumber.gödelNumber' a = ↑(PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.GödelNumber.gödelNumber a)

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.GödelNumber.instGödelQuote {L : Language} {α : Type u_2} [GödelNumber L α] {ξ : Type u_3} {n : ℕ} : GödelQuote α (Semiterm L ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.GödelNumber.instGödelQuote = { quote := PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.GödelNumber.gödelNumber' }

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.GödelNumber.ofEncodable {L : Language} [Operator.Zero L] [Operator.One L] [Operator.Add L] {α : Type u_1} [Encodable α] : GödelNumber L α

The of Encodable construction in FFL.FirstOrder.Semiterm.Operator.GödelNumber.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.GödelNumber.ofEncodable = { gödelNumber := PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.encode L }

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.complexity_zero {L : Language} {ξ : Type u_1} {n : ℕ} [L.Zero] : (↑op(0)).complexity = 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.complexity_one {L : Language} {ξ : Type u_1} {n : ℕ} [L.One] : (↑op(1)).complexity = 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.complexity_add {L : Language} {ξ : Type u_1} {n : ℕ} [L.Add] (t u : Semiterm L ξ n) : (op(+).operator ![t, u]).complexity = max t.complexity u.complexity + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.complexity_mul {L : Language} {ξ : Type u_1} {n : ℕ} [L.Mul] (t u : Semiterm L ξ n) : (op(*).operator ![t, u]).complexity = max t.complexity u.complexity + 1

structure PointwiseComposition.FFL.FirstOrder.Semiformula.Operator (L : Language) (n : ℕ) : Type u

Data and laws for Operator in FFL.FirstOrder.Semiformula.

• sentence : Semisentence L n

  The sentence construction in FFL.FirstOrder.Semiformula.Operator.

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiformula.Const (L : Language) : Type u

The Const construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.Const L = PointwiseComposition.FFL.FirstOrder.Semiformula.Operator L 0

def PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.operator {L : Language} {ξ : Type u_2} {n arity : ℕ} (o : Operator L arity) (v : Fin arity → Semiterm L ξ n) : Semiformula L ξ n

The operator construction in FFL.FirstOrder.Semiformula.Operator.

Equations

• o.operator v = PointwiseComposition.FFL.FirstOrder.Rewriting.emb o.sentence ↜ v

def PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.const {L : Language} {ξ : Type u_2} {n : ℕ} (c : Const L) : Semiformula L ξ n

The const construction in FFL.FirstOrder.Semiformula.Operator.

Equations

• ↑c = PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.operator c ![]

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.instCoeConst {L : Language} {ξ : Type u_2} {n : ℕ} : Coe (Const L) (Semiformula L ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.instCoeConst = { coe := PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.const }

def PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.comp {L : Language} {k l : ℕ} (o : Operator L k) (w : Fin k → Semiterm.Operator L l) : Operator L l

The comp construction in FFL.FirstOrder.Semiformula.Operator.

Equations

• o.comp w = { sentence := o.operator fun (x : Fin k) => (w x).term }

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.operator_comp {L : Language} {k l : ℕ} {ξ : Type u_1} {n : ℕ} (o : Operator L k) (w : Fin k → Semiterm.Operator L l) (v : Fin l → Semiterm L ξ n) : (o.comp w).operator v = o.operator fun (x : Fin k) => (w x).operator v

def PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.and {L : Language} {k : ℕ} (o₁ o₂ : Operator L k) : Operator L k

The and construction in FFL.FirstOrder.Semiformula.Operator.

Equations

• o₁.and o₂ = { sentence := o₁.sentence ⋏ o₂.sentence }

def PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.or {L : Language} {k : ℕ} (o₁ o₂ : Operator L k) : Operator L k

The or construction in FFL.FirstOrder.Semiformula.Operator.

Equations

• o₁.or o₂ = { sentence := o₁.sentence ⋎ o₂.sentence }

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.operator_and {L : Language} {k : ℕ} {ξ : Type u_1} {n : ℕ} (o₁ o₂ : Operator L k) (v : Fin k → Semiterm L ξ n) : (o₁.and o₂).operator v = o₁.operator v ⋏ o₂.operator v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.operator_or {L : Language} {k : ℕ} {ξ : Type u_1} {n : ℕ} (o₁ o₂ : Operator L k) (v : Fin k → Semiterm L ξ n) : (o₁.or o₂).operator v = o₁.operator v ⋎ o₂.operator v

class PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.Eq (L : Language) : Type u_1

Data and laws for Eq in FFL.FirstOrder.Semiformula.Operator.

• eq : Operator L 2

  The eq construction in FFL.FirstOrder.Semiformula.Operator.Eq.

class PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.LT (L : Language) : Type u_1

Data and laws for LT in FFL.FirstOrder.Semiformula.Operator.

• lt : Operator L 2

  The lt construction in FFL.FirstOrder.Semiformula.Operator.LT.

class PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.LE (L : Language) : Type u_1

Data and laws for LE in FFL.FirstOrder.Semiformula.Operator.

• le : Operator L 2

  The le construction in FFL.FirstOrder.Semiformula.Operator.LE.

class PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.Mem (L : Language) : Type u_1

Data and laws for Mem in FFL.FirstOrder.Semiformula.Operator.

• mem : Operator L 2

  The mem construction in FFL.FirstOrder.Semiformula.Operator.Mem.

def PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.«termOp(=)» : Lean.ParserDescr

The «term Op(=)» construction in FFL.FirstOrder.Semiformula.Operator.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.«termOp(=)[_]» : Lean.ParserDescr

The «term Op(=)[ ]» construction in FFL.FirstOrder.Semiformula.Operator.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.«termOp(<)» : Lean.ParserDescr

The «term Op(<)» construction in FFL.FirstOrder.Semiformula.Operator.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.«termOp(<)[_]» : Lean.ParserDescr

The «term Op(<)[ ]» construction in FFL.FirstOrder.Semiformula.Operator.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.«termOp(≤)» : Lean.ParserDescr

The «term Op(≤)» construction in FFL.FirstOrder.Semiformula.Operator.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.«termOp(≤)[_]» : Lean.ParserDescr

The «term Op(≤)[ ]» construction in FFL.FirstOrder.Semiformula.Operator.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.«termOp(∈)» : Lean.ParserDescr

The «term Op(∈)» construction in FFL.FirstOrder.Semiformula.Operator.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.«termOp(∈)[_]» : Lean.ParserDescr

The «term Op(∈)[ ]» construction in FFL.FirstOrder.Semiformula.Operator.

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.instEqOfEq {L : Language} [L.Eq] : Operator.Eq L

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.instLTOfLT {L : Language} [L.LT] : Operator.LT L

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.instMemOfMem {L : Language} [L.Mem] : Operator.Mem L

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.instLEOfEqOfLT {L : Language} [Operator.Eq L] [Operator.LT L] : Operator.LE L

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.instLEOfEqOfLT = { le := op(=).or op(<) }

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.Eq.sentence_eq {L : Language} [L.Eq] : op(=).sentence = rel Language.Eq.eq Semiterm.bvar

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.LT.sentence_eq {L : Language} [L.LT] : op(<).sentence = rel Language.LT.lt Semiterm.bvar

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.Mem.sentence_eq {L : Language} [L.Mem] : op(∈).sentence = rel Language.Mem.mem Semiterm.bvar

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.LE.sentence_eq {L : Language} [L.Eq] [L.LT] : op(≤).sentence = op(=).sentence ⋎ op(<).sentence

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.LE.def_of_Eq_of_LT {L : Language} [Operator.Eq L] [Operator.LT L] : op(≤) = op(=).or op(<)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.Eq.equal_inj {L : Language} {ξ₂ : Type u_1} {n₂ : ℕ} [L.Eq] {t₁ t₂ u₁ u₂ : Semiterm L ξ₂ n₂} : op(=).operator ![t₁, u₁] = op(=).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.LT.lt_inj {L : Language} {ξ₂ : Type u_1} {n₂ : ℕ} [L.LT] {t₁ t₂ u₁ u₂ : Semiterm L ξ₂ n₂} : op(<).operator ![t₁, u₁] = op(<).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.Mem.mem_inj {L : Language} {ξ₂ : Type u_1} {n₂ : ℕ} [L.Mem] {t₁ t₂ u₁ u₂ : Semiterm L ξ₂ n₂} : op(∈).operator ![t₁, u₁] = op(∈).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.LE.le_inj {L : Language} {ξ₂ : Type u_1} {n₂ : ℕ} [L.Eq] [L.LT] {t₁ t₂ u₁ u₂ : Semiterm L ξ₂ n₂} : op(≤).operator ![t₁, u₁] = op(≤).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.lt_def {L : Language} {ξ : Type u_1} {n : ℕ} [L.LT] (t u : Semiterm L ξ n) : op(<).operator ![t, u] = rel Language.LT.lt ![t, u]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.eq_def {L : Language} {ξ : Type u_1} {n : ℕ} [L.Eq] (t u : Semiterm L ξ n) : op(=).operator ![t, u] = rel Language.Eq.eq ![t, u]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.mem_def {L : Language} {ξ : Type u_1} {n : ℕ} [L.Mem] (t u : Semiterm L ξ n) : op(∈).operator ![t, u] = rel Language.Mem.mem ![t, u]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.le_def {L : Language} {ξ : Type u_1} {n : ℕ} [L.Eq] [L.LT] (t u : Semiterm L ξ n) : op(≤).operator ![t, u] = rel Language.Eq.eq ![t, u] ⋎ rel Language.LT.lt ![t, u]

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.Eq.open {L : Language} {ξ : Type u_1} {n : ℕ} [L.Eq] (t u : Semiterm L ξ n) : (op(=).operator ![t, u]).Open

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.LT.open {L : Language} {ξ : Type u_1} {n : ℕ} [L.LT] (t u : Semiterm L ξ n) : (op(<).operator ![t, u]).Open

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.Mem.open {L : Language} {ξ : Type u_1} {n : ℕ} [L.Mem] (t u : Semiterm L ξ n) : (op(∈).operator ![t, u]).Open

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.Operator.LE.open {L : Language} {ξ : Type u_1} {n : ℕ} [L.Eq] [L.LT] (t u : Semiterm L ξ n) : (op(≤).operator ![t, u]).Open

def PointwiseComposition.FFL.FirstOrder.Semiformula.ballLT {L : Language} {ξ : Type u_2} {n : ℕ} [Operator.LT L] (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)) : Semiformula L ξ n

The ball LT construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.ballLT t φ = ∀¹[op(<).operator ![PointwiseComposition.FFL.FirstOrder.Semiterm.bvar 0, PointwiseComposition.FFL.FirstOrder.Rew.bShift t]] φ

def PointwiseComposition.FFL.FirstOrder.Semiformula.bexsLT {L : Language} {ξ : Type u_2} {n : ℕ} [Operator.LT L] (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)) : Semiformula L ξ n

The bexs LT construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.bexsLT t φ = ∃¹[op(<).operator ![PointwiseComposition.FFL.FirstOrder.Semiterm.bvar 0, PointwiseComposition.FFL.FirstOrder.Rew.bShift t]] φ

def PointwiseComposition.FFL.FirstOrder.Semiformula.ballLE {L : Language} {ξ : Type u_2} {n : ℕ} [Operator.LE L] (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)) : Semiformula L ξ n

The ball LE construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.ballLE t φ = ∀¹[op(≤).operator ![PointwiseComposition.FFL.FirstOrder.Semiterm.bvar 0, PointwiseComposition.FFL.FirstOrder.Rew.bShift t]] φ

def PointwiseComposition.FFL.FirstOrder.Semiformula.bexsLE {L : Language} {ξ : Type u_2} {n : ℕ} [Operator.LE L] (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)) : Semiformula L ξ n

The bexs LE construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.bexsLE t φ = ∃¹[op(≤).operator ![PointwiseComposition.FFL.FirstOrder.Semiterm.bvar 0, PointwiseComposition.FFL.FirstOrder.Rew.bShift t]] φ

def PointwiseComposition.FFL.FirstOrder.Semiformula.ballMem {L : Language} {ξ : Type u_2} {n : ℕ} [Operator.Mem L] (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)) : Semiformula L ξ n

The ball Mem construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.ballMem t φ = ∀¹[op(∈).operator ![PointwiseComposition.FFL.FirstOrder.Semiterm.bvar 0, PointwiseComposition.FFL.FirstOrder.Rew.bShift t]] φ

def PointwiseComposition.FFL.FirstOrder.Semiformula.bexsMem {L : Language} {ξ : Type u_2} {n : ℕ} [Operator.Mem L] (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)) : Semiformula L ξ n

The bexs Mem construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.bexsMem t φ = ∃¹[op(∈).operator ![PointwiseComposition.FFL.FirstOrder.Semiterm.bvar 0, PointwiseComposition.FFL.FirstOrder.Rew.bShift t]] φ

theorem PointwiseComposition.FFL.FirstOrder.Rew.operator {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (o : Semiterm.Operator L k) (v : Fin k → Semiterm L ξ₁ n₁) : ω (o.operator v) = o.operator fun (i : Fin k) => ω (v i)

theorem PointwiseComposition.FFL.FirstOrder.Rew.operator' {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (o : Semiterm.Operator L k) (v : Fin k → Semiterm L ξ₁ n₁) : ω (o.operator v) = o.operator (⇑ω ∘ v)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Rew.finitary0 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiterm.Operator L 0) (v : Fin 0 → Semiterm L ξ₁ n₁) : ω (o.operator v) = o.operator ![]

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Rew.finitary1 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiterm.Operator L 1) (t : Semiterm L ξ₁ n₁) : ω (o.operator ![t]) = o.operator ![ω t]

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Rew.finitary2 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiterm.Operator L 2) (t₁ t₂ : Semiterm L ξ₁ n₁) : ω (o.operator ![t₁, t₂]) = o.operator ![ω t₁, ω t₂]

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Rew.finitary3 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiterm.Operator L 3) (t₁ t₂ t₃ : Semiterm L ξ₁ n₁) : ω (o.operator ![t₁, t₂, t₃]) = o.operator ![ω t₁, ω t₂, ω t₃]

theorem PointwiseComposition.FFL.FirstOrder.Rew.const {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_1} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (c : Semiterm.Const L) : ω ↑c = ↑c

theorem PointwiseComposition.FFL.FirstOrder.Rew.hom_operator {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (o : Semiformula.Operator L k) (v : Fin k → Semiterm L ξ₁ n₁) : (Rewriting.app ω) (o.operator v) = o.operator fun (i : Fin k) => ω (v i)

theorem PointwiseComposition.FFL.FirstOrder.Rew.hom_operator' {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (o : Semiformula.Operator L k) (v : Fin k → Semiterm L ξ₁ n₁) : (Rewriting.app ω) (o.operator v) = o.operator (⇑ω ∘ v)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Rew.hom_finitary0 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiformula.Operator L 0) (v : Fin 0 → Semiterm L ξ₁ n₁) : (Rewriting.app ω) (o.operator v) = o.operator ![]

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Rew.hom_finitary1 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiformula.Operator L 1) (t : Semiterm L ξ₁ n₁) : (Rewriting.app ω) (o.operator ![t]) = o.operator ![ω t]

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Rew.hom_finitary2 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiformula.Operator L 2) (t₁ t₂ : Semiterm L ξ₁ n₁) : (Rewriting.app ω) (o.operator ![t₁, t₂]) = o.operator ![ω t₁, ω t₂]

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Rew.hom_finitary3 {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (o : Semiformula.Operator L 3) (t₁ t₂ t₃ : Semiterm L ξ₁ n₁) : (Rewriting.app ω) (o.operator ![t₁, t₂, t₃]) = o.operator ![ω t₁, ω t₂, ω t₃]

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Rew.hom_const {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_1} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {c : Semiformula.Const L} : (Rewriting.app ω) ↑c = ↑c

theorem PointwiseComposition.FFL.FirstOrder.Rew.eq_equal_iff {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) [L.Eq] {φ : Semiformula L ξ₁ n₁} {t u : Semiterm L ξ₂ n₂} : (Rewriting.app ω) φ = op(=).operator ![t, u] ↔ ∃ (t' : Semiterm L ξ₁ n₁) (u' : Semiterm L ξ₁ n₁), ω t' = t ∧ ω u' = u ∧ φ = op(=).operator ![t', u']

theorem PointwiseComposition.FFL.FirstOrder.Rew.eq_lt_iff {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) [L.LT] {φ : Semiformula L ξ₁ n₁} {t u : Semiterm L ξ₂ n₂} : (Rewriting.app ω) φ = op(<).operator ![t, u] ↔ ∃ (t' : Semiterm L ξ₁ n₁) (u' : Semiterm L ξ₁ n₁), ω t' = t ∧ ω u' = u ∧ φ = op(<).operator ![t', u']

theorem PointwiseComposition.FFL.FirstOrder.Rew.eq_mem_iff {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {L : Language} (ω : Rew L ξ₁ n₁ ξ₂ n₂) [L.Mem] {φ : Semiformula L ξ₁ n₁} {t u : Semiterm L ξ₂ n₂} : (Rewriting.app ω) φ = op(∈).operator ![t, u] ↔ ∃ (t' : Semiterm L ξ₁ n₁) (u' : Semiterm L ξ₁ n₁), ω t' = t ∧ ω u' = u ∧ φ = op(∈).operator ![t', u']

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiterm.numeral {L : Language} [L.Zero] [L.One] [L.Add] {ξ : Type u_2} {n : ℕ} (k : ℕ) : Semiterm L ξ n

The numeral construction in FFL.FirstOrder.Semiterm.

Equations

• ↑k = ↑(PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.numeral L k)

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiterm.instCoeNat {L : Language} [L.Zero] [L.One] [L.Add] {ξ : Type u_2} {n : ℕ} : Coe ℕ (Semiterm L ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Semiterm.instCoeNat = { coe := PointwiseComposition.FFL.FirstOrder.Semiterm.numeral }