Documentation

Arithmetization.Definability.Boldface

Equations
Instances For
    Equations
    Instances For
      theorem LO.FirstOrder.Defined.iff {L : LO.FirstOrder.Language} {V : Type u_2} [LO.FirstOrder.Structure L V] {k : } {R : (Fin kV)Prop} {p : LO.FirstOrder.Semisentence L k} (h : LO.FirstOrder.Defined R p) (v : Fin kV) :
      V ⊧/v p R v
      def LO.FirstOrder.Arith.HierarchySymbol.Defined {V : Type u_2} [LO.ORingStruc V] {k : } (R : (Fin kV)Prop) {ℌ : LO.FirstOrder.Arith.HierarchySymbol} :
      .Semisentence kProp
      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
          Instances
            theorem LO.FirstOrder.Arith.HierarchySymbol.Lightface.definable {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {P : (Fin kV)Prop} [self : .Lightface P] :
            ∃ (p : .Semisentence k), LO.FirstOrder.Arith.HierarchySymbol.Defined P p
            @[reducible, inline]
            abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedPred {V : Type u_2} [LO.ORingStruc V] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) (P : VProp) (p : .Semisentence 1) :
            Equations
            Instances For
              @[reducible, inline]
              abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedRel {V : Type u_2} [LO.ORingStruc V] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) (R : VVProp) (p : .Semisentence 2) :
              Equations
              Instances For
                @[reducible, inline]
                abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedRel₃ {V : Type u_2} [LO.ORingStruc V] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) (R : VVVProp) (p : .Semisentence 3) :
                Equations
                Instances For
                  @[reducible, inline]
                  abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedRel₄ {V : Type u_2} [LO.ORingStruc V] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) (R : VVVVProp) (p : .Semisentence 4) :
                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } (f : (Fin kV)V) (p : .Semisentence (k + 1)) :
                    Equations
                    Instances For
                      @[reducible, inline]
                      Equations
                      Instances For
                        @[reducible, inline]
                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₂ {V : Type u_2} [LO.ORingStruc V] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) (f : VVV) (p : .Semisentence 3) :
                          Equations
                          Instances For
                            @[reducible, inline]
                            abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₃ {V : Type u_2} [LO.ORingStruc V] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) (f : VVVV) (p : .Semisentence 4) :
                            Equations
                            Instances For
                              @[reducible, inline]
                              abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₄ {V : Type u_2} [LO.ORingStruc V] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) (f : VVVVV) (p : .Semisentence 5) :
                              Equations
                              Instances For
                                @[reducible, inline]
                                abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₅ {V : Type u_2} [LO.ORingStruc V] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) (f : VVVVVV) (p : .Semisentence 6) :
                                Equations
                                Instances For
                                  @[reducible, inline]
                                  Equations
                                  Instances For
                                    @[reducible, inline]
                                    Equations
                                    • (-Relation P) = .Boldface fun (v : Fin 2V) => P (v 0) (v 1)
                                    Instances For
                                      @[reducible, inline]
                                      Equations
                                      Instances For
                                        @[reducible, inline]
                                        Equations
                                        • (-Relation₄ P) = .Boldface fun (v : Fin 4V) => P (v 0) (v 1) (v 2) (v 3)
                                        Instances For
                                          @[reducible, inline]
                                          Equations
                                          • (-Relation₅ P) = .Boldface fun (v : Fin 5V) => P (v 0) (v 1) (v 2) (v 3) (v 4)
                                          Instances For
                                            @[reducible, inline]
                                            abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₆ {V : Type u_2} [LO.ORingStruc V] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) (P : VVVVVVProp) :
                                            Equations
                                            • .BoldfaceRel₆ P = .Boldface fun (v : Fin 6V) => P (v 0) (v 1) (v 2) (v 3) (v 4) (v 5)
                                            Instances For
                                              @[reducible, inline]
                                              Equations
                                              • .BoldfaceFunction f = .Boldface fun (v : Fin (k + 1)V) => v 0 = f fun (x : Fin k) => v x.succ
                                              Instances For
                                                @[reducible, inline]
                                                Equations
                                                • .BoldfaceFunction₀ c = .BoldfaceFunction fun (x : Fin 0V) => c
                                                Instances For
                                                  @[reducible, inline]
                                                  Equations
                                                  Instances For
                                                    @[reducible, inline]
                                                    Equations
                                                    • (-Function₂ f) = .BoldfaceFunction fun (v : Fin 2V) => f (v 0) (v 1)
                                                    Instances For
                                                      @[reducible, inline]
                                                      Equations
                                                      • (-Function₃ f) = .BoldfaceFunction fun (v : Fin 3V) => f (v 0) (v 1) (v 2)
                                                      Instances For
                                                        @[reducible, inline]
                                                        Equations
                                                        • (-Function₄ f) = .BoldfaceFunction fun (v : Fin 4V) => f (v 0) (v 1) (v 2) (v 3)
                                                        Instances For
                                                          @[reducible, inline]
                                                          Equations
                                                          • .BoldfaceFunction₅ f = .BoldfaceFunction fun (v : Fin 5V) => f (v 0) (v 1) (v 2) (v 3) (v 4)
                                                          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
                                                                    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
                                                                            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
                                                                                    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
                                                                                            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
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.of_iff {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {P : (Fin kV)Prop} {Q : (Fin kV)Prop} (h : ∀ (x : Fin kV), P x Q x) {p : .Semisentence k} (H : LO.FirstOrder.Arith.HierarchySymbol.Defined Q p) :
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.to_definable {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {P : (Fin kV)Prop} (p : .Semisentence k) (hP : LO.FirstOrder.Arith.HierarchySymbol.Defined P p) :
                                                                                                  .Boldface P
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction.of_eq {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {f : (Fin kV)V} {g : (Fin kV)V} (h : ∀ (x : Fin kV), f x = g x) {p : .Semisentence (k + 1)} (H : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction f p) :
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.ex {V : Type u_2} [LO.ORingStruc V] {k : } {m : } {P : (Fin (k + 1)V)Prop} {p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V (k + 1) { Γ := 𝚺, rank := m + 1 }} (hp : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p) :
                                                                                                  LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam (fun (v : Fin kV) => ∃ (x : V), P (x :> v)) p.ex
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.all {V : Type u_2} [LO.ORingStruc V] {k : } {m : } {P : (Fin (k + 1)V)Prop} {p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V (k + 1) { Γ := 𝚷, rank := m + 1 }} (hp : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p) :
                                                                                                  LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam (fun (v : Fin kV) => ∀ (x : V), P (x :> v)) p.all
                                                                                                  @[simp]
                                                                                                  Equations
                                                                                                  • =
                                                                                                  @[simp]
                                                                                                  Equations
                                                                                                  • =
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.mkPolarity {V : Type u_2} [LO.ORingStruc V] {k : } {m : } {P : (Fin kV)Prop} {Γ : LO.Polarity} (p : LO.FirstOrder.Semiformula ℒₒᵣ V k) (hp : LO.FirstOrder.Arith.Hierarchy Γ m p) (hP : ∀ (v : Fin kV), P v (LO.FirstOrder.Semiformula.Evalm V v id) p) :
                                                                                                  { Γ := Γ.coe, rank := m }.Boldface P
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_iff {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {P : (Fin kV)Prop} {Q : (Fin kV)Prop} (H : .Boldface Q) (h : ∀ (x : Fin kV), P x Q x) :
                                                                                                  .Boldface P
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_oRing {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {P : (Fin kV)Prop} (h : .Boldface P) :
                                                                                                  .Boldface P
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_delta {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {k : } {P : (Fin kV)Prop} {m : } (h : { Γ := 𝚫, rank := m }.Boldface P) :
                                                                                                  { Γ := Γ, rank := m }.Boldface P
                                                                                                  instance LO.FirstOrder.Arith.HierarchySymbol.Boldface.instMkOfDeltaSigmaPiDelta {V : Type u_2} [LO.ORingStruc V] {k : } {P : (Fin kV)Prop} {m : } [{ Γ := 𝚫, rank := m }.Boldface P] (Γ : LO.SigmaPiDelta) :
                                                                                                  { Γ := Γ, rank := m }.Boldface P
                                                                                                  Equations
                                                                                                  • =
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_sigma_of_pi {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {k : } {P : (Fin kV)Prop} {m : } (hσ : { Γ := 𝚺, rank := m }.Boldface P) (hπ : { Γ := 𝚷, rank := m }.Boldface P) :
                                                                                                  { Γ := Γ, rank := m }.Boldface P
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_zero {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {P : (Fin kV)Prop} {Γ' : LO.SigmaPiDelta} (h : { Γ := Γ', rank := 0 }.Boldface P) :
                                                                                                  .Boldface P
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_deltaOne {V : Type u_2} [LO.ORingStruc V] {k : } {P : (Fin kV)Prop} (h : 𝚫₁.Boldface P) {Γ : LO.SigmaPiDelta} {m : } :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface P
                                                                                                  instance LO.FirstOrder.Arith.HierarchySymbol.Boldface.instOfSigmaZero {V : Type u_2} [LO.ORingStruc V] {k : } {P : (Fin kV)Prop} [𝚺₀.Boldface P] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) :
                                                                                                  .Boldface P
                                                                                                  Equations
                                                                                                  • =
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.retraction {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {P : (Fin kV)Prop} (h : .Boldface P) {n : } (f : Fin kFin n) :
                                                                                                  .Boldface fun (v : Fin nV) => P fun (i : Fin k) => v (f i)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.retractiont (n : ) {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {P : (Fin kV)Prop} (h : .Boldface P) (f : Fin kLO.FirstOrder.Semiterm ℒₒᵣ V n) :
                                                                                                  .Boldface fun (v : Fin nV) => P fun (i : Fin k) => LO.FirstOrder.Semiterm.valm V v id (f i)
                                                                                                  @[simp]
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.const {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {P : Prop} :
                                                                                                  .Boldface fun (x : Fin kV) => P
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.and {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {P : (Fin kV)Prop} {Q : (Fin kV)Prop} (h₁ : .Boldface P) (h₂ : .Boldface Q) :
                                                                                                  .Boldface fun (v : Fin kV) => P v Q v
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.conj {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {l : } {P : Fin l(Fin kV)Prop} (h : ∀ (i : Fin l), .Boldface fun (w : Fin kV) => P i w) :
                                                                                                  .Boldface fun (v : Fin kV) => ∀ (i : Fin l), P i v
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.or {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {P : (Fin kV)Prop} {Q : (Fin kV)Prop} (h₁ : .Boldface P) (h₂ : .Boldface Q) :
                                                                                                  .Boldface fun (v : Fin kV) => P v Q v
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.not {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {k : } {P : (Fin kV)Prop} {m : } (h : { Γ := Γ.alt, rank := m }.Boldface P) :
                                                                                                  { Γ := Γ, rank := m }.Boldface fun (v : Fin kV) => ¬P v
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.imp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {k : } {P : (Fin kV)Prop} {Q : (Fin kV)Prop} {m : } (h₁ : { Γ := Γ.alt, rank := m }.Boldface P) (h₂ : { Γ := Γ, rank := m }.Boldface Q) :
                                                                                                  { Γ := Γ, rank := m }.Boldface fun (v : Fin kV) => P vQ v
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.iff {V : Type u_2} [LO.ORingStruc V] {k : } {P : (Fin kV)Prop} {Q : (Fin kV)Prop} {m : } (h₁ : { Γ := 𝚫, rank := m }.Boldface P) (h₂ : { Γ := 𝚫, rank := m }.Boldface Q) {Γ : LO.SigmaPiDelta} :
                                                                                                  { Γ := Γ, rank := m }.Boldface fun (v : Fin kV) => P v Q v
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.all {V : Type u_2} [LO.ORingStruc V] {k : } {s : } {P : (Fin kV)VProp} (h : { Γ := 𝚷, rank := s + 1 }.Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                  { Γ := 𝚷, rank := s + 1 }.Boldface fun (v : Fin kV) => ∀ (x : V), P v x
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ex {V : Type u_2} [LO.ORingStruc V] {k : } {s : } {P : (Fin kV)VProp} (h : { Γ := 𝚺, rank := s + 1 }.Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                  { Γ := 𝚺, rank := s + 1 }.Boldface fun (v : Fin kV) => ∃ (x : V), P v x
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.equal' {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } (i : Fin k) (j : Fin k) :
                                                                                                  .Boldface fun (v : Fin kV) => v i = v j
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_sigma {V : Type u_2} [LO.ORingStruc V] {k : } {m : } {f : (Fin kV)V} (h : { Γ := 𝚺, rank := m }.BoldfaceFunction f) {Γ : LO.SigmaPiDelta} :
                                                                                                  { Γ := Γ, rank := m }.BoldfaceFunction f
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.exVec {V : Type u_2} [LO.ORingStruc V] {m : } {k : } {l : } {P : (Fin kV)(Fin lV)Prop} (h : { Γ := 𝚺, rank := m + 1 }.Boldface fun (w : Fin (k + l)V) => P (fun (i : Fin k) => w (Fin.castAdd l i)) fun (j : Fin l) => w (Fin.natAdd k j)) :
                                                                                                  { Γ := 𝚺, rank := m + 1 }.Boldface fun (v : Fin kV) => ∃ (ys : Fin lV), P v ys
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.allVec {V : Type u_2} [LO.ORingStruc V] {m : } {k : } {l : } {P : (Fin kV)(Fin lV)Prop} (h : { Γ := 𝚷, rank := m + 1 }.Boldface fun (w : Fin (k + l)V) => P (fun (i : Fin k) => w (Fin.castAdd l i)) fun (j : Fin l) => w (Fin.natAdd k j)) :
                                                                                                  { Γ := 𝚷, rank := m + 1 }.Boldface fun (v : Fin kV) => ∀ (ys : Fin lV), P v ys
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.substitution {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {k : } {P : (Fin kV)Prop} {l : } {m : } {f : Fin k(Fin lV)V} (hP : { Γ := Γ, rank := m + 1 }.Boldface P) (hf : ∀ (i : Fin k), { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction (f i)) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (z : Fin lV) => P fun (i : Fin k) => f i z
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfacePred.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {P : VProp} {k : } {f : (Fin kV)V} (hP : { Γ := Γ, rank := m + 1 }-Predicate P) (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {P : VVProp} {k : } {f : (Fin kV)V} {g : (Fin kV)V} (hP : { Γ := Γ, rank := m + 1 }-Relation P) (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (hg : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f v) (g v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₃.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {P : VVVProp} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} (hP : { Γ := Γ, rank := m + 1 }-Relation₃ P) (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f₁ v) (f₂ v) (f₃ v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₄.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {P : VVVVProp} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} {f₄ : (Fin kV)V} (hP : { Γ := Γ, rank := m + 1 }-Relation₄ P) (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₅.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {P : VVVVVProp} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} {f₄ : (Fin kV)V} {f₅ : (Fin kV)V} (hP : { Γ := Γ, rank := m + 1 }-Relation₅ P) (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄) (hf₅ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₅) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v) (f₅ v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₁ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {P : VProp} {f : (Fin kV)V} [{ Γ := Γ, rank := m + 1 }-Predicate P] (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₂ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {P : VVProp} {f : (Fin kV)V} {g : (Fin kV)V} [{ Γ := Γ, rank := m + 1 }-Relation P] (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (hg : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f v) (g v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₃ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {P : VVVProp} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} [{ Γ := Γ, rank := m + 1 }-Relation₃ P] (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f₁ v) (f₂ v) (f₃ v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₄ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {P : VVVVProp} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} {f₄ : (Fin kV)V} [{ Γ := Γ, rank := m + 1 }-Relation₄ P] (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₅ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {P : VVVVVProp} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} {f₄ : (Fin kV)V} {f₅ : (Fin kV)V} [{ Γ := Γ, rank := m + 1 }-Relation₅ P] (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄) (hf₅ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₅) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v) (f₅ v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfacePred.of_iff {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {P : VProp} {Q : VProp} (H : -Predicate Q) (h : ∀ (x : V), P x Q x) :
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.graph_delta {V : Type u_2} [LO.ORingStruc V] {m : } {k : } {f : (Fin kV)V} (h : { Γ := 𝚺, rank := m }.BoldfaceFunction f) :
                                                                                                  { Γ := 𝚫, rank := m }.BoldfaceFunction f
                                                                                                  instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.instMkDeltaSigmaPiDeltaOfSigma {V : Type u_2} [LO.ORingStruc V] {m : } {k : } {f : (Fin kV)V} [h : { Γ := 𝚺, rank := m }.BoldfaceFunction f] :
                                                                                                  { Γ := 𝚫, rank := m }.BoldfaceFunction f
                                                                                                  Equations
                                                                                                  • =
                                                                                                  instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.instOfSigmaZero {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } {f : (Fin kV)V} [𝚺₀.BoldfaceFunction f] :
                                                                                                  .BoldfaceFunction f
                                                                                                  Equations
                                                                                                  • =
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.of_sigmaOne {V : Type u_2} [LO.ORingStruc V] {k : } {f : (Fin kV)V} (h : 𝚺₁.BoldfaceFunction f) {Γ : LO.SigmaPiDelta} {m : } :
                                                                                                  { Γ := Γ, rank := m + 1 }.BoldfaceFunction f
                                                                                                  @[simp]
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.var {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } (i : Fin k) :
                                                                                                  .BoldfaceFunction fun (v : Fin kV) => v i
                                                                                                  @[simp]
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.const {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : } (c : V) :
                                                                                                  .BoldfaceFunction fun (x : Fin kV) => c
                                                                                                  @[simp]
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.term_retraction (n : ) {V : Type u_2} [LO.ORingStruc V] {k : } {ℌ : LO.FirstOrder.Arith.HierarchySymbol} (t : LO.FirstOrder.Semiterm ℒₒᵣ V n) (e : Fin nFin k) :
                                                                                                  .BoldfaceFunction fun (v : Fin kV) => LO.FirstOrder.Semiterm.valm V (fun (x : Fin n) => v (e x)) id t
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.of_eq {V : Type u_2} [LO.ORingStruc V] {k : } {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {f : (Fin kV)V} (g : (Fin kV)V) (h : ∀ (v : Fin kV), f v = g v) (H : .BoldfaceFunction f) :
                                                                                                  .BoldfaceFunction g
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.retraction {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {n : } {k : } {f : (Fin kV)V} (hf : .BoldfaceFunction f) (e : Fin kFin n) :
                                                                                                  .BoldfaceFunction fun (v : Fin nV) => f fun (i : Fin k) => v (e i)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.retractiont {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {n : } {k : } {f : (Fin kV)V} (hf : .BoldfaceFunction f) (t : Fin kLO.FirstOrder.Semiterm ℒₒᵣ V n) :
                                                                                                  .BoldfaceFunction fun (v : Fin nV) => f fun (i : Fin k) => LO.FirstOrder.Semiterm.valm V v id (t i)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.rel {V : Type u_2} [LO.ORingStruc V] {k : } {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {f : (Fin kV)V} (h : .BoldfaceFunction f) :
                                                                                                  .Boldface fun (v : Fin k.succV) => v 0 = f fun (x : Fin k) => v x.succ
                                                                                                  @[simp]
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.nth {V : Type u_2} [LO.ORingStruc V] {k : } (ℌ : LO.FirstOrder.Arith.HierarchySymbol) (i : Fin k) :
                                                                                                  .BoldfaceFunction fun (w : Fin kV) => w i
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.substitution {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {k : } {l : } {m : } {F : (Fin kV)V} {f : Fin k(Fin lV)V} (hF : { Γ := Γ, rank := m + 1 }.BoldfaceFunction F) (hf : ∀ (i : Fin k), { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction (f i)) :
                                                                                                  { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (z : Fin lV) => F fun (i : Fin k) => f i z
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₁.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {F : VV} {f : (Fin kV)V} (hF : { Γ := Γ, rank := m + 1 }-Function₁ F) (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) :
                                                                                                  { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => F (f v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {F : VVV} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} (hF : { Γ := Γ, rank := m + 1 }-Function₂ F) (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) :
                                                                                                  { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => F (f₁ v) (f₂ v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₃.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {F : VVVV} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} (hF : { Γ := Γ, rank := m + 1 }-Function₃ F) (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) :
                                                                                                  { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => F (f₁ v) (f₂ v) (f₃ v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₄.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {F : VVVVV} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} {f₄ : (Fin kV)V} (hF : { Γ := Γ, rank := m + 1 }-Function₄ F) (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄) :
                                                                                                  { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => F (f₁ v) (f₂ v) (f₃ v) (f₄ v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₅.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {F : VVVVVV} {f₁ : (Fin kV)V} {f₂ : (Fin kV)V} {f₃ : (Fin kV)V} {f₄ : (Fin kV)V} {f₅ : (Fin kV)V} (hF : { Γ := Γ, rank := m + 1 }.BoldfaceFunction₅ F) (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄) (hf₅ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₅) :
                                                                                                  { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => F (f₁ v) (f₂ v) (f₃ v) (f₄ v) (f₅ v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₁ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {f : VV} [{ Γ := Γ, rank := m + 1 }-Function₁ f] {g : (Fin kV)V} (hg : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g) :
                                                                                                  { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => f (g v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₂ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {f : VVV} [{ Γ := Γ, rank := m + 1 }-Function₂ f] {g₁ : (Fin kV)V} {g₂ : (Fin kV)V} (hg₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₁) (hg₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₂) :
                                                                                                  { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => f (g₁ v) (g₂ v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₃ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {f : VVVV} [{ Γ := Γ, rank := m + 1 }-Function₃ f] {g₁ : (Fin kV)V} {g₂ : (Fin kV)V} {g₃ : (Fin kV)V} (hg₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₁) (hg₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₂) (hg₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₃) :
                                                                                                  { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => f (g₁ v) (g₂ v) (g₃ v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₄ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {f : VVVVV} [{ Γ := Γ, rank := m + 1 }-Function₄ f] {g₁ : (Fin kV)V} {g₂ : (Fin kV)V} {g₃ : (Fin kV)V} {g₄ : (Fin kV)V} (hg₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₁) (hg₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₂) (hg₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₃) (hg₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₄) :
                                                                                                  { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => f (g₁ v) (g₂ v) (g₃ v) (g₄ v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₅ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : } {k : } {f : VVVVVV} [{ Γ := Γ, rank := m + 1 }.BoldfaceFunction₅ f] {g₁ : (Fin kV)V} {g₂ : (Fin kV)V} {g₃ : (Fin kV)V} {g₄ : (Fin kV)V} {g₅ : (Fin kV)V} (hg₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₁) (hg₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₂) (hg₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₃) (hg₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₄) (hg₅ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₅) :
                                                                                                  { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => f (g₁ v) (g₂ v) (g₃ v) (g₄ v) (g₅ v)
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_lt {V : Type u_2} [LO.ORingStruc V] {k : } {m : } {Γ : LO.SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => x < f v, P v x
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_lt {V : Type u_2} [LO.ORingStruc V] {k : } {m : } {Γ : LO.SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => x < f v, P v x
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_le {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } {m : } {Γ : LO.SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => xf v, P v x
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_le {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } {m : } {Γ : LO.SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => xf v, P v x
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_lt' {V : Type u_2} [LO.ORingStruc V] {k : } {m : } {Γ : LO.SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => ∀ {x : V}, x < f vP v x
                                                                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_le' {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } {m : } {Γ : LO.SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                  { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => ∀ {x : V}, x f vP v x