Documentation

LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Formula.Functions

Functions #

source
def LO.Arith.Negation.blueprint (pL : FirstOrder.Arith.LDef) :
Language.UformulaRec1.Blueprint pL

Imported declaration from the Incompleteness formalization.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def LO.Arith.Negation.construction {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} :
    Language.UformulaRec1.Construction V L (blueprint pL)

    Imported declaration from the Incompleteness formalization.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def LO.Arith.Language.neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : V) :
      V

      Imported declaration from the Incompleteness formalization.

      Equations
      Instances For
        source
        def LO.FirstOrder.Arith.LDef.negDef (pL : LDef) :
        Sg1.Semisentence 2

        Imported declaration from the Incompleteness formalization.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem LO.Arith.Language.neg_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
          FirstOrder.Arith.Sg1-Function₁ L.neg via pL.negDef
          source
          instance LO.Arith.Language.neg_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
          FirstOrder.Arith.Sg1-Function₁ L.neg
          source
          instance LO.Arith.Language.neg_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {m : ℕ} (Γ : SigmaPiDelta) :
          { Γ := Γ, rank := m + 1 }-Function₁ L.neg
          source
          @[simp]
          theorem LO.Arith.neg_rel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
          L.neg (qqRel k R v) = qqNRel k R v
          source
          @[simp]
          theorem LO.Arith.neg_nrel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
          L.neg (qqNRel k R v) = qqRel k R v
          source
          @[simp]
          theorem LO.Arith.neg_verum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
          L.neg qqVerum = qqFalsum
          source
          @[simp]
          theorem LO.Arith.neg_falsum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
          L.neg qqFalsum = qqVerum
          source
          @[simp]
          theorem LO.Arith.neg_and {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
          L.neg (qqAnd p q) = qqOr (L.neg p) (L.neg q)
          source
          @[simp]
          theorem LO.Arith.neg_or {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
          L.neg (qqOr p q) = qqAnd (L.neg p) (L.neg q)
          source
          @[simp]
          theorem LO.Arith.neg_all {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :
          L.neg (qqAll p) = qqEx (L.neg p)
          source
          @[simp]
          theorem LO.Arith.neg_ex {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :
          L.neg (qqEx p) = qqAll (L.neg p)
          source
          theorem LO.Arith.neg_not_uformula {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {x : V} (h : ¬L.IsUFormula x) :
          L.neg x = 0
          source
          theorem LO.Arith.Language.IsUFormula.neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
          L.IsUFormula p → L.IsUFormula (L.neg p)
          source
          @[simp]
          theorem LO.Arith.Language.IsUFormula.bv_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
          L.IsUFormula p → L.bv (L.neg p) = L.bv p
          source
          @[simp]
          theorem LO.Arith.Language.IsUFormula.neg_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
          L.IsUFormula p → L.neg (L.neg p) = p
          source
          @[simp]
          theorem LO.Arith.Language.IsUFormula.neg_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
          L.IsUFormula (L.neg p) ↔ L.IsUFormula p
          source
          @[simp]
          theorem LO.Arith.Language.IsSemiformula.neg_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} :
          L.IsSemiformula n (L.neg p) ↔ L.IsSemiformula n p
          source
          theorem LO.Arith.Language.IsSemiformula.neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} :
          L.IsSemiformula n p → L.IsSemiformula n (L.neg p)

          Alias of the reverse direction of LO.Arith.Language.IsSemiformula.neg_iff.

          source
          theorem LO.Arith.Language.IsSemiformula.elim_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} :
          L.IsSemiformula n (L.neg p) → L.IsSemiformula n p

          Alias of the forward direction of LO.Arith.Language.IsSemiformula.neg_iff.

          source
          @[simp]
          theorem LO.Arith.neg_inj_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
          L.neg p = L.neg q ↔ p = q
          source
          noncomputable def LO.Arith.Language.imp {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p q : V) :
          V

          Imported declaration from the Incompleteness formalization.

          Equations
          Instances For
            source
            def LO.Arith.«term_^→[_]_» :
            Lean.TrailingParserDescr

            Imported declaration from the Incompleteness formalization.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def LO.Arith.Language.iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p q : V) :
              V

              Imported declaration from the Incompleteness formalization.

              Equations
              Instances For
                source
                @[simp]
                theorem LO.Arith.Language.IsUFormula.imp {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} :
                L.IsUFormula (p ^→[L] q) ↔ L.IsUFormula p ∧ L.IsUFormula q
                source
                @[simp]
                theorem LO.Arith.Language.IsSemiformula.imp {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p q : V} :
                L.IsSemiformula n (p ^→[L] q) ↔ L.IsSemiformula n p ∧ L.IsSemiformula n q
                source
                def LO.FirstOrder.Arith.LDef.impDef (pL : LDef) :
                Sg1.Semisentence 3

                Imported declaration from the Incompleteness formalization.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem LO.Arith.Language.imp_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                  FirstOrder.Arith.Sg1-Function₂ L.imp via pL.impDef
                  source
                  instance LO.Arith.Language.imp_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                  FirstOrder.Arith.Sg1-Function₂ L.imp
                  source
                  instance LO.Arith.Language.imp_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : ℕ} :
                  { Γ := Γ, rank := m + 1 }-Function₂ L.imp
                  source
                  @[simp]
                  theorem LO.Arith.Language.IsUFormula.iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} :
                  L.IsUFormula (L.iff p q) ↔ L.IsUFormula p ∧ L.IsUFormula q
                  source
                  @[simp]
                  theorem LO.Arith.Language.IsSemiformula.iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p q : V} :
                  L.IsSemiformula n (L.iff p q) ↔ L.IsSemiformula n p ∧ L.IsSemiformula n q
                  source
                  @[simp]
                  theorem LO.Arith.lt_iff_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p q : V) :
                  p < L.iff p q
                  source
                  @[simp]
                  theorem LO.Arith.lt_iff_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p q : V) :
                  q < L.iff p q
                  source
                  def LO.FirstOrder.Arith.LDef.qqIffDef (pL : LDef) :
                  Sg1.Semisentence 3

                  Imported declaration from the Incompleteness formalization.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem LO.Arith.Language.iff_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                    FirstOrder.Arith.Sg1-Function₂ L.iff via pL.qqIffDef
                    source
                    instance LO.Arith.Language.iff_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                    FirstOrder.Arith.Sg1-Function₂ L.iff
                    source
                    instance LO.Arith.Language.iff_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : ℕ} :
                    { Γ := Γ, rank := m + 1 }-Function₂ L.iff
                    source
                    def LO.Arith.Shift.blueprint (pL : FirstOrder.Arith.LDef) :
                    Language.UformulaRec1.Blueprint pL

                    Imported declaration from the Incompleteness formalization.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      noncomputable def LO.Arith.Shift.construction {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                      Language.UformulaRec1.Construction V L (blueprint pL)

                      Imported declaration from the Incompleteness formalization.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        noncomputable def LO.Arith.Language.shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : V) :
                        V

                        Imported declaration from the Incompleteness formalization.

                        Equations
                        Instances For
                          source
                          def LO.FirstOrder.Arith.LDef.shiftDef (pL : LDef) :
                          Sg1.Semisentence 2

                          Imported declaration from the Incompleteness formalization.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            theorem LO.Arith.Language.shift_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                            FirstOrder.Arith.Sg1-Function₁ L.shift via pL.shiftDef
                            source
                            instance LO.Arith.Language.shift_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                            FirstOrder.Arith.Sg1-Function₁ L.shift
                            source
                            instance LO.Arith.language.shift_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : ℕ} :
                            { Γ := Γ, rank := m + 1 }-Function₁ L.shift
                            source
                            @[simp]
                            theorem LO.Arith.shift_rel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                            L.shift (qqRel k R v) = qqRel k R (L.termShiftVec k v)
                            source
                            @[simp]
                            theorem LO.Arith.shift_nrel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                            L.shift (qqNRel k R v) = qqNRel k R (L.termShiftVec k v)
                            source
                            @[simp]
                            theorem LO.Arith.shift_verum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                            L.shift qqVerum = qqVerum
                            source
                            @[simp]
                            theorem LO.Arith.shift_falsum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                            L.shift qqFalsum = qqFalsum
                            source
                            @[simp]
                            theorem LO.Arith.shift_and {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                            L.shift (qqAnd p q) = qqAnd (L.shift p) (L.shift q)
                            source
                            @[simp]
                            theorem LO.Arith.shift_or {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                            L.shift (qqOr p q) = qqOr (L.shift p) (L.shift q)
                            source
                            @[simp]
                            theorem LO.Arith.shift_all {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :
                            L.shift (qqAll p) = qqAll (L.shift p)
                            source
                            @[simp]
                            theorem LO.Arith.shift_ex {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :
                            L.shift (qqEx p) = qqEx (L.shift p)
                            source
                            theorem LO.Arith.shift_not_uformula {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {x : V} (h : ¬L.IsUFormula x) :
                            L.shift x = 0
                            source
                            theorem LO.Arith.Language.IsUFormula.shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
                            L.IsUFormula p → L.IsUFormula (L.shift p)
                            source
                            theorem LO.Arith.Language.IsUFormula.bv_shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
                            L.IsUFormula p → L.bv (L.shift p) = L.bv p
                            source
                            theorem LO.Arith.Language.IsSemiformula.shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} :
                            L.IsSemiformula n p → L.IsSemiformula n (L.shift p)
                            source
                            @[simp]
                            theorem LO.Arith.Language.IsSemiformula.shift_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} :
                            L.IsSemiformula n (L.shift p) ↔ L.IsSemiformula n p
                            source
                            theorem LO.Arith.shift_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} (hp : L.IsSemiformula n p) :
                            L.shift (L.neg p) = L.neg (L.shift p)
                            source
                            def LO.FirstOrder.Arith.LDef.qVecDef (pL : LDef) :
                            Sg1.Semisentence 2

                            Imported declaration from the Incompleteness formalization.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              theorem LO.Arith.Language.qVec_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                              FirstOrder.Arith.Sg1-Function₁ L.qVec via pL.qVecDef
                              source
                              instance LO.Arith.Language.qVec_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                              FirstOrder.Arith.Sg1-Function₁ L.qVec
                              source
                              instance LO.Arith.Language.qVec_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : ℕ} :
                              { Γ := Γ, rank := m + 1 }-Function₁ L.qVec
                              source
                              def LO.Arith.Substs.blueprint (pL : FirstOrder.Arith.LDef) :
                              Language.UformulaRec1.Blueprint pL

                              Imported declaration from the Incompleteness formalization.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                noncomputable def LO.Arith.Substs.construction {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                                Language.UformulaRec1.Construction V L (blueprint pL)

                                Imported declaration from the Incompleteness formalization.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  noncomputable def LO.Arith.Language.substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (w p : V) :
                                  V

                                  Imported declaration from the Incompleteness formalization.

                                  Equations
                                  Instances For
                                    source
                                    def LO.FirstOrder.Arith.LDef.substsDef (pL : LDef) :
                                    Sg1.Semisentence 3

                                    Imported declaration from the Incompleteness formalization.

                                    Equations
                                    Instances For
                                      source
                                      theorem LO.Arith.Language.substs_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                                      FirstOrder.Arith.Sg1-Function₂ L.substs via pL.substsDef
                                      source
                                      instance LO.Arith.Language.substs_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                                      FirstOrder.Arith.Sg1-Function₂ L.substs
                                      source
                                      instance LO.Arith.Language.substs_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : ℕ} :
                                      { Γ := Γ, rank := m + 1 }-Function₂ L.substs
                                      source
                                      @[simp]
                                      theorem LO.Arith.substs_rel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                                      L.substs w (qqRel k R v) = qqRel k R (L.termSubstVec k w v)
                                      source
                                      @[simp]
                                      theorem LO.Arith.substs_nrel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                                      L.substs w (qqNRel k R v) = qqNRel k R (L.termSubstVec k w v)
                                      source
                                      @[simp]
                                      theorem LO.Arith.substs_verum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (w : V) :
                                      L.substs w qqVerum = qqVerum
                                      source
                                      @[simp]
                                      theorem LO.Arith.substs_falsum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (w : V) :
                                      L.substs w qqFalsum = qqFalsum
                                      source
                                      @[simp]
                                      theorem LO.Arith.substs_and {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                                      L.substs w (qqAnd p q) = qqAnd (L.substs w p) (L.substs w q)
                                      source
                                      @[simp]
                                      theorem LO.Arith.substs_or {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                                      L.substs w (qqOr p q) = qqOr (L.substs w p) (L.substs w q)
                                      source
                                      @[simp]
                                      theorem LO.Arith.substs_all {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w p : V} (hp : L.IsUFormula p) :
                                      L.substs w (qqAll p) = qqAll (L.substs (L.qVec w) p)
                                      source
                                      @[simp]
                                      theorem LO.Arith.substs_ex {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w p : V} (hp : L.IsUFormula p) :
                                      L.substs w (qqEx p) = qqEx (L.substs (L.qVec w) p)
                                      source
                                      theorem LO.Arith.isUFormula_subst_induction_sigma1 {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {P : V → V → V → Prop} (hP : FirstOrder.Arith.Sg1-Relation₃ P) (hRel : ∀ (w k R v : V), L.Rel k R → L.IsUTermVec k v → P w (qqRel k R v) (qqRel k R (L.termSubstVec k w v))) (hNRel : ∀ (w k R v : V), L.Rel k R → L.IsUTermVec k v → P w (qqNRel k R v) (qqNRel k R (L.termSubstVec k w v))) (hverum : ∀ (w : V), P w qqVerum qqVerum) (hfalsum : ∀ (w : V), P w qqFalsum qqFalsum) (hand : ∀ (w p q : V), L.IsUFormula p → L.IsUFormula q → P w p (L.substs w p) → P w q (L.substs w q) → P w (qqAnd p q) (qqAnd (L.substs w p) (L.substs w q))) (hor : ∀ (w p q : V), L.IsUFormula p → L.IsUFormula q → P w p (L.substs w p) → P w q (L.substs w q) → P w (qqOr p q) (qqOr (L.substs w p) (L.substs w q))) (hall : ∀ (w p : V), L.IsUFormula p → P (L.qVec w) p (L.substs (L.qVec w) p) → P w (qqAll p) (qqAll (L.substs (L.qVec w) p))) (hex : ∀ (w p : V), L.IsUFormula p → P (L.qVec w) p (L.substs (L.qVec w) p) → P w (qqEx p) (qqEx (L.substs (L.qVec w) p))) {w p : V} :
                                      L.IsUFormula p → P w p (L.substs w p)
                                      source
                                      theorem LO.Arith.semiformula_subst_induction {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {P : V → V → V → V → Prop} (hP : FirstOrder.Arith.Sg1-Relation₄ P) (hRel : ∀ (n w k R v : V), L.Rel k R → L.IsSemitermVec k n v → P n w (qqRel k R v) (qqRel k R (L.termSubstVec k w v))) (hNRel : ∀ (n w k R v : V), L.Rel k R → L.IsSemitermVec k n v → P n w (qqNRel k R v) (qqNRel k R (L.termSubstVec k w v))) (hverum : ∀ (n w : V), P n w qqVerum qqVerum) (hfalsum : ∀ (n w : V), P n w qqFalsum qqFalsum) (hand : ∀ (n w p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n w p (L.substs w p) → P n w q (L.substs w q) → P n w (qqAnd p q) (qqAnd (L.substs w p) (L.substs w q))) (hor : ∀ (n w p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n w p (L.substs w p) → P n w q (L.substs w q) → P n w (qqOr p q) (qqOr (L.substs w p) (L.substs w q))) (hall : ∀ (n w p : V), L.IsSemiformula (n + 1) p → P (n + 1) (L.qVec w) p (L.substs (L.qVec w) p) → P n w (qqAll p) (qqAll (L.substs (L.qVec w) p))) (hex : ∀ (n w p : V), L.IsSemiformula (n + 1) p → P (n + 1) (L.qVec w) p (L.substs (L.qVec w) p) → P n w (qqEx p) (qqEx (L.substs (L.qVec w) p))) {n p w : V} :
                                      L.IsSemiformula n p → P n w p (L.substs w p)
                                      source
                                      theorem LO.Arith.Language.IsSemiformula.substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p m w : V} :
                                      L.IsSemiformula n p → L.IsSemitermVec n m w → L.IsSemiformula m (L.substs w p)
                                      source
                                      theorem LO.Arith.substs_not_uformula {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w x : V} (h : ¬L.IsUFormula x) :
                                      L.substs w x = 0
                                      source
                                      theorem LO.Arith.substs_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {m w n p : V} (hp : L.IsSemiformula n p) :
                                      L.IsSemitermVec n m w → L.substs w (L.neg p) = L.neg (L.substs w p)
                                      source
                                      theorem LO.Arith.shift_substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {m w n p : V} (hp : L.IsSemiformula n p) :
                                      L.IsSemitermVec n m w → L.shift (L.substs w p) = L.substs (L.termShiftVec n w) (L.shift p)
                                      source
                                      theorem LO.Arith.substs_substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {m w l n v p : V} (hp : L.IsSemiformula l p) :
                                      L.IsSemitermVec n m w → L.IsSemitermVec l n v → L.substs w (L.substs v p) = L.substs (L.termSubstVec l w v) p
                                      source
                                      theorem LO.Arith.subst_eq_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p n w : V} (hp : L.IsSemiformula n p) (hw : L.IsSemitermVec n n w) (H : ∀ i < n, nth w i = qqBvar i) :
                                      L.substs w p = p
                                      source
                                      theorem LO.Arith.subst_eq_self₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsSemiformula 1 p) :
                                      L.substs ?[qqBvar 0] p = p
                                      source
                                      noncomputable def LO.Arith.Language.substs₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (t u : V) :
                                      V

                                      Imported declaration from the Incompleteness formalization.

                                      Equations
                                      Instances For
                                        source
                                        def LO.FirstOrder.Arith.LDef.substs₁Def (pL : LDef) :
                                        Sg1.Semisentence 3

                                        Imported declaration from the Incompleteness formalization.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          source
                                          theorem LO.Arith.Language.substs₁_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                                          FirstOrder.Arith.Sg1-Function₂ L.substs₁ via pL.substs₁Def
                                          source
                                          instance LO.Arith.Language.substs₁_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                                          FirstOrder.Arith.Sg1-Function₂ L.substs₁
                                          source
                                          instance LO.Arith.instBoldfaceFunction₂MkHAddNatOfNatSubsts₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : ℕ} :
                                          { Γ := Γ, rank := m + 1 }-Function₂ L.substs₁
                                          source
                                          theorem LO.Arith.Language.IsSemiformula.substs₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n t p : V} (ht : L.IsSemiterm n t) (hp : L.IsSemiformula 1 p) :
                                          L.IsSemiformula n (L.substs₁ t p)
                                          source
                                          noncomputable def LO.Arith.Language.free {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : V) :
                                          V

                                          Imported declaration from the Incompleteness formalization.

                                          Equations
                                          Instances For
                                            source
                                            def LO.FirstOrder.Arith.LDef.freeDef (pL : LDef) :
                                            Sg1.Semisentence 2

                                            Imported declaration from the Incompleteness formalization.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              source
                                              theorem LO.Arith.Language.free_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                                              FirstOrder.Arith.Sg1-Function₁ L.free via pL.freeDef
                                              source
                                              instance LO.Arith.Language.free_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                                              FirstOrder.Arith.Sg1-Function₁ L.free
                                              source
                                              instance LO.Arith.Language.free_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : ℕ} :
                                              { Γ := Γ, rank := m + 1 }-Function₁ L.free
                                              source
                                              @[simp]
                                              theorem LO.Arith.Language.IsSemiformula.free {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsSemiformula 1 p) :
                                              L.IsFormula (L.free p)
                                              source
                                              noncomputable def LO.Arith.Formalized.qqEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (x y : V) :
                                              V

                                              Imported declaration from the Incompleteness formalization.

                                              Equations
                                              Instances For
                                                source
                                                noncomputable def LO.Arith.Formalized.qqNEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (x y : V) :
                                                V

                                                Imported declaration from the Incompleteness formalization.

                                                Equations
                                                Instances For
                                                  source
                                                  noncomputable def LO.Arith.Formalized.qqLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (x y : V) :
                                                  V

                                                  Imported declaration from the Incompleteness formalization.

                                                  Equations
                                                  Instances For
                                                    source
                                                    noncomputable def LO.Arith.Formalized.qqNLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (x y : V) :
                                                    V

                                                    Imported declaration from the Incompleteness formalization.

                                                    Equations
                                                    Instances For
                                                      source
                                                      def LO.Arith.Formalized.«term_^=_» :
                                                      Lean.TrailingParserDescr

                                                      Imported declaration from the Incompleteness formalization.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        source
                                                        def LO.Arith.Formalized.«term_^≠_» :
                                                        Lean.TrailingParserDescr

                                                        Imported declaration from the Incompleteness formalization.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          source
                                                          def LO.Arith.Formalized.«term_^<_» :
                                                          Lean.TrailingParserDescr

                                                          Imported declaration from the Incompleteness formalization.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            source
                                                            def LO.Arith.Formalized.«term_^</_» :
                                                            Lean.TrailingParserDescr

                                                            Imported declaration from the Incompleteness formalization.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              source
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqEQ_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (x y : V) :
                                                              x < x ^= y
                                                              source
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqEQ_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (x y : V) :
                                                              y < x ^= y
                                                              source
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqLT_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (x y : V) :
                                                              x < x ^< y
                                                              source
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqLT_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (x y : V) :
                                                              y < x ^< y
                                                              source
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqNEQ_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (x y : V) :
                                                              x < x ^≠ y
                                                              source
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqNEQ_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (x y : V) :
                                                              y < x ^≠ y
                                                              source
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqNLT_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (x y : V) :
                                                              x < x ^</ y
                                                              source
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqNLT_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (x y : V) :
                                                              y < x ^</ y
                                                              source
                                                              def LO.FirstOrder.Arith.qqEQDef :
                                                              Sg1.Semisentence 3

                                                              Imported declaration from the Incompleteness formalization.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                source
                                                                def LO.FirstOrder.Arith.qqNEQDef :
                                                                Sg1.Semisentence 3

                                                                Imported declaration from the Incompleteness formalization.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  source
                                                                  def LO.FirstOrder.Arith.qqLTDef :
                                                                  Sg1.Semisentence 3

                                                                  Imported declaration from the Incompleteness formalization.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    source
                                                                    def LO.FirstOrder.Arith.qqNLTDef :
                                                                    Sg1.Semisentence 3

                                                                    Imported declaration from the Incompleteness formalization.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      source
                                                                      theorem LO.Arith.Formalized.qqEQ_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] :
                                                                      FirstOrder.Arith.Sg1-Function₂ qqEQ via FirstOrder.Arith.qqEQDef
                                                                      source
                                                                      theorem LO.Arith.Formalized.qqNEQ_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] :
                                                                      FirstOrder.Arith.Sg1-Function₂ qqNEQ via FirstOrder.Arith.qqNEQDef
                                                                      source
                                                                      theorem LO.Arith.Formalized.qqLT_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] :
                                                                      FirstOrder.Arith.Sg1-Function₂ qqLT via FirstOrder.Arith.qqLTDef
                                                                      source
                                                                      theorem LO.Arith.Formalized.qqNLT_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] :
                                                                      FirstOrder.Arith.Sg1-Function₂ qqNLT via FirstOrder.Arith.qqNLTDef
                                                                      source
                                                                      instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (Γ : SigmaPiDelta) (m : ℕ) :
                                                                      { Γ := Γ, rank := m + 1 }-Function₂ qqEQ
                                                                      source
                                                                      instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqNEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (Γ : SigmaPiDelta) (m : ℕ) :
                                                                      { Γ := Γ, rank := m + 1 }-Function₂ qqNEQ
                                                                      source
                                                                      instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (Γ : SigmaPiDelta) (m : ℕ) :
                                                                      { Γ := Γ, rank := m + 1 }-Function₂ qqLT
                                                                      source
                                                                      instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqNLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (Γ : SigmaPiDelta) (m : ℕ) :
                                                                      { Γ := Γ, rank := m + 1 }-Function₂ qqNLT
                                                                      source
                                                                      @[simp]
                                                                      theorem LO.Arith.Formalized.eval_qqEQDef {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (v : Fin 3 → V) :
                                                                      V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.qqEQDef) ↔ v 0 = v 1 ^= v 2
                                                                      source
                                                                      @[simp]
                                                                      theorem LO.Arith.Formalized.eval_qqNEQDef {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (v : Fin 3 → V) :
                                                                      V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.qqNEQDef) ↔ v 0 = v 1 ^≠ v 2
                                                                      source
                                                                      @[simp]
                                                                      theorem LO.Arith.Formalized.eval_qqLTDef {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (v : Fin 3 → V) :
                                                                      V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.qqLTDef) ↔ v 0 = v 1 ^< v 2
                                                                      source
                                                                      @[simp]
                                                                      theorem LO.Arith.Formalized.eval_qqNLTDef {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] (v : Fin 3 → V) :
                                                                      V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.qqNLTDef) ↔ v 0 = v 1 ^</ v 2
                                                                      source
                                                                      theorem LO.Arith.Formalized.neg_eq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {t u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :
                                                                      ⌜ℒₒᵣ⌝.neg (t ^= u) = t ^≠ u
                                                                      source
                                                                      theorem LO.Arith.Formalized.neg_neq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {t u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :
                                                                      ⌜ℒₒᵣ⌝.neg (t ^≠ u) = t ^= u
                                                                      source
                                                                      theorem LO.Arith.Formalized.neg_lt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {t u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :
                                                                      ⌜ℒₒᵣ⌝.neg (t ^< u) = t ^</ u
                                                                      source
                                                                      theorem LO.Arith.Formalized.neg_nlt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {t u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :
                                                                      ⌜ℒₒᵣ⌝.neg (t ^</ u) = t ^< u
                                                                      source
                                                                      theorem LO.Arith.Formalized.substs_eq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈Sg1] {w t u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :
                                                                      ⌜ℒₒᵣ⌝.substs w (t ^= u) = ⌜ℒₒᵣ⌝.termSubst w t ^= ⌜ℒₒᵣ⌝.termSubst w u