Documentation

Foundation.FirstOrder.Bootstrapping.Syntax.Term.Typed

Typed Formalized IsSemiterm/Term #

source
noncomputable def LO.FirstOrder.Arithmetic.matrixToVec {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {k : β„•} (v : Fin k β†’ V) :
V
Equations
Instances For
    source
    @[simp]
    theorem LO.FirstOrder.Arithmetic.matrixToVec_nil {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] (v : Fin 0 β†’ V) :
    matrixToVec v = 0
    source
    @[simp]
    theorem LO.FirstOrder.Arithmetic.matrixToVec_succ {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {k : β„•} (v : Fin (k + 1) β†’ V) :
    matrixToVec v = adjoin (Matrix.vecHead v) (matrixToVec (Matrix.vecTail v))
    source
    @[simp]
    theorem LO.FirstOrder.Arithmetic.matrixToVec_len {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {k : β„•} (v : Fin k β†’ V) :
    len (matrixToVec v) = ↑k
    source
    @[simp]
    theorem LO.FirstOrder.Arithmetic.matrixToVec_nth {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {k : β„•} (v : Fin k β†’ V) (i : Fin k) :
    nth (matrixToVec v) ↑↑i = v i
    source
    structure LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm (V : Type u_1) [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] (L : Language) [L.Encodable] [L.LORDefinable] (n : β„•) :
    Type u_1
    Instances For
      source
      @[reducible, inline]
      abbrev LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec (V : Type u_1) [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] (L : Language) [L.Encodable] [L.LORDefinable] (m n : β„•) :
      Type u_1
      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev LO.FirstOrder.Arithmetic.Bootstrapping.Term (V : Type u_1) [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] (L : Language) [L.Encodable] [L.LORDefinable] :
        Type u_1
        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev LO.FirstOrder.Arithmetic.Bootstrapping.TermVec (V : Type u_1) [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] (L : Language) [L.Encodable] [L.LORDefinable] (m : β„•) :
          Type u_1
          Equations
          Instances For
            source
            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.ext {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (t u : Semiterm V L n) (h : t.val = u.val) :
            t = u
            source
            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.ext_iff {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} {t u : Semiterm V L n} :
            t = u ↔ t.val = u.val
            source
            @[simp]
            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.isSemiterm_zero {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] (t : Term V L) :
            IsSemiterm L 0 t.val
            source
            @[simp]
            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.isSemiterm_one {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] (t : Semiterm V L 1) :
            IsSemiterm L 1 t.val
            source
            @[simp]
            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.isSemiterm_succ {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (t : Semiterm V L (n + 1)) :
            IsSemiterm L (↑n + 1) t.val
            source
            @[simp]
            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.isUTerm {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (t : Semiterm V L n) :
            IsUTerm L t.val
            source
            noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.val {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (v : SemitermVec V L k n) :
            V
            Equations
            Instances For
              source
              @[simp]
              theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.val_nil {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (v : SemitermVec V L 0 n) :
              v.val = 0
              source
              @[simp]
              theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.val_cons {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (t : Semiterm V L n) (v : SemitermVec V L k n) :
              val (t :> v) = Adjoin.adjoin t.val v.val
              source
              @[simp]
              theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.val_succ {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (v : SemitermVec V L (k + 1) n) :
              v.val = Adjoin.adjoin (Matrix.vecHead v).val (val (Matrix.vecTail v))
              source
              theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.val_inj {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (v₁ vβ‚‚ : SemitermVec V L k n) :
              v₁ = vβ‚‚ ↔ v₁.val = vβ‚‚.val
              source
              @[simp]
              theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.isSemitermVec {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n k : β„•} (v : SemitermVec V L k n) :
              IsSemitermVec L (↑k) (↑n) v.val
              source
              @[simp]
              theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.isUTermVec {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n k : β„•} (v : SemitermVec V L k n) :
              IsUTermVec L (↑k) v.val
              source
              @[simp]
              theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.len_eq {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (v : SemitermVec V L k n) :
              len v.val = ↑k
              source
              @[simp]
              theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.val_nth_eq {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (v : SemitermVec V L k n) (i : Fin k) :
              nth v.val ↑↑i = (v i).val
              source
              noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.bvar {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (z : Fin n) :
              Semiterm V L n
              Equations
              Instances For
                source
                noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.fvar {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (x : V) :
                Semiterm V L n
                Equations
                Instances For
                  source
                  noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.func {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (f : L.Func k) (v : SemitermVec V L k n) :
                  Semiterm V L n
                  Equations
                  Instances For
                    source
                    @[reducible, inline]
                    noncomputable abbrev LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.bv {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (x : Fin n) :
                    Semiterm V L n
                    Equations
                    Instances For
                      source
                      @[reducible, inline]
                      noncomputable abbrev LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.fv {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (x : V) :
                      Semiterm V L n
                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.bvar_val {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (z : Fin n) :
                        (bvar z).val = qqBvar ↑↑z
                        source
                        @[simp]
                        theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.fvar_val {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (x : V) :
                        (fvar x).val = qqFvar x
                        source
                        @[simp]
                        theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.func_val {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (f : L.Func k) (v : SemitermVec V L k n) :
                        (func f v).val = qqFunc ↑k ⌜f⌝ v.val
                        source
                        @[simp]
                        theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.bvar_inj_iff {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (z x : Fin n) :
                        bvar z = bvar x ↔ z = x
                        source
                        @[simp]
                        theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.fvar_inj_iff {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (z x : V) :
                        fvar z = fvar x ↔ z = x
                        source
                        @[simp]
                        theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.func_inj_iff {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (f₁ fβ‚‚ : L.Func k) (v₁ vβ‚‚ : SemitermVec V L k n) :
                        func f₁ v₁ = func fβ‚‚ vβ‚‚ ↔ f₁ = fβ‚‚ ∧ v₁ = vβ‚‚
                        source
                        noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.shift {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (t : Semiterm V L n) :
                        Semiterm V L n
                        Equations
                        Instances For
                          source
                          noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.bShift {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (t : Semiterm V L n) :
                          Semiterm V L (n + 1)
                          Equations
                          Instances For
                            source
                            noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.subst {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n m : β„•} (w : SemitermVec V L n m) (t : Semiterm V L n) :
                            Semiterm V L m
                            Equations
                            Instances For
                              source
                              noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.free {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] (t : Semiterm V L 1) :
                              Semiterm V L 0
                              Equations
                              Instances For
                                source
                                @[simp]
                                theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.val_shift {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (t : Semiterm V L n) :
                                t.shift.val = termShift L t.val
                                source
                                @[simp]
                                theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.val_bShift {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (t : Semiterm V L n) :
                                t.bShift.val = termBShift L t.val
                                source
                                @[simp]
                                theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.val_substs {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n m : β„•} (w : SemitermVec V L n m) (t : Semiterm V L n) :
                                (subst w t).val = termSubst L w.val t.val
                                source
                                @[simp]
                                theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.val_shift {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (v : SemitermVec V L k n) :
                                val (Semiterm.shift⨟ v) = termShiftVec L (↑k) v.val
                                source
                                @[simp]
                                theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.val_bShift {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (v : SemitermVec V L k n) :
                                val (Semiterm.bShift⨟ v) = termBShiftVec L (↑k) v.val
                                source
                                @[simp]
                                theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.val_substs {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n m : β„•} (v : SemitermVec V L k n) (w : SemitermVec V L n m) :
                                val ((Semiterm.subst w)⨟ v) = termSubstVec L (↑k) w.val v.val
                                source
                                noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.q {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (w : SemitermVec V L k n) :
                                SemitermVec V L (k + 1) (n + 1)
                                Equations
                                Instances For
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.q_zero {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (w : SemitermVec V L k n) :
                                  w.q 0 = Semiterm.bvar 0
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.q_succ {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (w : SemitermVec V L k n) (i : Fin k) :
                                  w.q i.succ = (w i).bShift
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.q_val_eq_qVec {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (w : SemitermVec V L k n) :
                                  w.q.val = qVec L w.val
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.q_vecHead {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (w : SemitermVec V L k n) :
                                  Matrix.vecHead w.q = Semiterm.bvar 0
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.q_vecTail {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (w : SemitermVec V L k n) :
                                  Matrix.vecTail w.q = Semiterm.bShift⨟ w
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.shift_bvar {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (z : Fin n) :
                                  (bvar z).shift = bvar z
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.shift_fvar {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (x : V) :
                                  (fvar x).shift = fvar (x + 1)
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.shift_func {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (f : L.Func k) (v : SemitermVec V L k n) :
                                  (func f v).shift = func f (shift⨟ v)
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.bShift_bvar {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (z : Fin n) :
                                  (bvar z).bShift = bvar z.succ
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.bShift_fvar {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (x : V) :
                                  (fvar x).bShift = fvar x
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.bShift_func {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n : β„•} (f : L.Func k) (v : SemitermVec V L k n) :
                                  (func f v).bShift = func f (bShift⨟ v)
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.substs_bvar {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n m : β„•} (z : Fin n) (w : SemitermVec V L n m) :
                                  subst w (bvar z) = w z
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.substs_fvar {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n m : β„•} (w : SemitermVec V L n m) (x : V) :
                                  subst w (fvar x) = fvar x
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.substs_func {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {k n m : β„•} (f : L.Func k) (w : SemitermVec V L n m) (v : SemitermVec V L k n) :
                                  subst w (func f v) = func f ((subst w)⨟ v)
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.free_bvar {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] (z : Fin 1) :
                                  (bvar z).free = fvar 0
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.free_fvar {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] (x : V) :
                                  (fvar x).free = fvar (x + 1)
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.bShift_substs_q {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n m : β„•} (t : Semiterm V L n) (w : SemitermVec V L n m) :
                                  subst w.q t.bShift = (subst w t).bShift
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.bShift_substs_sing {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] (t u : Term V L) :
                                  subst ![u] (bShift t) = t
                                  source
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.bShift_substs_succ {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n m : β„•} (w : SemitermVec V L (n + 1) m) (t : Semiterm V L n) :
                                  subst w t.bShift = subst (Matrix.vecTail w) t
                                  source
                                  @[simp]
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.bShift_substs_zero {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] (t : Term V L) :
                                  subst ![] t = t
                                  source
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.bShift_shift_comm {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (t : Semiterm V L n) :
                                  t.shift.bShift = t.bShift.shift
                                  source
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.shift_substs {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n m : β„•} (w : SemitermVec V L n m) (t : Semiterm V L n) :
                                  (subst w t).shift = subst (shift⨟ w) t.shift
                                  source
                                  theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.substs_substs {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n m l : β„•} (v : SemitermVec V L m l) (w : SemitermVec V L n m) (t : Semiterm V L n) :
                                  subst v (subst w t) = subst ((subst v)⨟ w) t
                                  source
                                  def LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.FVFree {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (t : Semiterm V L n) :
                                  Prop
                                  Equations
                                  Instances For
                                    source
                                    theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.FVFree.iff {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} {t : Semiterm V L n} :
                                    t.FVFree ↔ t.shift = t
                                    source
                                    @[simp]
                                    theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.FVFree.bvar {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (i : Fin n) :
                                    (Semiterm.bvar i).FVFree
                                    source
                                    @[simp]
                                    theorem LO.FirstOrder.Arithmetic.Bootstrapping.Semiterm.FVFree.bShift {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {L : Language} [L.Encodable] [L.LORDefinable] {n : β„•} (t : Semiterm V L n) (ht : t.FVFree) :
                                    t.bShift.FVFree
                                    source
                                    noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.typedNumeral {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (m : V) :
                                    Semiterm V β„’β‚’α΅£ n
                                    Equations
                                    Instances For
                                      source
                                      def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.term𝕹_ :
                                      Lean.ParserDescr
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.add {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (t u : Semiterm V β„’β‚’α΅£ n) :
                                        Semiterm V β„’β‚’α΅£ n
                                        Equations
                                        Instances For
                                          source
                                          noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.mul {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (t u : Semiterm V β„’β‚’α΅£ n) :
                                          Semiterm V β„’β‚’α΅£ n
                                          Equations
                                          Instances For
                                            source
                                            @[implicit_reducible]
                                            noncomputable instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.instAddSemitermORing {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] (n : β„•) :
                                            Add (Semiterm V β„’β‚’α΅£ n)
                                            Equations
                                            source
                                            @[implicit_reducible]
                                            noncomputable instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.instMulSemitermORing {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] (n : β„•) :
                                            Mul (Semiterm V β„’β‚’α΅£ n)
                                            Equations
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.val_numeral {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (x : V) :
                                            (typedNumeral x).val = numeral x
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.val_add {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (t₁ tβ‚‚ : Semiterm V β„’β‚’α΅£ n) :
                                            (t₁ + tβ‚‚).val = t₁.val ^+ tβ‚‚.val
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.val_mul {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (t₁ tβ‚‚ : Semiterm V β„’β‚’α΅£ n) :
                                            (t₁ * tβ‚‚).val = t₁.val ^* tβ‚‚.val
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.zero_eq {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (v : SemitermVec V β„’β‚’α΅£ 0 n) :
                                            Semiterm.func Language.Zero.zero v = typedNumeral 0
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.one_eq {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (v : SemitermVec V β„’β‚’α΅£ 0 n) :
                                            Semiterm.func Language.One.one v = typedNumeral 1
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.add_eq {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (v : Fin 2 β†’ Semiterm V β„’β‚’α΅£ n) :
                                            Semiterm.func Language.Add.add v = v 0 + v 1
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.mul_eq {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (v : Fin 2 β†’ Semiterm V β„’β‚’α΅£ n) :
                                            Semiterm.func Language.Mul.mul v = v 0 * v 1
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.add_inj_iff {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} {t₁ tβ‚‚ u₁ uβ‚‚ : Semiterm V β„’β‚’α΅£ n} :
                                            t₁ + tβ‚‚ = u₁ + uβ‚‚ ↔ t₁ = u₁ ∧ tβ‚‚ = uβ‚‚
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.mul_inj_iff {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} {t₁ tβ‚‚ u₁ uβ‚‚ : Semiterm V β„’β‚’α΅£ n} :
                                            t₁ * tβ‚‚ = u₁ * uβ‚‚ ↔ t₁ = u₁ ∧ tβ‚‚ = uβ‚‚
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_add_two' {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (x : V) :
                                            typedNumeral (x + 1 + 1) = typedNumeral (x + 1) + typedNumeral 1
                                            source
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_succ_pos' {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} {x : V} (pos : 0 < x) :
                                            typedNumeral (x + 1) = typedNumeral x + typedNumeral 1
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.subst_numeral {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n m : β„•} (w : SemitermVec V β„’β‚’α΅£ n m) (x : V) :
                                            Semiterm.subst w (typedNumeral x) = typedNumeral x
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.subst_add {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n m : β„•} (w : SemitermVec V β„’β‚’α΅£ n m) (t₁ tβ‚‚ : Semiterm V β„’β‚’α΅£ n) :
                                            Semiterm.subst w (t₁ + tβ‚‚) = Semiterm.subst w t₁ + Semiterm.subst w tβ‚‚
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.subst_mul {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n m : β„•} (w : SemitermVec V β„’β‚’α΅£ n m) (t₁ tβ‚‚ : Semiterm V β„’β‚’α΅£ n) :
                                            Semiterm.subst w (t₁ * tβ‚‚) = Semiterm.subst w t₁ * Semiterm.subst w tβ‚‚
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.shift_numeral {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (x : V) :
                                            (typedNumeral x).shift = typedNumeral x
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.shift_add {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (t₁ tβ‚‚ : Semiterm V β„’β‚’α΅£ n) :
                                            (t₁ + tβ‚‚).shift = t₁.shift + tβ‚‚.shift
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.shift_mul {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (t₁ tβ‚‚ : Semiterm V β„’β‚’α΅£ n) :
                                            (t₁ * tβ‚‚).shift = t₁.shift * tβ‚‚.shift
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.bShift_numeral {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (x : V) :
                                            (typedNumeral x).bShift = typedNumeral x
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.bShift_add {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (t₁ tβ‚‚ : Semiterm V β„’β‚’α΅£ n) :
                                            (t₁ + tβ‚‚).bShift = t₁.bShift + tβ‚‚.bShift
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.bShift_mul {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (t₁ tβ‚‚ : Semiterm V β„’β‚’α΅£ n) :
                                            (t₁ * tβ‚‚).bShift = t₁.bShift * tβ‚‚.bShift
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.fvFree_numeral {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (x : V) :
                                            (typedNumeral x).FVFree
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.fvFree_add {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (t₁ tβ‚‚ : Semiterm V β„’β‚’α΅£ n) :
                                            (t₁ + tβ‚‚).FVFree ↔ t₁.FVFree ∧ tβ‚‚.FVFree
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.fvFree_mul {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] {n : β„•} (t₁ tβ‚‚ : Semiterm V β„’β‚’α΅£ n) :
                                            (t₁ * tβ‚‚).FVFree ↔ t₁.FVFree ∧ tβ‚‚.FVFree
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.free_add {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] (t₁ tβ‚‚ : Semiterm V β„’β‚’α΅£ 1) :
                                            (t₁ + tβ‚‚).free = t₁.free + tβ‚‚.free
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.free_mul {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] (t₁ tβ‚‚ : Semiterm V β„’β‚’α΅£ 1) :
                                            (t₁ * tβ‚‚).free = t₁.free * tβ‚‚.free
                                            source
                                            @[simp]
                                            theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.free_numeral {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] (x : V) :
                                            (typedNumeral x).free = typedNumeral x