Documentation

Arithmetization.ISigmaOne.Metamath.Formula.Basic

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

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

                                            theorem LO.Arith.Language.IsUFormula.case {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.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 = LO.Arith.qqRel k R v) (∃ (k : V) (R : V) (v : V), L.Rel k R L.IsUTermVec k v p = LO.Arith.qqNRel k R v) p = LO.Arith.qqVerum p = LO.Arith.qqFalsum (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ L.IsUFormula p₂ p = LO.Arith.qqAnd p₁ p₂) (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ L.IsUFormula p₂ p = LO.Arith.qqOr p₁ p₂) (∃ (p₁ : V), L.IsUFormula p₁ p = LO.Arith.qqAll p₁) ∃ (p₁ : V), L.IsUFormula p₁ p = LO.Arith.qqEx p₁

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

                                            @[simp]
                                            theorem LO.Arith.Language.IsUFormula.rel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {r : V} {v : V} :
                                            L.IsUFormula (LO.Arith.qqRel k r v) L.Rel k r L.IsUTermVec k v
                                            @[simp]
                                            theorem LO.Arith.Language.IsUFormula.nrel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {r : V} {v : V} :
                                            L.IsUFormula (LO.Arith.qqNRel k r v) L.Rel k r L.IsUTermVec k v
                                            @[simp]
                                            theorem LO.Arith.Language.IsUFormula.verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                                            L.IsUFormula LO.Arith.qqVerum
                                            @[simp]
                                            theorem LO.Arith.Language.IsUFormula.falsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                                            L.IsUFormula LO.Arith.qqFalsum
                                            @[simp]
                                            theorem LO.Arith.Language.IsUFormula.and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} :
                                            L.IsUFormula (LO.Arith.qqAnd p q) L.IsUFormula p L.IsUFormula q
                                            @[simp]
                                            theorem LO.Arith.Language.IsUFormula.or {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} :
                                            L.IsUFormula (LO.Arith.qqOr p q) L.IsUFormula p L.IsUFormula q
                                            @[simp]
                                            theorem LO.Arith.Language.IsUFormula.all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
                                            L.IsUFormula (LO.Arith.qqAll p) L.IsUFormula p
                                            @[simp]
                                            theorem LO.Arith.Language.IsUFormula.ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
                                            L.IsUFormula (LO.Arith.qqEx p) L.IsUFormula p
                                            theorem LO.Arith.Language.IsUFormula.pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                                            ¬L.IsUFormula 0
                                            theorem LO.Arith.Language.IsUFormula.induction1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (Γ : LO.SigmaPiDelta) {P : VProp} (hP : { Γ := Γ, rank := 1 }-Predicate P) (hrel : ∀ (k r v : V), L.Rel k rL.IsUTermVec k vP (LO.Arith.qqRel k r v)) (hnrel : ∀ (k r v : V), L.Rel k rL.IsUTermVec k vP (LO.Arith.qqNRel k r v)) (hverum : P LO.Arith.qqVerum) (hfalsum : P LO.Arith.qqFalsum) (hand : ∀ (p q : V), L.IsUFormula pL.IsUFormula qP pP qP (LO.Arith.qqAnd p q)) (hor : ∀ (p q : V), L.IsUFormula pL.IsUFormula qP pP qP (LO.Arith.qqOr p q)) (hall : ∀ (p : V), L.IsUFormula pP pP (LO.Arith.qqAll p)) (hex : ∀ (p : V), L.IsUFormula pP pP (LO.Arith.qqEx p)) (p : V) :
                                            L.IsUFormula pP p
                                            theorem LO.Arith.Language.IsUFormula.induction_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {P : VProp} (hP : 𝚺₁-Predicate P) (hrel : ∀ (k r v : V), L.Rel k rL.IsUTermVec k vP (LO.Arith.qqRel k r v)) (hnrel : ∀ (k r v : V), L.Rel k rL.IsUTermVec k vP (LO.Arith.qqNRel k r v)) (hverum : P LO.Arith.qqVerum) (hfalsum : P LO.Arith.qqFalsum) (hand : ∀ (p q : V), L.IsUFormula pL.IsUFormula qP pP qP (LO.Arith.qqAnd p q)) (hor : ∀ (p q : V), L.IsUFormula pL.IsUFormula qP pP qP (LO.Arith.qqOr p q)) (hall : ∀ (p : V), L.IsUFormula pP pP (LO.Arith.qqAll p)) (hex : ∀ (p : V), L.IsUFormula pP pP (LO.Arith.qqEx p)) (p : V) :
                                            L.IsUFormula pP p
                                            theorem LO.Arith.Language.IsUFormula.induction_pi1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {P : VProp} (hP : 𝚷₁-Predicate P) (hrel : ∀ (k r v : V), L.Rel k rL.IsUTermVec k vP (LO.Arith.qqRel k r v)) (hnrel : ∀ (k r v : V), L.Rel k rL.IsUTermVec k vP (LO.Arith.qqNRel k r v)) (hverum : P LO.Arith.qqVerum) (hfalsum : P LO.Arith.qqFalsum) (hand : ∀ (p q : V), L.IsUFormula pL.IsUFormula qP pP qP (LO.Arith.qqAnd p q)) (hor : ∀ (p q : V), L.IsUFormula pL.IsUFormula qP pP qP (LO.Arith.qqOr p q)) (hall : ∀ (p : V), L.IsUFormula pP pP (LO.Arith.qqAll p)) (hex : ∀ (p : V), L.IsUFormula pP pP (LO.Arith.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
                                                      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
                                                          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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} {c : LO.Arith.Language.UformulaRec1.Construction V L β} {param : V} {p : V} {y : V} :
                                                            c.Graph param p y L.IsUFormula p ((∃ (k : V) (R : V) (v : V), p = LO.Arith.qqRel k R v y = c.rel param k R v) (∃ (k : V) (R : V) (v : V), p = LO.Arith.qqNRel k R v y = c.nrel param k R v) p = LO.Arith.qqVerum y = c.verum param p = LO.Arith.qqFalsum y = c.falsum param (∃ (p₁ : V) (p₂ : V) (y₁ : V) (y₂ : V), c.Graph param p₁ y₁ c.Graph param p₂ y₂ p = LO.Arith.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 = LO.Arith.qqOr p₁ p₂ y = c.or param p₁ p₂ y₁ y₂) (∃ (p₁ : V) (y₁ : V), c.Graph (c.allChanges param) p₁ y₁ p = LO.Arith.qqAll p₁ y = c.all param p₁ y₁) ∃ (p₁ : V) (y₁ : V), c.Graph (c.exChanges param) p₁ y₁ p = LO.Arith.qqEx p₁ y = c.ex param p₁ y₁)
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.graph_dom_uformula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p : V} {r : V} :
                                                            c.Graph param p rL.IsUFormula p
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.graph_rel_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {k : V} {r : V} {v : V} {y : V} (hkr : L.Rel k r) (hv : L.IsUTermVec k v) :
                                                            c.Graph param (LO.Arith.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {k : V} {r : V} {v : V} {y : V} (hkr : L.Rel k r) (hv : L.IsUTermVec k v) :
                                                            c.Graph param (LO.Arith.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {y : V} :
                                                            c.Graph param LO.Arith.qqVerum y y = c.verum param
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.graph_falsum_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {y : V} :
                                                            c.Graph param LO.Arith.qqFalsum y y = c.falsum param
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.graph_rel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {k : V} {r : V} {v : V} (hkr : L.Rel k r) (hv : L.IsUTermVec k v) :
                                                            c.Graph param (LO.Arith.qqRel k r v) (c.rel param k r v)
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.graph_nrel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {k : V} {r : V} {v : V} (hkr : L.Rel k r) (hv : L.IsUTermVec k v) :
                                                            c.Graph param (LO.Arith.qqNRel k r v) (c.nrel param k r v)
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.graph_verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} :
                                                            c.Graph param LO.Arith.qqVerum (c.verum param)
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.graph_falsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} :
                                                            c.Graph param LO.Arith.qqFalsum (c.falsum param)
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.graph_and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {p₂ : V} {r₁ : V} {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 (LO.Arith.qqAnd p₁ p₂) (c.and param p₁ p₂ r₁ r₂)
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.graph_and_inv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {p₂ : V} {r : V} :
                                                            c.Graph param (LO.Arith.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {p₂ : V} {r₁ : V} {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 (LO.Arith.qqOr p₁ p₂) (c.or param p₁ p₂ r₁ r₂)
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.graph_or_inv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {p₂ : V} {r : V} :
                                                            c.Graph param (LO.Arith.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {r₁ : V} (hp₁ : L.IsUFormula p₁) (h₁ : c.Graph (c.allChanges param) p₁ r₁) :
                                                            c.Graph param (LO.Arith.qqAll p₁) (c.all param p₁ r₁)
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.graph_all_inv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {r : V} :
                                                            c.Graph param (LO.Arith.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {r₁ : V} (hp₁ : L.IsUFormula p₁) (h₁ : c.Graph (c.exChanges param) p₁ r₁) :
                                                            c.Graph param (LO.Arith.qqEx p₁) (c.ex param p₁ r₁)
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.graph_ex_inv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {r : V} :
                                                            c.Graph param (LO.Arith.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) (param : V) (p : V) :
                                                            ∃! r : V, (L.IsUFormula pc.Graph param p r) (¬L.IsUFormula pr = 0)
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.result_prop {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.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_eq_of_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p : V} {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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                                                            c.result param (LO.Arith.qqRel k R v) = c.rel param k R v
                                                            @[simp]
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.result_nrel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                                                            c.result param (LO.Arith.qqNRel k R v) = c.nrel param k R v
                                                            @[simp]
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.result_verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} :
                                                            c.result param LO.Arith.qqVerum = c.verum param
                                                            @[simp]
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.result_falsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} :
                                                            c.result param LO.Arith.qqFalsum = c.falsum param
                                                            @[simp]
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.result_and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                                                            c.result param (LO.Arith.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                                                            c.result param (LO.Arith.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p : V} (hp : L.IsUFormula p) :
                                                            c.result param (LO.Arith.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p : V} (hp : L.IsUFormula p) :
                                                            c.result param (LO.Arith.qqEx p) = c.ex param p (c.result (c.exChanges param) p)
                                                            theorem LO.Arith.Language.UformulaRec1.Construction.uformula_result_induction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {P : VVVProp} (hP : 𝚺₁-Relation₃ P) (hRel : ∀ (param k R v : V), L.Rel k RL.IsUTermVec k vP param (LO.Arith.qqRel k R v) (c.rel param k R v)) (hNRel : ∀ (param k R v : V), L.Rel k RL.IsUTermVec k vP param (LO.Arith.qqNRel k R v) (c.nrel param k R v)) (hverum : ∀ (param : V), P param LO.Arith.qqVerum (c.verum param)) (hfalsum : ∀ (param : V), P param LO.Arith.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 (LO.Arith.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 (LO.Arith.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 (LO.Arith.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 (LO.Arith.qqEx p) (c.ex param p (c.result (c.exChanges param) p))) {param : V} {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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : V) :
                                                                V
                                                                Equations
                                                                Instances For
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    instance LO.Arith.Language.bv_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {m : } (Γ : LO.SigmaPiDelta) :
                                                                    { Γ := Γ, rank := m + 1 }-Function₁ L.bv
                                                                    Equations
                                                                    • =
                                                                    @[simp]
                                                                    theorem LO.Arith.bv_rel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                                                                    L.bv (LO.Arith.qqRel k R v) = LO.Arith.listMax (L.termBVVec k v)
                                                                    @[simp]
                                                                    theorem LO.Arith.bv_nrel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
                                                                    L.bv (LO.Arith.qqNRel k R v) = LO.Arith.listMax (L.termBVVec k v)
                                                                    @[simp]
                                                                    theorem LO.Arith.bv_verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                                                                    L.bv LO.Arith.qqVerum = 0
                                                                    @[simp]
                                                                    theorem LO.Arith.bv_falsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                                                                    L.bv LO.Arith.qqFalsum = 0
                                                                    @[simp]
                                                                    theorem LO.Arith.bv_and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                                                                    L.bv (LO.Arith.qqAnd p q) = max (L.bv p) (L.bv q)
                                                                    @[simp]
                                                                    theorem LO.Arith.bv_or {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
                                                                    L.bv (LO.Arith.qqOr p q) = max (L.bv p) (L.bv q)
                                                                    @[simp]
                                                                    theorem LO.Arith.bv_all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :
                                                                    L.bv (LO.Arith.qqAll p) = L.bv p - 1
                                                                    @[simp]
                                                                    theorem LO.Arith.bv_ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :
                                                                    L.bv (LO.Arith.qqEx p) = L.bv p - 1
                                                                    theorem LO.Arith.bv_eq_of_not_isUFormula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (n : V) (p : V) :
                                                                    • isUFormula : L.IsUFormula p
                                                                    • bv : L.bv p n
                                                                    Instances For
                                                                      theorem LO.Arith.Language.IsSemiformula.isUFormula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} (self : L.IsSemiformula n p) :
                                                                      L.IsUFormula p
                                                                      theorem LO.Arith.Language.IsSemiformula.bv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} (self : L.IsSemiformula n p) :
                                                                      L.bv p n
                                                                      @[reducible, inline]
                                                                      Equations
                                                                      • L.IsFormula p = L.IsSemiformula 0 p
                                                                      Instances For
                                                                        theorem LO.Arith.Language.isSemiformula_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                                                                          𝚫₁-Relation L.IsSemiformula via pL.isSemiformulaDef
                                                                          Equations
                                                                          • =
                                                                          instance LO.Arith.Language.isSemiformulaDef_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : } :
                                                                          { Γ := Γ, rank := m + 1 }-Relation L.IsSemiformula
                                                                          Equations
                                                                          • =
                                                                          @[simp]
                                                                          theorem LO.Arith.Language.IsUFormula.isSemiformula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {k : V} {r : V} {v : V} :
                                                                          L.IsSemiformula n (LO.Arith.qqRel k r v) L.Rel k r L.IsSemitermVec k n v
                                                                          @[simp]
                                                                          theorem LO.Arith.Language.IsSemiformula.nrel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {k : V} {r : V} {v : V} :
                                                                          L.IsSemiformula n (LO.Arith.qqNRel k r v) L.Rel k r L.IsSemitermVec k n v
                                                                          @[simp]
                                                                          theorem LO.Arith.Language.IsSemiformula.verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} :
                                                                          L.IsSemiformula n LO.Arith.qqVerum
                                                                          @[simp]
                                                                          theorem LO.Arith.Language.IsSemiformula.falsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} :
                                                                          L.IsSemiformula n LO.Arith.qqFalsum
                                                                          @[simp]
                                                                          theorem LO.Arith.Language.IsSemiformula.and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} {q : V} :
                                                                          L.IsSemiformula n (LO.Arith.qqAnd p q) L.IsSemiformula n p L.IsSemiformula n q
                                                                          @[simp]
                                                                          theorem LO.Arith.Language.IsSemiformula.or {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} {q : V} :
                                                                          L.IsSemiformula n (LO.Arith.qqOr p q) L.IsSemiformula n p L.IsSemiformula n q
                                                                          @[simp]
                                                                          theorem LO.Arith.Language.IsSemiformula.all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} :
                                                                          L.IsSemiformula n (LO.Arith.qqAll p) L.IsSemiformula (n + 1) p
                                                                          @[simp]
                                                                          theorem LO.Arith.Language.IsSemiformula.ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} :
                                                                          L.IsSemiformula n (LO.Arith.qqEx p) L.IsSemiformula (n + 1) p
                                                                          theorem LO.Arith.Language.IsSemiformula.case_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} :
                                                                          L.IsSemiformula n p (∃ (k : V) (R : V) (v : V), L.Rel k R L.IsSemitermVec k n v p = LO.Arith.qqRel k R v) (∃ (k : V) (R : V) (v : V), L.Rel k R L.IsSemitermVec k n v p = LO.Arith.qqNRel k R v) p = LO.Arith.qqVerum p = LO.Arith.qqFalsum (∃ (p₁ : V) (p₂ : V), L.IsSemiformula n p₁ L.IsSemiformula n p₂ p = LO.Arith.qqAnd p₁ p₂) (∃ (p₁ : V) (p₂ : V), L.IsSemiformula n p₁ L.IsSemiformula n p₂ p = LO.Arith.qqOr p₁ p₂) (∃ (p₁ : V), L.IsSemiformula (n + 1) p₁ p = LO.Arith.qqAll p₁) ∃ (p₁ : V), L.IsSemiformula (n + 1) p₁ p = LO.Arith.qqEx p₁
                                                                          theorem LO.Arith.Language.IsSemiformula.case {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {P : VVProp} {n : V} {p : V} (hp : L.IsSemiformula n p) (hrel : ∀ (n k r v : V), L.Rel k rL.IsSemitermVec k n vP n (LO.Arith.qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k rL.IsSemitermVec k n vP n (LO.Arith.qqNRel k r v)) (hverum : ∀ (n : V), P n LO.Arith.qqVerum) (hfalsum : ∀ (n : V), P n LO.Arith.qqFalsum) (hand : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n (LO.Arith.qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n (LO.Arith.qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) pP n (LO.Arith.qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) pP n (LO.Arith.qqEx p)) :
                                                                          P n p
                                                                          theorem LO.Arith.Language.IsSemiformula.induction_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.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 (LO.Arith.qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k rL.IsSemitermVec k n vP n (LO.Arith.qqNRel k r v)) (hverum : ∀ (n : V), P n LO.Arith.qqVerum) (hfalsum : ∀ (n : V), P n LO.Arith.qqFalsum) (hand : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n pP n qP n (LO.Arith.qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n pP n qP n (LO.Arith.qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) pP (n + 1) pP n (LO.Arith.qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) pP (n + 1) pP n (LO.Arith.qqEx p)) {n : V} {p : V} :
                                                                          L.IsSemiformula n pP n p
                                                                          theorem LO.Arith.Language.IsSemiformula.induction_pi1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.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 (LO.Arith.qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k rL.IsSemitermVec k n vP n (LO.Arith.qqNRel k r v)) (hverum : ∀ (n : V), P n LO.Arith.qqVerum) (hfalsum : ∀ (n : V), P n LO.Arith.qqFalsum) (hand : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n pP n qP n (LO.Arith.qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n pP n qP n (LO.Arith.qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) pP (n + 1) pP n (LO.Arith.qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) pP (n + 1) pP n (LO.Arith.qqEx p)) {n : V} {p : V} :
                                                                          L.IsSemiformula n pP n p
                                                                          theorem LO.Arith.Language.IsSemiformula.induction1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (Γ : LO.SigmaPiDelta) {P : VVProp} (hP : { Γ := Γ, rank := 1 }-Relation P) (hrel : ∀ (n k r v : V), L.Rel k rL.IsSemitermVec k n vP n (LO.Arith.qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k rL.IsSemitermVec k n vP n (LO.Arith.qqNRel k r v)) (hverum : ∀ (n : V), P n LO.Arith.qqVerum) (hfalsum : ∀ (n : V), P n LO.Arith.qqFalsum) (hand : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n pP n qP n (LO.Arith.qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n pL.IsSemiformula n qP n pP n qP n (LO.Arith.qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) pP (n + 1) pP n (LO.Arith.qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) pP (n + 1) pP n (LO.Arith.qqEx p)) {n : V} {p : V} :
                                                                          L.IsSemiformula n pP n p
                                                                          theorem LO.Arith.Language.IsSemiformula.pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} (h : L.IsSemiformula n p) :
                                                                          0 < p
                                                                          @[simp]
                                                                          theorem LO.Arith.Language.IsSemiformula.not_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} {c : LO.Arith.Language.UformulaRec1.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 (LO.Arith.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 (LO.Arith.qqNRel k R v) (c.nrel param k R v)) (hverum : ∀ (n param : V), P param n LO.Arith.qqVerum (c.verum param)) (hfalsum : ∀ (n param : V), P param n LO.Arith.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 (LO.Arith.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 (LO.Arith.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 (LO.Arith.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 (LO.Arith.qqEx p) (c.ex param p (c.result (c.exChanges param) p))) {param : V} {n : V} {p : V} :
                                                                          L.IsSemiformula n pP param n p (c.result param p)