Documentation

Arithmetization.ISigmaOne.Metamath.Term.Typed

Typed Formalized IsSemiterm/Term #

structure LO.Arith.Language.Semiterm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (n : V) :
Type u_1
  • val : V
  • prop : L.IsSemiterm n self.val
Instances For
    @[simp]
    theorem LO.Arith.Language.Semiterm.prop {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (self : L.Semiterm n) :
    L.IsSemiterm n self.val
    structure LO.Arith.Language.SemitermVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (m : V) (n : V) :
    Type u_1
    • val : V
    • prop : L.IsSemitermVec m n self.val
    Instances For
      @[simp]
      theorem LO.Arith.Language.SemitermVec.prop {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {m : V} {n : V} (self : L.SemitermVec m n) :
      L.IsSemitermVec m n self.val
      @[reducible, inline]
      Equations
      • L.Term = L.Semiterm 0
      Instances For
        theorem LO.Arith.Language.Semiterm.ext {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t : L.Semiterm n} {u : L.Semiterm n} (h : t.val = u.val) :
        t = u
        theorem LO.Arith.Language.Semiterm.ext_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t : L.Semiterm n} {u : L.Semiterm n} :
        t = u t.val = u.val
        @[simp]
        theorem LO.Arith.Language.Semiterm.isUTerm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
        L.IsUTerm t.val
        @[simp]
        theorem LO.Arith.Language.SemitermVec.isUTerm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} (v : L.SemitermVec k n) :
        L.IsUTermVec k v.val
        theorem LO.Arith.Language.SemitermVec.ext {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} {v : L.SemitermVec k n} {w : L.SemitermVec k n} (h : v.val = w.val) :
        v = w
        def LO.Arith.Language.bvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (z : V) (hz : autoParam (z < n) _auto✝) :
        L.Semiterm n
        Equations
        Instances For
          def LO.Arith.Language.fvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) :
          L.Semiterm n
          Equations
          Instances For
            def LO.Arith.Language.func {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {k : V} {f : V} (hf : L.Func k f) (v : L.SemitermVec k n) :
            L.Semiterm n
            Equations
            Instances For
              @[reducible, inline]
              abbrev LO.Arith.bv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) (h : autoParam (x < n) _auto✝) :
              L.Semiterm n
              Equations
              Instances For
                @[reducible, inline]
                abbrev LO.Arith.fv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) :
                L.Semiterm n
                Equations
                Instances For
                  @[simp]
                  theorem LO.Arith.Language.val_bvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (z : V) (hz : z < n) :
                  (L.bvar z hz).val = LO.Arith.qqBvar z
                  @[simp]
                  theorem LO.Arith.Language.val_fvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) :
                  (L.fvar x).val = LO.Arith.qqFvar x
                  def LO.Arith.Language.Semiterm.cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {m : V} {n : V} (t : L.Semiterm n) (v : L.SemitermVec m n) :
                  L.SemitermVec (m + 1) n
                  Equations
                  • t.cons v = { val := cons t.val v.val, prop := }
                  Instances For
                    @[simp]
                    theorem LO.Arith.Language.Semitermvec.val_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {m : V} {n : V} (t : L.Semiterm n) (v : L.SemitermVec m n) :
                    (t.cons v).val = cons t.val v.val
                    def LO.Arith.Language.SemitermVec.nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (n : V) :
                    L.SemitermVec 0 n
                    Equations
                    Instances For
                      @[reducible, inline]
                      abbrev LO.Arith.Language.Semiterm.sing {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
                      L.SemitermVec (0 + 1) n
                      Equations
                      Instances For
                        def LO.Arith.Language.Semiterm.shift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
                        L.Semiterm n
                        Equations
                        • t.shift = { val := L.termShift t.val, prop := }
                        Instances For
                          def LO.Arith.Language.Semiterm.bShift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
                          L.Semiterm (n + 1)
                          Equations
                          • t.bShift = { val := L.termBShift t.val, prop := }
                          Instances For
                            def LO.Arith.Language.Semiterm.substs {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (t : L.Semiterm n) (w : L.SemitermVec n m) :
                            L.Semiterm m
                            Equations
                            • t^ᵗ/[w] = { val := L.termSubst w.val t.val, prop := }
                            Instances For
                              @[simp]
                              theorem LO.Arith.Language.Semiterm.val_shift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
                              t.shift.val = L.termShift t.val
                              @[simp]
                              theorem LO.Arith.Language.Semiterm.val_bShift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
                              t.bShift.val = L.termBShift t.val
                              @[simp]
                              theorem LO.Arith.Language.Semiterm.val_substs {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (w : L.SemitermVec n m) (t : L.Semiterm n) :
                              t^ᵗ/[w].val = L.termSubst w.val t.val
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def LO.Arith.Language.SemitermVec.shift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} (v : L.SemitermVec k n) :
                                L.SemitermVec k n
                                Equations
                                • v.shift = { val := L.termShiftVec k v.val, prop := }
                                Instances For
                                  def LO.Arith.Language.SemitermVec.bShift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} (v : L.SemitermVec k n) :
                                  L.SemitermVec k (n + 1)
                                  Equations
                                  • v.bShift = { val := L.termBShiftVec k v.val, prop := }
                                  Instances For
                                    def LO.Arith.Language.SemitermVec.substs {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} {m : V} (v : L.SemitermVec k n) (w : L.SemitermVec n m) :
                                    L.SemitermVec k m
                                    Equations
                                    • v.substs w = { val := L.termSubstVec k w.val v.val, prop := }
                                    Instances For
                                      @[simp]
                                      theorem LO.Arith.Language.SemitermVec.val_shift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} (v : L.SemitermVec k n) :
                                      v.shift.val = L.termShiftVec k v.val
                                      @[simp]
                                      theorem LO.Arith.Language.SemitermVec.val_bShift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} (v : L.SemitermVec k n) :
                                      v.bShift.val = L.termBShiftVec k v.val
                                      @[simp]
                                      theorem LO.Arith.Language.SemitermVec.val_substs {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} {m : V} (v : L.SemitermVec k n) (w : L.SemitermVec n m) :
                                      (v.substs w).val = L.termSubstVec k w.val v.val
                                      @[simp]
                                      theorem LO.Arith.Language.SemitermVec.bShift_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {k : V} (t : L.Semiterm n) (v : L.SemitermVec k n) :
                                      (t.cons v).bShift = t.bShift.cons v.bShift
                                      @[simp]
                                      theorem LO.Arith.Language.SemitermVec.shift_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {k : V} (t : L.Semiterm n) (v : L.SemitermVec k n) :
                                      (t.cons v).shift = t.shift.cons v.shift
                                      @[simp]
                                      theorem LO.Arith.Language.SemitermVec.substs_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (w : L.SemitermVec n m) :
                                      @[simp]
                                      theorem LO.Arith.Language.SemitermVec.substs_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} {k : V} (w : L.SemitermVec n m) (t : L.Semiterm n) (v : L.SemitermVec k n) :
                                      (t.cons v).substs w = t^ᵗ/[w].cons (v.substs w)
                                      def LO.Arith.Language.SemitermVec.nth {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} (t : L.SemitermVec k n) (i : V) (hi : autoParam (i < k) _auto✝) :
                                      L.Semiterm n
                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem LO.Arith.Language.SemitermVec.nth_val {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} (v : L.SemitermVec k n) (i : V) (hi : i < k) :
                                        (v.nth i hi).val = LO.Arith.nth v.val i
                                        @[simp]
                                        theorem LO.Arith.Language.SemitermVec.nth_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {k : V} (t : L.Semiterm n) (v : L.SemitermVec k n) :
                                        (t.cons v).nth 0 = t
                                        @[simp]
                                        theorem LO.Arith.Language.SemitermVec.nth_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {k : V} (t : L.Semiterm n) (v : L.SemitermVec k n) (i : V) (hi : i < k) :
                                        (t.cons v).nth (i + 1) = v.nth i hi
                                        @[simp]
                                        theorem LO.Arith.Language.SemitermVec.nth_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {k : V} (t : L.Semiterm n) (v : L.SemitermVec (k + 1) n) :
                                        (t.cons v).nth 1 = v.nth 0
                                        theorem LO.Arith.Language.SemitermVec.nth_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {k : V} (t : L.Semiterm n) (v : L.SemitermVec k n) (i : V) (ipos : 0 < i) (hi : i < k + 1) :
                                        (t.cons v).nth i = v.nth (i - 1)
                                        def LO.Arith.Language.SemitermVec.q {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} (w : L.SemitermVec k n) :
                                        L.SemitermVec (k + 1) (n + 1)
                                        Equations
                                        • w.q = (L.bvar 0 ).cons w.bShift
                                        Instances For
                                          @[simp]
                                          theorem LO.Arith.Language.SemitermVec.q_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} (w : L.SemitermVec k n) :
                                          w.q.nth 0 = L.bvar 0
                                          @[simp]
                                          theorem LO.Arith.Language.SemitermVec.q_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} (w : L.SemitermVec k n) {i : V} (hi : i < k) :
                                          w.q.nth (i + 1) = (w.nth i hi).bShift
                                          @[simp]
                                          theorem LO.Arith.Language.SemitermVec.q_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} (w : L.SemitermVec k n) (h : 0 < k) :
                                          w.q.nth 1 = (w.nth 0 h).bShift
                                          theorem LO.Arith.Language.SemitermVec.q_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} (w : L.SemitermVec k n) (i : V) (ipos : 0 < i) (hi : i < k + 1) :
                                          w.q.nth i = (w.nth (i - 1) ).bShift
                                          @[simp]
                                          theorem LO.Arith.Language.SemitermVec.q_val_eq_qVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} (w : L.SemitermVec k n) :
                                          w.q.val = L.qVec w.val
                                          @[simp]
                                          theorem LO.Arith.Language.Semiterm.shift_bvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {z : V} {n : V} (hz : z < n) :
                                          (L.bvar z hz).shift = L.bvar z hz
                                          @[simp]
                                          theorem LO.Arith.Language.Semiterm.shift_fvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) :
                                          (L.fvar x).shift = L.fvar (x + 1)
                                          @[simp]
                                          theorem LO.Arith.Language.Semiterm.shift_func {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {k : V} {f : V} (hf : L.Func k f) (v : L.SemitermVec k n) :
                                          (L.func hf v).shift = L.func hf v.shift
                                          @[simp]
                                          theorem LO.Arith.Language.Semiterm.bShift_bvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {z : V} {n : V} (hz : z < n) :
                                          (L.bvar z hz).bShift = L.bvar (z + 1)
                                          @[simp]
                                          theorem LO.Arith.Language.Semiterm.bShift_fvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) :
                                          (L.fvar x).bShift = L.fvar x
                                          @[simp]
                                          theorem LO.Arith.Language.Semiterm.bShift_func {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {k : V} {f : V} (hf : L.Func k f) (v : L.SemitermVec k n) :
                                          (L.func hf v).bShift = L.func hf v.bShift
                                          @[simp]
                                          theorem LO.Arith.Language.Semiterm.substs_bvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {z : V} {m : V} (w : L.SemitermVec n m) (hz : z < n) :
                                          (L.bvar z hz)^ᵗ/[w] = w.nth z hz
                                          @[simp]
                                          theorem LO.Arith.Language.Semiterm.substs_fvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (w : L.SemitermVec n m) (x : V) :
                                          (L.fvar x)^ᵗ/[w] = L.fvar x
                                          @[simp]
                                          theorem LO.Arith.Language.Semiterm.substs_func {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} {k : V} {f : V} (w : L.SemitermVec n m) (hf : L.Func k f) (v : L.SemitermVec k n) :
                                          (L.func hf v)^ᵗ/[w] = L.func hf (v.substs w)
                                          @[simp]
                                          theorem LO.Arith.Language.Semiterm.bShift_substs_q {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (t : L.Semiterm n) (w : L.SemitermVec n m) :
                                          t.bShift^ᵗ/[w.q] = t^ᵗ/[w].bShift
                                          theorem LO.Arith.Language.Semiterm.bShift_shift_comm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
                                          t.shift.bShift = t.bShift.shift
                                          def LO.Arith.Language.Semiterm.FVFree {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
                                          Equations
                                          • t.FVFree = L.IsTermFVFree n t.val
                                          Instances For
                                            theorem LO.Arith.Language.Semiterm.FVFree.iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t : L.Semiterm n} :
                                            t.FVFree t.shift = t
                                            @[simp]
                                            theorem LO.Arith.Language.Semiterm.FVFree.bvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (z : V) (h : z < n) :
                                            (L.bvar z h).FVFree
                                            @[simp]
                                            theorem LO.Arith.Language.Semiterm.FVFree.bShift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) (ht : t.FVFree) :
                                            t.bShift.FVFree
                                            def LO.Arith.Formalized.typedNumeral {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) (m : V) :
                                            ⌜ℒₒᵣ⌝.Semiterm n
                                            Equations
                                            Instances For
                                              def LO.Arith.Formalized.add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (u : ⌜ℒₒᵣ⌝.Semiterm n) :
                                              ⌜ℒₒᵣ⌝.Semiterm n
                                              Equations
                                              Instances For
                                                def LO.Arith.Formalized.mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (u : ⌜ℒₒᵣ⌝.Semiterm n) :
                                                ⌜ℒₒᵣ⌝.Semiterm n
                                                Equations
                                                Instances For
                                                  Equations
                                                  Equations
                                                  @[simp]
                                                  theorem LO.Arith.Formalized.val_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
                                                  (t₁ + t₂).val = t₁.val ^+ t₂.val
                                                  @[simp]
                                                  theorem LO.Arith.Formalized.val_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
                                                  (t₁ * t₂).val = t₁.val ^* t₂.val
                                                  @[simp]
                                                  theorem LO.Arith.Formalized.add_inj_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {t₁ : ⌜ℒₒᵣ⌝.Semiterm n} {t₂ : ⌜ℒₒᵣ⌝.Semiterm n} {u₁ : ⌜ℒₒᵣ⌝.Semiterm n} {u₂ : ⌜ℒₒᵣ⌝.Semiterm n} :
                                                  t₁ + t₂ = u₁ + u₂ t₁ = u₁ t₂ = u₂
                                                  @[simp]
                                                  theorem LO.Arith.Formalized.mul_inj_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {t₁ : ⌜ℒₒᵣ⌝.Semiterm n} {t₂ : ⌜ℒₒᵣ⌝.Semiterm n} {u₁ : ⌜ℒₒᵣ⌝.Semiterm n} {u₂ : ⌜ℒₒᵣ⌝.Semiterm n} :
                                                  t₁ * t₂ = u₁ * u₂ t₁ = u₁ t₂ = u₂
                                                  @[simp]
                                                  theorem LO.Arith.Formalized.subst_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : V} {n : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
                                                  (t₁ + t₂)^ᵗ/[w] = t₁^ᵗ/[w] + t₂^ᵗ/[w]
                                                  @[simp]
                                                  theorem LO.Arith.Formalized.subst_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : V} {n : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
                                                  (t₁ * t₂)^ᵗ/[w] = t₁^ᵗ/[w] * t₂^ᵗ/[w]
                                                  @[simp]
                                                  theorem LO.Arith.Formalized.shift_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
                                                  (t₁ + t₂).shift = t₁.shift + t₂.shift
                                                  @[simp]
                                                  theorem LO.Arith.Formalized.shift_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
                                                  (t₁ * t₂).shift = t₁.shift * t₂.shift
                                                  @[simp]
                                                  theorem LO.Arith.Formalized.bShift_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
                                                  (t₁ + t₂).bShift = t₁.bShift + t₂.bShift
                                                  @[simp]
                                                  theorem LO.Arith.Formalized.bShift_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
                                                  (t₁ * t₂).bShift = t₁.bShift * t₂.bShift
                                                  @[simp]
                                                  theorem LO.Arith.Formalized.fvFree_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
                                                  (t₁ + t₂).FVFree t₁.FVFree t₂.FVFree
                                                  @[simp]
                                                  theorem LO.Arith.Formalized.fvFree_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
                                                  (t₁ * t₂).FVFree t₁.FVFree t₂.FVFree