Documentation

Arithmetization.ISigmaOne.Metamath.Formula.Functions

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

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

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

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

          @[simp]
          theorem LO.Arith.neg_inj_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
          L.neg p = L.neg q p = q
          def LO.Arith.Language.imp {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : V) (q : V) :
          V
          Equations
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def LO.Arith.Language.iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : V) (q : V) :
              V
              Equations
              Instances For
                @[simp]
                theorem LO.Arith.Language.IsUFormula.imp {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} :
                L.IsUFormula (p ^→[L] q) L.IsUFormula p L.IsUFormula q
                @[simp]
                theorem LO.Arith.Language.IsSemiformula.imp {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} {q : V} :
                L.IsSemiformula n (p ^→[L] q) L.IsSemiformula n p L.IsSemiformula n q
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem LO.Arith.Language.imp_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                  𝚺₁-Function₂ L.imp via pL.impDef
                  instance LO.Arith.Language.imp_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                  Equations
                  • =
                  instance LO.Arith.Language.imp_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : } :
                  { Γ := Γ, rank := m + 1 }-Function₂ L.imp
                  Equations
                  • =
                  @[simp]
                  theorem LO.Arith.Language.IsUFormula.iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} :
                  L.IsUFormula (L.iff p q) L.IsUFormula p L.IsUFormula q
                  @[simp]
                  theorem LO.Arith.Language.IsSemiformula.iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} {q : V} :
                  L.IsSemiformula n (L.iff p q) L.IsSemiformula n p L.IsSemiformula n q
                  @[simp]
                  theorem LO.Arith.lt_iff_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : V) (q : V) :
                  p < L.iff p q
                  @[simp]
                  theorem LO.Arith.lt_iff_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : V) (q : V) :
                  q < L.iff p q
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem LO.Arith.Language.iff_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                    𝚺₁-Function₂ L.iff via pL.qqIffDef
                    instance LO.Arith.Language.iff_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                    Equations
                    • =
                    instance LO.Arith.Language.iff_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : } :
                    { Γ := Γ, rank := m + 1 }-Function₂ L.iff
                    Equations
                    • =
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def LO.Arith.Language.shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : V) :
                        V
                        Equations
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            theorem LO.Arith.Language.shift_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                            𝚺₁-Function₁ L.shift via pL.shiftDef
                            instance LO.Arith.Language.shift_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                            Equations
                            • =
                            instance LO.Arith.language.shift_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : } :
                            { Γ := Γ, rank := m + 1 }-Function₁ L.shift
                            Equations
                            • =
                            @[simp]
                            theorem LO.Arith.shift_rel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                            L.shift (LO.Arith.qqRel k R v) = LO.Arith.qqRel k R (L.termShiftVec k v)
                            @[simp]
                            theorem LO.Arith.shift_nrel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                            L.shift (LO.Arith.qqNRel k R v) = LO.Arith.qqNRel k R (L.termShiftVec k v)
                            @[simp]
                            theorem LO.Arith.shift_verum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                            L.shift LO.Arith.qqVerum = LO.Arith.qqVerum
                            @[simp]
                            theorem LO.Arith.shift_falsum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                            L.shift LO.Arith.qqFalsum = LO.Arith.qqFalsum
                            @[simp]
                            theorem LO.Arith.shift_and {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                            L.shift (LO.Arith.qqAnd p q) = LO.Arith.qqAnd (L.shift p) (L.shift q)
                            @[simp]
                            theorem LO.Arith.shift_or {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                            L.shift (LO.Arith.qqOr p q) = LO.Arith.qqOr (L.shift p) (L.shift q)
                            @[simp]
                            theorem LO.Arith.shift_all {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :
                            L.shift (LO.Arith.qqAll p) = LO.Arith.qqAll (L.shift p)
                            @[simp]
                            theorem LO.Arith.shift_ex {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :
                            L.shift (LO.Arith.qqEx p) = LO.Arith.qqEx (L.shift p)
                            theorem LO.Arith.shift_not_uformula {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {x : V} (h : ¬L.IsUFormula x) :
                            L.shift x = 0
                            theorem LO.Arith.Language.IsUFormula.shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
                            L.IsUFormula pL.IsUFormula (L.shift p)
                            theorem LO.Arith.Language.IsUFormula.bv_shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
                            L.IsUFormula pL.bv (L.shift p) = L.bv p
                            theorem LO.Arith.Language.IsSemiformula.shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} :
                            L.IsSemiformula n pL.IsSemiformula n (L.shift p)
                            @[simp]
                            theorem LO.Arith.Language.IsSemiformula.shift_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} :
                            L.IsSemiformula n (L.shift p) L.IsSemiformula n p
                            theorem LO.Arith.shift_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} (hp : L.IsSemiformula n p) :
                            L.shift (L.neg p) = L.neg (L.shift p)
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem LO.Arith.Language.qVec_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                              𝚺₁-Function₁ L.qVec via pL.qVecDef
                              instance LO.Arith.Language.qVec_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                              Equations
                              • =
                              instance LO.Arith.Language.qVec_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : } :
                              { Γ := Γ, rank := m + 1 }-Function₁ L.qVec
                              Equations
                              • =
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  def LO.Arith.Language.substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (w : V) (p : V) :
                                  V
                                  Equations
                                  Instances For
                                    Equations
                                    Instances For
                                      theorem LO.Arith.Language.substs_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                                      𝚺₁-Function₂ L.substs via pL.substsDef
                                      instance LO.Arith.Language.substs_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                                      Equations
                                      • =
                                      instance LO.Arith.Language.substs_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : } :
                                      { Γ := Γ, rank := m + 1 }-Function₂ L.substs
                                      Equations
                                      • =
                                      @[simp]
                                      theorem LO.Arith.substs_rel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                                      L.substs w (LO.Arith.qqRel k R v) = LO.Arith.qqRel k R (L.termSubstVec k w v)
                                      @[simp]
                                      theorem LO.Arith.substs_nrel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                                      L.substs w (LO.Arith.qqNRel k R v) = LO.Arith.qqNRel k R (L.termSubstVec k w v)
                                      @[simp]
                                      theorem LO.Arith.substs_verum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (w : V) :
                                      L.substs w LO.Arith.qqVerum = LO.Arith.qqVerum
                                      @[simp]
                                      theorem LO.Arith.substs_falsum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (w : V) :
                                      L.substs w LO.Arith.qqFalsum = LO.Arith.qqFalsum
                                      @[simp]
                                      theorem LO.Arith.substs_and {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                                      L.substs w (LO.Arith.qqAnd p q) = LO.Arith.qqAnd (L.substs w p) (L.substs w q)
                                      @[simp]
                                      theorem LO.Arith.substs_or {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                                      L.substs w (LO.Arith.qqOr p q) = LO.Arith.qqOr (L.substs w p) (L.substs w q)
                                      @[simp]
                                      theorem LO.Arith.substs_all {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {p : V} (hp : L.IsUFormula p) :
                                      L.substs w (LO.Arith.qqAll p) = LO.Arith.qqAll (L.substs (L.qVec w) p)
                                      @[simp]
                                      theorem LO.Arith.substs_ex {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {p : V} (hp : L.IsUFormula p) :
                                      L.substs w (LO.Arith.qqEx p) = LO.Arith.qqEx (L.substs (L.qVec w) p)
                                      theorem LO.Arith.isUFormula_subst_induction_sigma1 {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {P : VVVProp} (hP : 𝚺₁-Relation₃ P) (hRel : ∀ (w k R v : V), L.Rel k RL.IsUTermVec k vP w (LO.Arith.qqRel k R v) (LO.Arith.qqRel k R (L.termSubstVec k w v))) (hNRel : ∀ (w k R v : V), L.Rel k RL.IsUTermVec k vP w (LO.Arith.qqNRel k R v) (LO.Arith.qqNRel k R (L.termSubstVec k w v))) (hverum : ∀ (w : V), P w LO.Arith.qqVerum LO.Arith.qqVerum) (hfalsum : ∀ (w : V), P w LO.Arith.qqFalsum LO.Arith.qqFalsum) (hand : ∀ (w p q : V), L.IsUFormula pL.IsUFormula qP w p (L.substs w p)P w q (L.substs w q)P w (LO.Arith.qqAnd p q) (LO.Arith.qqAnd (L.substs w p) (L.substs w q))) (hor : ∀ (w p q : V), L.IsUFormula pL.IsUFormula qP w p (L.substs w p)P w q (L.substs w q)P w (LO.Arith.qqOr p q) (LO.Arith.qqOr (L.substs w p) (L.substs w q))) (hall : ∀ (w p : V), L.IsUFormula pP (L.qVec w) p (L.substs (L.qVec w) p)P w (LO.Arith.qqAll p) (LO.Arith.qqAll (L.substs (L.qVec w) p))) (hex : ∀ (w p : V), L.IsUFormula pP (L.qVec w) p (L.substs (L.qVec w) p)P w (LO.Arith.qqEx p) (LO.Arith.qqEx (L.substs (L.qVec w) p))) {w : V} {p : V} :
                                      L.IsUFormula pP w p (L.substs w p)
                                      theorem LO.Arith.semiformula_subst_induction {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {P : VVVVProp} (hP : 𝚺₁-Relation₄ P) (hRel : ∀ (n w k R v : V), L.Rel k RL.IsSemitermVec k n vP n w (LO.Arith.qqRel k R v) (LO.Arith.qqRel k R (L.termSubstVec k w v))) (hNRel : ∀ (n w k R v : V), L.Rel k RL.IsSemitermVec k n vP n w (LO.Arith.qqNRel k R v) (LO.Arith.qqNRel k R (L.termSubstVec k w v))) (hverum : ∀ (n w : V), P n w LO.Arith.qqVerum LO.Arith.qqVerum) (hfalsum : ∀ (n w : V), P n w LO.Arith.qqFalsum LO.Arith.qqFalsum) (hand : ∀ (n w p q : V), L.IsSemiformula n pL.IsSemiformula n qP n w p (L.substs w p)P n w q (L.substs w q)P n w (LO.Arith.qqAnd p q) (LO.Arith.qqAnd (L.substs w p) (L.substs w q))) (hor : ∀ (n w p q : V), L.IsSemiformula n pL.IsSemiformula n qP n w p (L.substs w p)P n w q (L.substs w q)P n w (LO.Arith.qqOr p q) (LO.Arith.qqOr (L.substs w p) (L.substs w q))) (hall : ∀ (n w p : V), L.IsSemiformula (n + 1) pP (n + 1) (L.qVec w) p (L.substs (L.qVec w) p)P n w (LO.Arith.qqAll p) (LO.Arith.qqAll (L.substs (L.qVec w) p))) (hex : ∀ (n w p : V), L.IsSemiformula (n + 1) pP (n + 1) (L.qVec w) p (L.substs (L.qVec w) p)P n w (LO.Arith.qqEx p) (LO.Arith.qqEx (L.substs (L.qVec w) p))) {n : V} {p : V} {w : V} :
                                      L.IsSemiformula n pP n w p (L.substs w p)
                                      @[simp]
                                      theorem LO.Arith.Language.IsSemiformula.substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} {m : V} {w : V} :
                                      L.IsSemiformula n pL.IsSemitermVec n m wL.IsSemiformula m (L.substs w p)
                                      theorem LO.Arith.substs_not_uformula {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {x : V} (h : ¬L.IsUFormula x) :
                                      L.substs w x = 0
                                      theorem LO.Arith.substs_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {m : V} {w : V} {n : V} {p : V} (hp : L.IsSemiformula n p) :
                                      L.IsSemitermVec n m wL.substs w (L.neg p) = L.neg (L.substs w p)
                                      theorem LO.Arith.shift_substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {m : V} {w : V} {n : V} {p : V} (hp : L.IsSemiformula n p) :
                                      L.IsSemitermVec n m wL.shift (L.substs w p) = L.substs (L.termShiftVec n w) (L.shift p)
                                      theorem LO.Arith.substs_substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {m : V} {w : V} {l : V} {n : V} {v : V} {p : V} (hp : L.IsSemiformula l p) :
                                      L.IsSemitermVec n m wL.IsSemitermVec l n vL.substs w (L.substs v p) = L.substs (L.termSubstVec l w v) p
                                      theorem LO.Arith.subst_eq_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {n : V} {w : V} (hp : L.IsSemiformula n p) (hw : L.IsSemitermVec n n w) (H : i < n, LO.Arith.nth w i = LO.Arith.qqBvar i) :
                                      L.substs w p = p
                                      theorem LO.Arith.subst_eq_self₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsSemiformula 1 p) :
                                      L.substs ?[LO.Arith.qqBvar 0] p = p
                                      def LO.Arith.Language.substs₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (t : V) (u : V) :
                                      V
                                      Equations
                                      • L.substs₁ t u = L.substs ?[t] u
                                      Instances For
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          theorem LO.Arith.Language.substs₁_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                                          𝚺₁-Function₂ L.substs₁ via pL.substs₁Def
                                          instance LO.Arith.Language.substs₁_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                                          Equations
                                          • =
                                          instance LO.Arith.instBoldfaceFunction₂MkHAddNatOfNatSubsts₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : } :
                                          { Γ := Γ, rank := m + 1 }-Function₂ L.substs₁
                                          Equations
                                          • =
                                          theorem LO.Arith.Language.IsSemiformula.substs₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t : V} {p : V} (ht : L.IsSemiterm n t) (hp : L.IsSemiformula 1 p) :
                                          L.IsSemiformula n (L.substs₁ t p)
                                          def LO.Arith.Language.free {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : V) :
                                          V
                                          Equations
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              theorem LO.Arith.Language.free_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                                              𝚺₁-Function₁ L.free via pL.freeDef
                                              instance LO.Arith.Language.free_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                                              Equations
                                              • =
                                              instance LO.Arith.Language.free_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : } :
                                              { Γ := Γ, rank := m + 1 }-Function₁ L.free
                                              Equations
                                              • =
                                              @[simp]
                                              theorem LO.Arith.Language.IsSemiformula.free {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsSemiformula 1 p) :
                                              L.IsFormula (L.free p)
                                              def LO.Arith.Formalized.qqEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                                              V
                                              Equations
                                              Instances For
                                                def LO.Arith.Formalized.qqNEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                                                V
                                                Equations
                                                Instances For
                                                  def LO.Arith.Formalized.qqLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                                                  V
                                                  Equations
                                                  Instances For
                                                    def LO.Arith.Formalized.qqNLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                                                    V
                                                    Equations
                                                    Instances For
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqEQ_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                                                              x < x ^= y
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqEQ_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                                                              y < x ^= y
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqLT_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                                                              x < x ^< y
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqLT_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                                                              y < x ^< y
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqNEQ_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                                                              x < x ^≠ y
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqNEQ_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                                                              y < x ^≠ y
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqNLT_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                                                              x < x ^≮ y
                                                              @[simp]
                                                              theorem LO.Arith.Formalized.lt_qqNLT_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
                                                              y < x ^≮ y
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ) :
                                                                      { Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.Formalized.qqEQ
                                                                      Equations
                                                                      • =
                                                                      instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqNEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ) :
                                                                      { Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.Formalized.qqNEQ
                                                                      Equations
                                                                      • =
                                                                      instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ) :
                                                                      { Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.Formalized.qqLT
                                                                      Equations
                                                                      • =
                                                                      instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqNLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ) :
                                                                      { Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.Formalized.qqNLT
                                                                      Equations
                                                                      • =
                                                                      theorem LO.Arith.Formalized.neg_eq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {t : V} {u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :
                                                                      ⌜ℒₒᵣ⌝.neg (t ^= u) = t ^≠ u
                                                                      theorem LO.Arith.Formalized.neg_neq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {t : V} {u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :
                                                                      ⌜ℒₒᵣ⌝.neg (t ^≠ u) = t ^= u
                                                                      theorem LO.Arith.Formalized.neg_lt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {t : V} {u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :
                                                                      ⌜ℒₒᵣ⌝.neg (t ^< u) = t ^≮ u
                                                                      theorem LO.Arith.Formalized.neg_nlt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {t : V} {u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :
                                                                      ⌜ℒₒᵣ⌝.neg (t ^≮ u) = t ^< u
                                                                      theorem LO.Arith.Formalized.substs_eq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {w : V} {t : V} {u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :
                                                                      ⌜ℒₒᵣ⌝.substs w (t ^= u) = ⌜ℒₒᵣ⌝.termSubst w t ^= ⌜ℒₒᵣ⌝.termSubst w u