Documentation

Arithmetization.ISigmaOne.Metamath.Proof.Typed

Typed Formalized Tait-Calculus #

@[reducible, inline]
abbrev LO.Arith.Language.Semiformula.substs₁ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1)) (t : L.Term) :
L.Formula
Equations
Instances For
    @[reducible, inline]
    abbrev LO.Arith.Language.Semiformula.free {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1)) :
    L.Formula
    Equations
    • p.free = p.shift.substs₁ (L.fvar 0)
    Instances For
      @[simp]
      theorem LO.Arith.Language.Semiformula.val_substs₁ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1)) (t : L.Term) :
      (p.substs₁ t).val = L.substs ?[t.val] p.val
      @[simp]
      theorem LO.Arith.Language.Semiformula.val_free {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1)) :
      p.free.val = L.substs ?[LO.Arith.qqFvar 0] (L.shift p.val)
      @[simp]
      theorem LO.Arith.substs₁_neg {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1)) (t : L.Term) :
      (p).substs₁ t = p.substs₁ t
      @[simp]
      theorem LO.Arith.substs₁_all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1 + 1)) (t : L.Term) :
      p.all.substs₁ t = p^/[(LO.Arith.Language.Semiterm.sing t).q].all
      @[simp]
      theorem LO.Arith.substs₁_ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1 + 1)) (t : L.Term) :
      p.ex.substs₁ t = p^/[(LO.Arith.Language.Semiterm.sing t).q].ex
      @[reducible, inline]
      abbrev LO.Arith.Language.Theory.tmem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Formula) (T : L.Theory) :
      Equations
      Instances For
        structure LO.Arith.Language.Sequent {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
        Type u_1
        • val : V
        • val_formulaSet : L.IsFormulaSet self.val
        Instances For
          @[simp]
          theorem LO.Arith.Language.Sequent.val_formulaSet {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (self : L.Sequent) :
          L.IsFormulaSet self.val
          Equations
          • LO.Arith.instEmptyCollectionSequent = { emptyCollection := { val := , val_formulaSet := } }
          instance LO.Arith.instSingletonFormulaSequent {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
          Singleton L.Formula L.Sequent
          Equations
          • LO.Arith.instSingletonFormulaSequent = { singleton := fun (p : L.Formula) => { val := {p.val}, val_formulaSet := } }
          instance LO.Arith.instInsertFormulaSequent {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
          Insert L.Formula L.Sequent
          Equations
          • LO.Arith.instInsertFormulaSequent = { insert := fun (p : L.Formula) (Γ : L.Sequent) => { val := insert p.val Γ.val, val_formulaSet := } }
          instance LO.Arith.instUnionSequent {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
          Union L.Sequent
          Equations
          • LO.Arith.instUnionSequent = { union := fun (Γ Δ : L.Sequent) => { val := Γ.val Δ.val, val_formulaSet := } }
          instance LO.Arith.instMembershipFormulaSequent {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
          Membership L.Formula L.Sequent
          Equations
          • LO.Arith.instMembershipFormulaSequent = { mem := fun (x : L.Formula) (x_1 : L.Sequent) => x.val x_1.val }
          Equations
          • LO.Arith.instHasSubsetSequent = { Subset := fun (x x_1 : L.Sequent) => x.val x_1.val }
          theorem LO.Arith.Language.Sequent.mem_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : L.Sequent} {p : L.Formula} :
          p Γ p.val Γ.val
          theorem LO.Arith.Language.Sequent.subset_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : L.Sequent} {Δ : L.Sequent} :
          Γ Δ Γ.val Δ.val
          @[simp]
          theorem LO.Arith.Language.Sequent.val_singleton {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Formula) :
          {p}.val = {p.val}
          @[simp]
          theorem LO.Arith.Language.Sequent.val_insert {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Formula) (Γ : L.Sequent) :
          (insert p Γ).val = insert p.val Γ.val
          @[simp]
          theorem LO.Arith.Language.Sequent.val_union {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (Γ : L.Sequent) (Δ : L.Sequent) :
          (Γ Δ).val = Γ.val Δ.val
          @[simp]
          theorem LO.Arith.Language.Sequent.not_mem_empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Formula) :
          p
          @[simp]
          theorem LO.Arith.Language.Sequent.mem_singleton_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : L.Formula} {q : L.Formula} :
          p {q} p = q
          @[simp]
          theorem LO.Arith.Language.Sequent.mem_insert_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : L.Sequent} {p : L.Formula} {q : L.Formula} :
          p insert q Γ p = q p Γ
          @[simp]
          theorem LO.Arith.Language.Sequent.mem_union_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : L.Sequent} {Δ : L.Sequent} {p : L.Formula} :
          p Γ Δ p Γ p Δ
          theorem LO.Arith.Language.Sequent.ext {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : L.Sequent} {Δ : L.Sequent} (h : ∀ (x : L.Formula), x Γ x Δ) :
          Γ = Δ
          theorem LO.Arith.Language.Sequent.ext' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : L.Sequent} {Δ : L.Sequent} (h : Γ.val = Δ.val) :
          Γ = Δ
          def LO.Arith.Language.Sequent.shift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (s : L.Sequent) :
          L.Sequent
          Equations
          • s.shift = { val := L.setShift s.val, val_formulaSet := }
          Instances For
            @[simp]
            theorem LO.Arith.Language.Sequent.shift_insert {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : L.Sequent} {p : L.Formula} :
            structure LO.Arith.Language.TTheory {V : Type u_1} [LO.ORingStruc V] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
            Type u_1
            • thy : L.Theory
            • pthy : pL.TDef
            • defined : self.thy.Defined self.pthy
            Instances For
              instance LO.Arith.instDefinedThyPthy {V : Type u_1} [LO.ORingStruc V] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.TTheory) :
              T.thy.Defined T.pthy
              Equations
              structure LO.Arith.Language.Theory.TDerivation {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.TTheory) (Γ : L.Sequent) :
              Type u_1
              • derivation : V
              • derivationOf : T.thy.DerivationOf self.derivation Γ.val
              Instances For
                theorem LO.Arith.Language.Theory.TDerivation.derivationOf {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} (self : LO.Arith.Language.Theory.TDerivation T Γ) :
                T.thy.DerivationOf self.derivation Γ.val
                def LO.Arith.Language.Theory.TProof {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.TTheory) (p : L.Formula) :
                Type u_1
                Equations
                Instances For
                  instance LO.Arith.instSystemFormulaTTheory {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                  LO.System L.Formula L.TTheory
                  Equations
                  • LO.Arith.instSystemFormulaTTheory = { Prf := LO.Arith.Language.Theory.TProof }
                  instance LO.Arith.instHasSubsetTTheory {V : Type u_1} [LO.ORingStruc V] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :
                  HasSubset L.TTheory
                  Equations
                  • LO.Arith.instHasSubsetTTheory = { Subset := fun (T U : L.TTheory) => T.thy U.thy }
                  def LO.Arith.Language.Theory.Derivable.toTDerivation {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (Γ : L.Sequent) (h : T.thy.Derivable Γ.val) :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem LO.Arith.Language.Theory.TDerivation.toDerivable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} (d : LO.Arith.Language.Theory.TDerivation T Γ) :
                    T.thy.Derivable Γ.val
                    theorem LO.Arith.Language.Theory.TProvable.iff_provable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {σ : L.Formula} :
                    T ⊢! σ T.thy.Provable σ.val
                    Equations
                    • d.toTProof = d
                    Instances For
                      def LO.Arith.Language.Theory.TDerivation.and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p : L.Formula} {q : L.Formula} (dp : LO.Arith.Language.Theory.TDerivation T (insert p Γ)) (dq : LO.Arith.Language.Theory.TDerivation T (insert q Γ)) :
                      Equations
                      Instances For
                        def LO.Arith.Language.Theory.TDerivation.or {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p : L.Formula} {q : L.Formula} (dpq : LO.Arith.Language.Theory.TDerivation T (insert p (insert q Γ))) :
                        Equations
                        Instances For
                          def LO.Arith.Language.Theory.TDerivation.all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p : L.Semiformula (0 + 1)} (dp : LO.Arith.Language.Theory.TDerivation T (insert p.free Γ.shift)) :
                          Equations
                          Instances For
                            def LO.Arith.Language.Theory.TDerivation.ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p : L.Semiformula (0 + 1)} (t : L.Term) (dp : LO.Arith.Language.Theory.TDerivation T (insert (p.substs₁ t) Γ)) :
                            Equations
                            Instances For
                              def LO.Arith.Language.Theory.TDerivation.wk {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {Δ : L.Sequent} (d : LO.Arith.Language.Theory.TDerivation T Δ) (h : Δ Γ) :
                              Equations
                              Instances For
                                Equations
                                Instances For
                                  def LO.Arith.Language.Theory.TDerivation.ofSubset {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {U : L.TTheory} {Γ : L.Sequent} (h : T U) (d : LO.Arith.Language.Theory.TDerivation T Γ) :
                                  Equations
                                  Instances For
                                    def LO.Arith.Language.Theory.TDerivation.cut' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {Δ : L.Sequent} {p : L.Formula} (d₁ : LO.Arith.Language.Theory.TDerivation T (insert p Γ)) (d₂ : LO.Arith.Language.Theory.TDerivation T (insert (p) Δ)) :
                                    Equations
                                    • d₁.cut' d₂ = (d₁.wk ).cut (d₂.wk )
                                    Instances For
                                      def LO.Arith.Language.Theory.TDerivation.conj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} (ps : LO.Arith.Language.SemiformulaVec 0) (ds : (i : V) → (hi : i < LO.Arith.len ps.val) → LO.Arith.Language.Theory.TDerivation T (insert (ps.nth i hi) Γ)) :
                                      Equations
                                      Instances For
                                        def LO.Arith.Language.Theory.TDerivation.disj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} (ps : LO.Arith.Language.SemiformulaVec 0) {i : V} (hi : i < LO.Arith.len ps.val) (d : LO.Arith.Language.Theory.TDerivation T (insert (ps.nth i hi) Γ)) :
                                        Equations
                                        Instances For
                                          def LO.Arith.Language.Theory.TDerivation.modusPonens {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p : L.Formula} {q : L.Formula} (dpq : LO.Arith.Language.Theory.TDerivation T (insert (p q) Γ)) (dp : LO.Arith.Language.Theory.TDerivation T (insert p Γ)) :
                                          Equations
                                          Instances For
                                            def LO.Arith.Language.Theory.TDerivation.ofEq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {Δ : L.Sequent} (d : LO.Arith.Language.Theory.TDerivation T Γ) (h : Γ = Δ) :
                                            Equations
                                            • d.ofEq h = hd
                                            Instances For
                                              def LO.Arith.Language.Theory.TDerivation.rotate₁ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p₀ : L.Formula} {p₁ : L.Formula} (d : LO.Arith.Language.Theory.TDerivation T (insert p₀ (insert p₁ Γ))) :
                                              Equations
                                              • d.rotate₁ = d.ofEq
                                              Instances For
                                                def LO.Arith.Language.Theory.TDerivation.rotate₂ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p₀ : L.Formula} {p₁ : L.Formula} {p₂ : L.Formula} (d : LO.Arith.Language.Theory.TDerivation T (insert p₀ (insert p₁ (insert p₂ Γ)))) :
                                                Equations
                                                • d.rotate₂ = d.ofEq
                                                Instances For
                                                  def LO.Arith.Language.Theory.TDerivation.rotate₃ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p₀ : L.Formula} {p₁ : L.Formula} {p₂ : L.Formula} {p₃ : L.Formula} (d : LO.Arith.Language.Theory.TDerivation T (insert p₀ (insert p₁ (insert p₂ (insert p₃ Γ))))) :
                                                  Equations
                                                  • d.rotate₃ = d.ofEq
                                                  Instances For
                                                    def LO.Arith.Language.Theory.TDerivation.orInv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p : L.Formula} {q : L.Formula} (d : LO.Arith.Language.Theory.TDerivation T (insert (p q) Γ)) :
                                                    Equations
                                                    Instances For
                                                      def LO.Arith.Language.Theory.TDerivation.specialize {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p : L.Semiformula (0 + 1)} (b : LO.Arith.Language.Theory.TDerivation T (insert p.all Γ)) (t : L.Term) :
                                                      Equations
                                                      Instances For
                                                        def LO.Arith.Language.Theory.TProof.modusPonens {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Formula} {q : L.Formula} (d : T p q) (b : T p) :
                                                        T q

                                                        Condition D2

                                                        Equations
                                                        Instances For
                                                          def LO.Arith.Language.Theory.TProof.ofSubset {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {U : L.TTheory} (h : T U) {p : L.Formula} :
                                                          T pU p
                                                          Equations
                                                          Instances For
                                                            theorem LO.Arith.Language.Theory.TProof.of_subset {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {U : L.TTheory} (h : T U) {p : L.Formula} :
                                                            T ⊢! pU ⊢! p
                                                            Equations
                                                            • LO.Arith.Language.Theory.TProof.instModusPonensTTheoryFormula = { mdp := fun {p q : L.Formula} => LO.Arith.Language.Theory.TProof.modusPonens }
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Equations
                                                            • LO.Arith.Language.Theory.TProof.instMinimalTTheoryFormula = LO.System.Minimal.mk
                                                            Equations
                                                            • LO.Arith.Language.Theory.TProof.instClassicalTTheoryFormula = LO.System.Classical.mk
                                                            def LO.Arith.Language.Theory.TProof.exIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (p : L.Semiformula (0 + 1)) (t : L.Term) (b : T p.substs₁ t) :
                                                            T p.ex
                                                            Equations
                                                            Instances For
                                                              theorem LO.Arith.Language.Theory.TProof.ex_intro! {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (p : L.Semiformula (0 + 1)) (t : L.Term) (b : T ⊢! p.substs₁ t) :
                                                              T ⊢! p.ex
                                                              def LO.Arith.Language.Theory.TProof.specialize {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Semiformula (0 + 1)} (b : T p.all) (t : L.Term) :
                                                              T p.substs₁ t
                                                              Equations
                                                              Instances For
                                                                theorem LO.Arith.Language.Theory.TProof.specialize! {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Semiformula (0 + 1)} (b : T ⊢! p.all) (t : L.Term) :
                                                                T ⊢! p.substs₁ t
                                                                def LO.Arith.Language.Theory.TProof.conj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (ps : LO.Arith.Language.SemiformulaVec 0) (ds : (i : V) → (hi : i < LO.Arith.len ps.val) → T ps.nth i hi) :
                                                                T ps.conj
                                                                Equations
                                                                Instances For
                                                                  theorem LO.Arith.Language.Theory.TProof.conj! {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (ps : LO.Arith.Language.SemiformulaVec 0) (ds : ∀ (i : V) (hi : i < LO.Arith.len ps.val), T ⊢! ps.nth i hi) :
                                                                  T ⊢! ps.conj
                                                                  def LO.Arith.Language.Theory.TProof.conj' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (ps : LO.Arith.Language.SemiformulaVec 0) (ds : (i : V) → (hi : i < LO.Arith.len ps.val) → T ps.nth (LO.Arith.len ps.val - (i + 1)) ) :
                                                                  T ps.conj
                                                                  Equations
                                                                  Instances For
                                                                    def LO.Arith.Language.Theory.TProof.conjOr' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (ps : LO.Arith.Language.SemiformulaVec 0) (q : L.Semiformula 0) (ds : (i : V) → (hi : i < LO.Arith.len ps.val) → T ps.nth (LO.Arith.len ps.val - (i + 1)) q) :
                                                                    T ps.conj q
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      def LO.Arith.Language.Theory.TProof.disj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (ps : LO.Arith.Language.SemiformulaVec 0) {i : V} (hi : i < LO.Arith.len ps.val) (d : T ps.nth i hi) :
                                                                      T ps.disj
                                                                      Equations
                                                                      Instances For
                                                                        theorem LO.Arith.Language.Theory.TProof.shift! {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Formula} (d : T ⊢! p) :
                                                                        def LO.Arith.Language.Theory.TProof.all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Semiformula (0 + 1)} (dp : T p.free) :
                                                                        T p.all
                                                                        Equations
                                                                        Instances For
                                                                          theorem LO.Arith.Language.Theory.TProof.all! {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Semiformula (0 + 1)} (dp : T ⊢! p.free) :
                                                                          T ⊢! p.all
                                                                          def LO.Arith.Language.Theory.TProof.generalizeAux {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {C : L.Formula} {p : L.Semiformula (0 + 1)} (dp : T LO.Arith.Language.Semiformula.shift C p.free) :
                                                                          T C p.all
                                                                          Equations
                                                                          Instances For
                                                                            theorem LO.Arith.Language.Theory.TProof.conj_shift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (Γ : List L.Formula) :
                                                                            LO.Arith.Language.Semiformula.shift (Γ) = List.map LO.Arith.Language.Semiformula.shift Γ
                                                                            def LO.Arith.Language.Theory.TProof.generalize {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : List (L.Semiformula 0)} {p : L.Semiformula (0 + 1)} (d : List.map LO.Arith.Language.Semiformula.shift Γ ⊢[T] p.free) :
                                                                            Γ ⊢[T] p.all
                                                                            Equations
                                                                            Instances For
                                                                              theorem LO.Arith.Language.Theory.TProof.generalize! {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : List (L.Semiformula 0)} {p : L.Semiformula (0 + 1)} (d : List.map LO.Arith.Language.Semiformula.shift Γ ⊢[T]! p.free) :
                                                                              Γ ⊢[T]! p.all
                                                                              def LO.Arith.Language.Theory.TProof.specializeWithCtxAux {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {C : L.Formula} {p : L.Semiformula (0 + 1)} (d : T C p.all) (t : L.Term) :
                                                                              T C p.substs₁ t
                                                                              Equations
                                                                              Instances For
                                                                                def LO.Arith.Language.Theory.TProof.specializeWithCtx {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : List (L.Semiformula 0)} {p : L.Semiformula (0 + 1)} (d : Γ ⊢[T] p.all) (t : L.Term) :
                                                                                Γ ⊢[T] p.substs₁ t
                                                                                Equations
                                                                                Instances For
                                                                                  theorem LO.Arith.Language.Theory.TProof.specialize_with_ctx! {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : List (L.Semiformula 0)} {p : L.Semiformula (0 + 1)} (d : Γ ⊢[T]! p.all) (t : L.Term) :
                                                                                  Γ ⊢[T]! p.substs₁ t
                                                                                  def LO.Arith.Language.Theory.TProof.ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Semiformula (0 + 1)} (t : L.Term) (dp : T p.substs₁ t) :
                                                                                  T p.ex
                                                                                  Equations
                                                                                  Instances For
                                                                                    theorem LO.Arith.Language.Theory.TProof.ex! {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Semiformula (0 + 1)} (t : L.Term) (dp : T ⊢! p.substs₁ t) :
                                                                                    T ⊢! p.ex