Documentation

Arithmetization.ISigmaOne.Metamath.Formula.Basic

def LO.Arith.qqRel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k r v : V) :
V
Equations
Instances For
    def LO.Arith.qqNRel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k r v : V) :
    V
    Equations
    Instances For
      Equations
      Instances For
        Equations
        Instances For
          def LO.Arith.qqAnd {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p q : V) :
          V
          Equations
          Instances For
            def LO.Arith.qqOr {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p q : V) :
            V
            Equations
            Instances For
              def LO.Arith.qqAll {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) :
              V
              Equations
              Instances For
                def LO.Arith.qqEx {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) :
                V
                Equations
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem LO.Arith.qqRel_inj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k₁ r₁ v₁ k₂ r₂ v₂ : V) :
                                  qqRel k₁ r₁ v₁ = qqRel k₂ r₂ v₂ k₁ = k₂ r₁ = r₂ v₁ = v₂
                                  @[simp]
                                  theorem LO.Arith.qqNRel_inj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k₁ r₁ v₁ k₂ r₂ v₂ : V) :
                                  qqNRel k₁ r₁ v₁ = qqNRel k₂ r₂ v₂ k₁ = k₂ r₁ = r₂ v₁ = v₂
                                  @[simp]
                                  theorem LO.Arith.qqAnd_inj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p₁ q₁ p₂ q₂ : V) :
                                  qqAnd p₁ q₁ = qqAnd p₂ q₂ p₁ = p₂ q₁ = q₂
                                  @[simp]
                                  theorem LO.Arith.qqOr_inj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p₁ q₁ p₂ q₂ : V) :
                                  qqOr p₁ q₁ = qqOr p₂ q₂ p₁ = p₂ q₁ = q₂
                                  @[simp]
                                  theorem LO.Arith.qqAll_inj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p₁ p₂ : V) :
                                  qqAll p₁ = qqAll p₂ p₁ = p₂
                                  @[simp]
                                  theorem LO.Arith.qqEx_inj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p₁ p₂ : V) :
                                  qqEx p₁ = qqEx p₂ p₁ = p₂
                                  @[simp]
                                  theorem LO.Arith.arity_lt_rel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k r v : V) :
                                  k < qqRel k r v
                                  @[simp]
                                  theorem LO.Arith.r_lt_rel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k r v : V) :
                                  r < qqRel k r v
                                  @[simp]
                                  theorem LO.Arith.v_lt_rel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k r v : V) :
                                  v < qqRel k r v
                                  @[simp]
                                  theorem LO.Arith.arity_lt_nrel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k r v : V) :
                                  k < qqNRel k r v
                                  @[simp]
                                  theorem LO.Arith.r_lt_nrel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k r v : V) :
                                  r < qqNRel k r v
                                  @[simp]
                                  theorem LO.Arith.v_lt_nrel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k r v : V) :
                                  v < qqNRel k r v
                                  theorem LO.Arith.nth_lt_qqRel_of_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i k r v : V} (hi : i < len v) :
                                  nth v i < qqRel k r v
                                  theorem LO.Arith.nth_lt_qqNRel_of_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i k r v : V} (hi : i < len v) :
                                  nth v i < qqNRel k r v
                                  @[simp]
                                  theorem LO.Arith.lt_and_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p q : V) :
                                  p < qqAnd p q
                                  @[simp]
                                  theorem LO.Arith.lt_and_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p q : V) :
                                  q < qqAnd p q
                                  @[simp]
                                  theorem LO.Arith.lt_or_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p q : V) :
                                  p < qqOr p q
                                  @[simp]
                                  theorem LO.Arith.lt_or_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p q : V) :
                                  q < qqOr p q
                                  @[simp]
                                  theorem LO.Arith.lt_forall {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) :
                                  p < qqAll p
                                  @[simp]
                                  theorem LO.Arith.lt_exists {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) :
                                  p < qqEx p
                                  def LO.Arith.FormalizedFormula.Phi {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (C : Set V) (p : V) :
                                  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
                                        Instances For
                                          def LO.Arith.Language.IsUFormula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                                          VProp
                                          Equations
                                          Instances For
                                            Equations
                                            Instances For
                                              theorem LO.Arith.Language.isUFormula_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                                              𝚫₁-Predicate L.IsUFormula via pL.isUFormulaDef
                                              instance LO.Arith.Language.isUFormulaDef_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : } :
                                              { Γ := Γ, rank := m + 1 }-Predicate L.IsUFormula
                                              theorem LO.Arith.Language.IsUFormula.case_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
                                              L.IsUFormula p (∃ (k : V) (R : V) (v : V), L.Rel k R L.IsUTermVec k v p = qqRel k R v) (∃ (k : V) (R : V) (v : V), L.Rel k R L.IsUTermVec k v p = qqNRel k R v) p = qqVerum p = qqFalsum (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ L.IsUFormula p₂ p = qqAnd p₁ p₂) (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ L.IsUFormula p₂ p = qqOr p₁ p₂) (∃ (p₁ : V), L.IsUFormula p₁ p = qqAll p₁) ∃ (p₁ : V), L.IsUFormula p₁ p = qqEx p₁
                                              theorem LO.Arith.Language.IsUFormula.case {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
                                              L.IsUFormula p(∃ (k : V) (R : V) (v : V), L.Rel k R L.IsUTermVec k v p = qqRel k R v) (∃ (k : V) (R : V) (v : V), L.Rel k R L.IsUTermVec k v p = qqNRel k R v) p = qqVerum p = qqFalsum (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ L.IsUFormula p₂ p = qqAnd p₁ p₂) (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ L.IsUFormula p₂ p = qqOr p₁ p₂) (∃ (p₁ : V), L.IsUFormula p₁ p = qqAll p₁) ∃ (p₁ : V), L.IsUFormula p₁ p = qqEx p₁

                                              Alias of the forward direction of LO.Arith.Language.IsUFormula.case_iff.

                                              theorem LO.Arith.Language.IsUFormula.mk {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
                                              ((∃ (k : V) (R : V) (v : V), L.Rel k R L.IsUTermVec k v p = qqRel k R v) (∃ (k : V) (R : V) (v : V), L.Rel k R L.IsUTermVec k v p = qqNRel k R v) p = qqVerum p = qqFalsum (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ L.IsUFormula p₂ p = qqAnd p₁ p₂) (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ L.IsUFormula p₂ p = qqOr p₁ p₂) (∃ (p₁ : V), L.IsUFormula p₁ p = qqAll p₁) ∃ (p₁ : V), L.IsUFormula p₁ p = qqEx p₁)L.IsUFormula p

                                              Alias of the reverse direction of LO.Arith.Language.IsUFormula.case_iff.

                                              @[simp]
                                              theorem LO.Arith.Language.IsUFormula.rel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k r v : V} :
                                              L.IsUFormula (qqRel k r v) L.Rel k r L.IsUTermVec k v
                                              @[simp]
                                              theorem LO.Arith.Language.IsUFormula.nrel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k r v : V} :
                                              L.IsUFormula (qqNRel k r v) L.Rel k r L.IsUTermVec k v
                                              @[simp]
                                              theorem LO.Arith.Language.IsUFormula.verum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                                              L.IsUFormula qqVerum
                                              @[simp]
                                              theorem LO.Arith.Language.IsUFormula.falsum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                                              L.IsUFormula qqFalsum
                                              @[simp]
                                              theorem LO.Arith.Language.IsUFormula.and {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} :
                                              L.IsUFormula (qqAnd p q) L.IsUFormula p L.IsUFormula q
                                              @[simp]
                                              theorem LO.Arith.Language.IsUFormula.or {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} :
                                              L.IsUFormula (qqOr p q) L.IsUFormula p L.IsUFormula q
                                              @[simp]
                                              theorem LO.Arith.Language.IsUFormula.all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
                                              L.IsUFormula (qqAll p) L.IsUFormula p
                                              @[simp]
                                              theorem LO.Arith.Language.IsUFormula.ex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
                                              L.IsUFormula (qqEx p) L.IsUFormula p
                                              theorem LO.Arith.Language.IsUFormula.pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (h : L.IsUFormula p) :
                                              0 < p
                                              @[simp]
                                              theorem LO.Arith.Language.IsUFormula.not_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                                              ¬L.IsUFormula 0
                                              theorem LO.Arith.Language.IsUFormula.induction1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (Γ : SigmaPiDelta) {P : VProp} (hP : { Γ := Γ, rank := 1 }-Predicate P) (hrel : ∀ (k r v : V), L.Rel k rL.IsUTermVec k vP (qqRel k r v)) (hnrel : ∀ (k r v : V), L.Rel k rL.IsUTermVec k vP (qqNRel k r v)) (hverum : P qqVerum) (hfalsum : P qqFalsum) (hand : ∀ (p q : V), L.IsUFormula pL.IsUFormula qP pP qP (qqAnd p q)) (hor : ∀ (p q : V), L.IsUFormula pL.IsUFormula qP pP qP (qqOr p q)) (hall : ∀ (p : V), L.IsUFormula pP pP (qqAll p)) (hex : ∀ (p : V), L.IsUFormula pP pP (qqEx p)) (p : V) :
                                              L.IsUFormula pP p
                                              theorem LO.Arith.Language.IsUFormula.induction_sigma1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {P : VProp} (hP : 𝚺₁-Predicate P) (hrel : ∀ (k r v : V), L.Rel k rL.IsUTermVec k vP (qqRel k r v)) (hnrel : ∀ (k r v : V), L.Rel k rL.IsUTermVec k vP (qqNRel k r v)) (hverum : P qqVerum) (hfalsum : P qqFalsum) (hand : ∀ (p q : V), L.IsUFormula pL.IsUFormula qP pP qP (qqAnd p q)) (hor : ∀ (p q : V), L.IsUFormula pL.IsUFormula qP pP qP (qqOr p q)) (hall : ∀ (p : V), L.IsUFormula pP pP (qqAll p)) (hex : ∀ (p : V), L.IsUFormula pP pP (qqEx p)) (p : V) :
                                              L.IsUFormula pP p
                                              theorem LO.Arith.Language.IsUFormula.induction_pi1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {P : VProp} (hP : 𝚷₁-Predicate P) (hrel : ∀ (k r v : V), L.Rel k rL.IsUTermVec k vP (qqRel k r v)) (hnrel : ∀ (k r v : V), L.Rel k rL.IsUTermVec k vP (qqNRel k r v)) (hverum : P qqVerum) (hfalsum : P qqFalsum) (hand : ∀ (p q : V), L.IsUFormula pL.IsUFormula qP pP qP (qqAnd p q)) (hor : ∀ (p q : V), L.IsUFormula pL.IsUFormula qP pP qP (qqOr p q)) (hall : ∀ (p : V), L.IsUFormula pP pP (qqAll p)) (hex : ∀ (p : V), L.IsUFormula pP pP (qqEx p)) (p : V) :
                                              L.IsUFormula pP p
                                              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
                                                      Instances For
                                                        def LO.Arith.Language.UformulaRec1.Construction.Phi {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) (C : Set V) (pr : V) :
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          Equations
                                                          • c.construction = { Φ := fun (x : Fin 0V) => c.Phi, defined := , monotone := }
                                                          Instances For
                                                            def LO.Arith.Language.UformulaRec1.Construction.Graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) (param x y : V) :
                                                            Equations
                                                            • c.Graph param x y = c.construction.Fixpoint ![] param, x, y
                                                            Instances For
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.Graph.case_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} {c : Construction V L β} {param p y : V} :
                                                              c.Graph param p y L.IsUFormula p ((∃ (k : V) (R : V) (v : V), p = qqRel k R v y = c.rel param k R v) (∃ (k : V) (R : V) (v : V), p = qqNRel k R v y = c.nrel param k R v) p = qqVerum y = c.verum param p = qqFalsum y = c.falsum param (∃ (p₁ : V) (p₂ : V) (y₁ : V) (y₂ : V), c.Graph param p₁ y₁ c.Graph param p₂ y₂ p = qqAnd p₁ p₂ y = c.and param p₁ p₂ y₁ y₂) (∃ (p₁ : V) (p₂ : V) (y₁ : V) (y₂ : V), c.Graph param p₁ y₁ c.Graph param p₂ y₂ p = qqOr p₁ p₂ y = c.or param p₁ p₂ y₁ y₂) (∃ (p₁ : V) (y₁ : V), c.Graph (c.allChanges param) p₁ y₁ p = qqAll p₁ y = c.all param p₁ y₁) ∃ (p₁ : V) (y₁ : V), c.Graph (c.exChanges param) p₁ y₁ p = qqEx p₁ y = c.ex param p₁ y₁)
                                                              @[simp]
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.eval_graphDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (β : Blueprint pL) (c : Construction V L β) (v : Fin 3V) :
                                                              V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val β.graph) c.Graph (v 0) (v 1) (v 2)
                                                              instance LO.Arith.Language.UformulaRec1.Construction.graph_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (β : Blueprint pL) (c : Construction V L β) :
                                                              { Γ := 𝚺, rank := 0 + 1 }-Relation₃ c.Graph
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_dom_uformula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p r : V} :
                                                              c.Graph param p rL.IsUFormula p
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_rel_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param k r v y : V} (hkr : L.Rel k r) (hv : L.IsUTermVec k v) :
                                                              c.Graph param (qqRel k r v) y y = c.rel param k r v
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_nrel_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param k r v y : V} (hkr : L.Rel k r) (hv : L.IsUTermVec k v) :
                                                              c.Graph param (qqNRel k r v) y y = c.nrel param k r v
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_verum_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param y : V} :
                                                              c.Graph param qqVerum y y = c.verum param
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_falsum_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param y : V} :
                                                              c.Graph param qqFalsum y y = c.falsum param
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_rel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param k r v : V} (hkr : L.Rel k r) (hv : L.IsUTermVec k v) :
                                                              c.Graph param (qqRel k r v) (c.rel param k r v)
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_nrel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param k r v : V} (hkr : L.Rel k r) (hv : L.IsUTermVec k v) :
                                                              c.Graph param (qqNRel k r v) (c.nrel param k r v)
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_verum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param : V} :
                                                              c.Graph param qqVerum (c.verum param)
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_falsum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param : V} :
                                                              c.Graph param qqFalsum (c.falsum param)
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_and {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ p₂ r₁ r₂ : V} (hp₁ : L.IsUFormula p₁) (hp₂ : L.IsUFormula p₂) (h₁ : c.Graph param p₁ r₁) (h₂ : c.Graph param p₂ r₂) :
                                                              c.Graph param (qqAnd p₁ p₂) (c.and param p₁ p₂ r₁ r₂)
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_and_inv {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ p₂ r : V} :
                                                              c.Graph param (qqAnd p₁ p₂) r∃ (r₁ : V) (r₂ : V), c.Graph param p₁ r₁ c.Graph param p₂ r₂ r = c.and param p₁ p₂ r₁ r₂
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_or {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ p₂ r₁ r₂ : V} (hp₁ : L.IsUFormula p₁) (hp₂ : L.IsUFormula p₂) (h₁ : c.Graph param p₁ r₁) (h₂ : c.Graph param p₂ r₂) :
                                                              c.Graph param (qqOr p₁ p₂) (c.or param p₁ p₂ r₁ r₂)
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_or_inv {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ p₂ r : V} :
                                                              c.Graph param (qqOr p₁ p₂) r∃ (r₁ : V) (r₂ : V), c.Graph param p₁ r₁ c.Graph param p₂ r₂ r = c.or param p₁ p₂ r₁ r₂
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ r₁ : V} (hp₁ : L.IsUFormula p₁) (h₁ : c.Graph (c.allChanges param) p₁ r₁) :
                                                              c.Graph param (qqAll p₁) (c.all param p₁ r₁)
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_all_inv {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ r : V} :
                                                              c.Graph param (qqAll p₁) r∃ (r₁ : V), c.Graph (c.allChanges param) p₁ r₁ r = c.all param p₁ r₁
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_ex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ r₁ : V} (hp₁ : L.IsUFormula p₁) (h₁ : c.Graph (c.exChanges param) p₁ r₁) :
                                                              c.Graph param (qqEx p₁) (c.ex param p₁ r₁)
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_ex_inv {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ r : V} :
                                                              c.Graph param (qqEx p₁) r∃ (r₁ : V), c.Graph (c.exChanges param) p₁ r₁ r = c.ex param p₁ r₁
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_exists {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) (param : V) {p : V} :
                                                              L.IsUFormula p∃ (y : V), c.Graph param p y
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.graph_unique {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {p : V} :
                                                              L.IsUFormula p∀ {param r r' : V}, c.Graph param p rc.Graph param p r'r = r'
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.exists_unique {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) (param : V) {p : V} (hp : L.IsUFormula p) :
                                                              ∃! r : V, c.Graph param p r
                                                              theorem LO.Arith.Language.UformulaRec1.Construction.exists_unique_all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) (param p : V) :
                                                              ∃! r : V, (L.IsUFormula pc.Graph param p r) (¬L.IsUFormula pr = 0)
                                                              def LO.Arith.Language.UformulaRec1.Construction.result {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) (param p : V) :
                                                              V
                                                              Equations
                                                              Instances For
                                                                theorem LO.Arith.Language.UformulaRec1.Construction.result_prop {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) (param : V) {p : V} (hp : L.IsUFormula p) :
                                                                c.Graph param p (c.result param p)
                                                                theorem LO.Arith.Language.UformulaRec1.Construction.result_prop_not {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) (param : V) {p : V} (hp : ¬L.IsUFormula p) :
                                                                c.result param p = 0
                                                                theorem LO.Arith.Language.UformulaRec1.Construction.result_eq_of_graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p r : V} (h : c.Graph param p r) :
                                                                c.result param p = r
                                                                @[simp]
                                                                theorem LO.Arith.Language.UformulaRec1.Construction.result_rel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                                                                c.result param (qqRel k R v) = c.rel param k R v
                                                                @[simp]
                                                                theorem LO.Arith.Language.UformulaRec1.Construction.result_nrel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                                                                c.result param (qqNRel k R v) = c.nrel param k R v
                                                                @[simp]
                                                                theorem LO.Arith.Language.UformulaRec1.Construction.result_verum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param : V} :
                                                                c.result param qqVerum = c.verum param
                                                                @[simp]
                                                                theorem LO.Arith.Language.UformulaRec1.Construction.result_falsum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param : V} :
                                                                c.result param qqFalsum = c.falsum param
                                                                @[simp]
                                                                theorem LO.Arith.Language.UformulaRec1.Construction.result_and {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                                                                c.result param (qqAnd p q) = c.and param p q (c.result param p) (c.result param q)
                                                                @[simp]
                                                                theorem LO.Arith.Language.UformulaRec1.Construction.result_or {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                                                                c.result param (qqOr p q) = c.or param p q (c.result param p) (c.result param q)
                                                                @[simp]
                                                                theorem LO.Arith.Language.UformulaRec1.Construction.result_all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p : V} (hp : L.IsUFormula p) :
                                                                c.result param (qqAll p) = c.all param p (c.result (c.allChanges param) p)
                                                                @[simp]
                                                                theorem LO.Arith.Language.UformulaRec1.Construction.result_ex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p : V} (hp : L.IsUFormula p) :
                                                                c.result param (qqEx p) = c.ex param p (c.result (c.exChanges param) p)
                                                                instance LO.Arith.Language.UformulaRec1.Construction.result_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) :
                                                                { Γ := 𝚺, rank := 0 + 1 }-Function₂ c.result
                                                                theorem LO.Arith.Language.UformulaRec1.Construction.uformula_result_induction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {P : VVVProp} (hP : 𝚺₁-Relation₃ P) (hRel : ∀ (param k R v : V), L.Rel k RL.IsUTermVec k vP param (qqRel k R v) (c.rel param k R v)) (hNRel : ∀ (param k R v : V), L.Rel k RL.IsUTermVec k vP param (qqNRel k R v) (c.nrel param k R v)) (hverum : ∀ (param : V), P param qqVerum (c.verum param)) (hfalsum : ∀ (param : V), P param qqFalsum (c.falsum param)) (hand : ∀ (param p q : V), L.IsUFormula pL.IsUFormula qP param p (c.result param p)P param q (c.result param q)P param (qqAnd p q) (c.and param p q (c.result param p) (c.result param q))) (hor : ∀ (param p q : V), L.IsUFormula pL.IsUFormula qP param p (c.result param p)P param q (c.result param q)P param (qqOr p q) (c.or param p q (c.result param p) (c.result param q))) (hall : ∀ (param p : V), L.IsUFormula pP (c.allChanges param) p (c.result (c.allChanges param) p)P param (qqAll p) (c.all param p (c.result (c.allChanges param) p))) (hex : ∀ (param p : V), L.IsUFormula pP (c.exChanges param) p (c.result (c.exChanges param) p)P param (qqEx p) (c.ex param p (c.result (c.exChanges param) p))) {param p : V} :
                                                                L.IsUFormula pP param p (c.result param p)
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    def LO.Arith.Language.bv {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : V) :
                                                                    V
                                                                    Equations
                                                                    Instances For
                                                                      def LO.FirstOrder.Arith.LDef.bvDef (pL : LDef) :
                                                                      𝚺₁.Semisentence 2
                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        instance LO.Arith.Language.bv_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {m : } (Γ : SigmaPiDelta) :
                                                                        { Γ := Γ, rank := m + 1 }-Function₁ L.bv
                                                                        @[simp]
                                                                        theorem LO.Arith.bv_rel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                                                                        L.bv (qqRel k R v) = listMax (L.termBVVec k v)
                                                                        @[simp]
                                                                        theorem LO.Arith.bv_nrel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                                                                        L.bv (qqNRel k R v) = listMax (L.termBVVec k v)
                                                                        @[simp]
                                                                        theorem LO.Arith.bv_verum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                                                                        L.bv qqVerum = 0
                                                                        @[simp]
                                                                        theorem LO.Arith.bv_falsum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                                                                        L.bv qqFalsum = 0
                                                                        @[simp]
                                                                        theorem LO.Arith.bv_and {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                                                                        L.bv (qqAnd p q) = L.bv p L.bv q
                                                                        @[simp]
                                                                        theorem LO.Arith.bv_or {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                                                                        L.bv (qqOr p q) = L.bv p L.bv q
                                                                        @[simp]
                                                                        theorem LO.Arith.bv_all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :
                                                                        L.bv (qqAll p) = L.bv p - 1
                                                                        @[simp]
                                                                        theorem LO.Arith.bv_ex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :
                                                                        L.bv (qqEx p) = L.bv p - 1
                                                                        theorem LO.Arith.bv_eq_of_not_isUFormula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (h : ¬L.IsUFormula p) :
                                                                        L.bv p = 0
                                                                        structure LO.Arith.Language.IsSemiformula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n p : V) :
                                                                        • isUFormula : L.IsUFormula p
                                                                        • bv : L.bv p n
                                                                        Instances For
                                                                          @[reducible, inline]
                                                                          abbrev LO.Arith.Language.IsFormula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : V) :
                                                                          Equations
                                                                          • L.IsFormula p = L.IsSemiformula 0 p
                                                                          Instances For
                                                                            theorem LO.Arith.Language.isSemiformula_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} :
                                                                            L.IsSemiformula n p L.IsUFormula p L.bv p n
                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              theorem LO.Arith.Language.isSemiformula_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
                                                                              𝚫₁-Relation L.IsSemiformula via pL.isSemiformulaDef
                                                                              instance LO.Arith.Language.isSemiformulaDef_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : } :
                                                                              { Γ := Γ, rank := m + 1 }-Relation L.IsSemiformula
                                                                              @[simp]
                                                                              theorem LO.Arith.Language.IsUFormula.isSemiformula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (h : L.IsUFormula p) :
                                                                              L.IsSemiformula (L.bv p) p
                                                                              @[simp]
                                                                              theorem LO.Arith.Language.IsSemiformula.rel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n k r v : V} :
                                                                              L.IsSemiformula n (qqRel k r v) L.Rel k r L.IsSemitermVec k n v
                                                                              @[simp]
                                                                              theorem LO.Arith.Language.IsSemiformula.nrel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n k r v : V} :
                                                                              L.IsSemiformula n (qqNRel k r v) L.Rel k r L.IsSemitermVec k n v
                                                                              @[simp]
                                                                              theorem LO.Arith.Language.IsSemiformula.verum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} :
                                                                              L.IsSemiformula n qqVerum
                                                                              @[simp]
                                                                              theorem LO.Arith.Language.IsSemiformula.falsum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} :
                                                                              L.IsSemiformula n qqFalsum
                                                                              @[simp]
                                                                              theorem LO.Arith.Language.IsSemiformula.and {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p q : V} :
                                                                              L.IsSemiformula n (qqAnd p q) L.IsSemiformula n p L.IsSemiformula n q
                                                                              @[simp]
                                                                              theorem LO.Arith.Language.IsSemiformula.or {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p q : V} :
                                                                              L.IsSemiformula n (qqOr p q) L.IsSemiformula n p L.IsSemiformula n q
                                                                              @[simp]
                                                                              theorem LO.Arith.Language.IsSemiformula.all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} :
                                                                              L.IsSemiformula n (qqAll p) L.IsSemiformula (n + 1) p
                                                                              @[simp]
                                                                              theorem LO.Arith.Language.IsSemiformula.ex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} :
                                                                              L.IsSemiformula n (qqEx p) L.IsSemiformula (n + 1) p
                                                                              theorem LO.Arith.Language.IsSemiformula.case_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} :
                                                                              L.IsSemiformula n p (∃ (k : V) (R : V) (v : V), L.Rel k R L.IsSemitermVec k n v p = qqRel k R v) (∃ (k : V) (R : V) (v : V), L.Rel k R L.IsSemitermVec k n v p = qqNRel k R v) p = qqVerum p = qqFalsum (∃ (p₁ : V) (p₂ : V), L.IsSemiformula n p₁ L.IsSemiformula n p₂ p = qqAnd p₁ p₂) (∃ (p₁ : V) (p₂ : V), L.IsSemiformula n p₁ L.IsSemiformula n p₂ p = qqOr p₁ p₂) (∃ (p₁ : V), L.IsSemiformula (n + 1) p₁ p = qqAll p₁) ∃ (p₁ : V), L.IsSemiformula (n + 1) p₁ p = qqEx p₁
                                                                              theorem LO.Arith.Language.IsSemiformula.case {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {P : VVProp} {n p : V} (hp : L.IsSemiformula n p) (hrel : ∀ (n k r v : V), L.Rel k rL.IsSemitermVec k n vP n (qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k rL.IsSemitermVec k n vP n (qqNRel k r v)) (hverum : ∀ (n : V), P n qqVerum) (hfalsum : ∀ (n : V), P n qqFalsum) (hand : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n (qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n (qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) pP n (qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) pP n (qqEx p)) :
                                                                              P n p
                                                                              theorem LO.Arith.Language.IsSemiformula.induction_sigma1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {P : VVProp} (hP : 𝚺₁-Relation P) (hrel : ∀ (n k r v : V), L.Rel k rL.IsSemitermVec k n vP n (qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k rL.IsSemitermVec k n vP n (qqNRel k r v)) (hverum : ∀ (n : V), P n qqVerum) (hfalsum : ∀ (n : V), P n qqFalsum) (hand : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n pP n qP n (qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n pP n qP n (qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) pP (n + 1) pP n (qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) pP (n + 1) pP n (qqEx p)) {n p : V} :
                                                                              L.IsSemiformula n pP n p
                                                                              theorem LO.Arith.Language.IsSemiformula.induction_pi1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {P : VVProp} (hP : 𝚷₁-Relation P) (hrel : ∀ (n k r v : V), L.Rel k rL.IsSemitermVec k n vP n (qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k rL.IsSemitermVec k n vP n (qqNRel k r v)) (hverum : ∀ (n : V), P n qqVerum) (hfalsum : ∀ (n : V), P n qqFalsum) (hand : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n pP n qP n (qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n pP n qP n (qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) pP (n + 1) pP n (qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) pP (n + 1) pP n (qqEx p)) {n p : V} :
                                                                              L.IsSemiformula n pP n p
                                                                              theorem LO.Arith.Language.IsSemiformula.induction1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (Γ : SigmaPiDelta) {P : VVProp} (hP : { Γ := Γ, rank := 1 }-Relation P) (hrel : ∀ (n k r v : V), L.Rel k rL.IsSemitermVec k n vP n (qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k rL.IsSemitermVec k n vP n (qqNRel k r v)) (hverum : ∀ (n : V), P n qqVerum) (hfalsum : ∀ (n : V), P n qqFalsum) (hand : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n pP n qP n (qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n pP n qP n (qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) pP (n + 1) pP n (qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) pP (n + 1) pP n (qqEx p)) {n p : V} :
                                                                              L.IsSemiformula n pP n p
                                                                              theorem LO.Arith.Language.IsSemiformula.pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} (h : L.IsSemiformula n p) :
                                                                              0 < p
                                                                              @[simp]
                                                                              theorem LO.Arith.Language.IsSemiformula.not_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (m : V) :
                                                                              ¬L.IsSemiformula m 0
                                                                              theorem LO.Arith.Language.UformulaRec1.Construction.semiformula_result_induction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} {c : Construction V L β} {P : VVVVProp} (hP : 𝚺₁-Relation₄ P) (hRel : ∀ (n param k R v : V), L.Rel k RL.IsSemitermVec k n vP param n (qqRel k R v) (c.rel param k R v)) (hNRel : ∀ (n param k R v : V), L.Rel k RL.IsSemitermVec k n vP param n (qqNRel k R v) (c.nrel param k R v)) (hverum : ∀ (n param : V), P param n qqVerum (c.verum param)) (hfalsum : ∀ (n param : V), P param n qqFalsum (c.falsum param)) (hand : ∀ (n param p q : V), L.IsSemiformula n pL.IsSemiformula n qP param n p (c.result param p)P param n q (c.result param q)P param n (qqAnd p q) (c.and param p q (c.result param p) (c.result param q))) (hor : ∀ (n param p q : V), L.IsSemiformula n pL.IsSemiformula n qP param n p (c.result param p)P param n q (c.result param q)P param n (qqOr p q) (c.or param p q (c.result param p) (c.result param q))) (hall : ∀ (n param p : V), L.IsSemiformula (n + 1) pP (c.allChanges param) (n + 1) p (c.result (c.allChanges param) p)P param n (qqAll p) (c.all param p (c.result (c.allChanges param) p))) (hex : ∀ (n param p : V), L.IsSemiformula (n + 1) pP (c.exChanges param) (n + 1) p (c.result (c.exChanges param) p)P param n (qqEx p) (c.ex param p (c.result (c.exChanges param) p))) {param n p : V} :
                                                                              L.IsSemiformula n pP param n p (c.result param p)