Documentation

Arithmetization.ISigmaOne.Metamath.Coding

theorem LO.FirstOrder.Semiterm.encode_eq_toNat {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] {n : } (t : LO.FirstOrder.Semiterm L ξ n) :
theorem LO.FirstOrder.Semiterm.toNat_func {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] {n : } {k : } (f : L.Func k) (v : Fin kLO.FirstOrder.Semiterm L ξ n) :
(LO.FirstOrder.Semiterm.func f v).toNat = Nat.pair 2 (Nat.pair k (Nat.pair (Encodable.encode f) (Matrix.vecToNat fun (i : Fin k) => (v i).toNat))) + 1
@[simp]
theorem LO.FirstOrder.Semiterm.encode_emb {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] {n : } (t : LO.FirstOrder.Semiterm L Empty n) :
Encodable.encode (LO.FirstOrder.Rew.emb t) = Encodable.encode t
theorem LO.FirstOrder.Semiformula.encode_eq_toNat {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] {ξ : Type u_1} [Encodable ξ] {n : } (p : LO.FirstOrder.Semiformula L ξ n) :
@[simp]
theorem LO.FirstOrder.Semiformula.encode_emb {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] {ξ : Type u_1} [Encodable ξ] {n : } (p : LO.FirstOrder.Semisentence L n) :
Encodable.encode (LO.FirstOrder.Rew.emb.hom p) = Encodable.encode p
theorem LO.FirstOrder.Semiformula.Operator.lt_eq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [L.LT] (t : LO.FirstOrder.Semiterm L ξ n) (u : LO.FirstOrder.Semiterm L ξ n) :
(“!!t < !!u) = LO.FirstOrder.Semiformula.rel op(<) ![t, u]
def LO.Arith.finArrowToVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } :
(Fin kV)V
Equations
Instances For

    quasi-quotation rather than Godel quotation

    Equations
    • LO.Arith.instGoedelQuoteForallFin_arithmetization = { quote := LO.Arith.finArrowToVec }
    @[simp]
    @[simp]
    theorem LO.Arith.quote_singleton {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) :
    ![a] = ?[a]
    @[simp]
    theorem LO.Arith.quote_doubleton {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) :
    ![a, b] = ?[a, b]
    @[simp]
    theorem LO.Arith.quote_matrix_empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 0V) :
    theorem LO.Arith.quote_matrix_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } (v : Fin (k + 1)V) :
    v = cons (v 0) fun (i : Fin k) => v i.succ
    @[simp]
    theorem LO.Arith.quote_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } (v : Fin kV) (a : V) :
    @[simp]
    theorem LO.Arith.quote_matrix_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } (v : Fin kV) (w : Fin kV) :
    @[simp]
    theorem LO.Arith.quote_lh {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } (v : Fin kV) :
    @[simp]
    theorem LO.Arith.quote_nth_fin {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } (v : Fin kV) (i : Fin k) :
    LO.Arith.nth v i = v i
    @[simp]
    theorem LO.Arith.quote_matrix_absolute {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } (v : Fin k) :
    v = fun (i : Fin k) => (v i)
    Equations
    • LO.Arith.instGoedelQuote_arithmetization = { quote := fun (x : α) => (Encodable.encode x) }
    @[simp]
    theorem LO.Arith.quote_nat {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : ) :
    n = n
    theorem LO.Arith.coe_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {α : Type u_2} [Encodable α] (x : α) :
    @[simp]
    theorem LO.Arith.quote_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {α : Type u_2} [Encodable α] (x : α) :
    @[simp]
    theorem LO.Arith.val_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {α : Type u_2} [Encodable α] {ξ : Type u_3} {n : } {e : Fin nV} {ε : ξV} (x : α) :
    @[simp]
    theorem LO.Arith.quote_inj_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {α : Type u_2} [Encodable α] {x : α} {y : α} :
    @[simp]
    theorem LO.FirstOrder.Semiterm.quote_zero (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : ) :
    LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Zero.zero ![] = 𝟎
    @[simp]
    theorem LO.FirstOrder.Semiterm.quote_one (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : ) :
    LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.One.one ![] = 𝟏
    @[simp]
    theorem LO.Arith.eq_fin_of_lt_nat {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : } {x : V} (hx : x < n) :
    ∃ (i : Fin n), x = i

    TODO: move

    @[simp]
    theorem LO.Arith.semiterm_codeIn {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } (t : LO.FirstOrder.SyntacticSemiterm L n) :
    (L.codeIn V).IsSemiterm n t
    @[simp]
    theorem LO.Arith.semitermVec_codeIn {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {k : } {n : } (v : Fin kLO.FirstOrder.SyntacticSemiterm L n) :
    (L.codeIn V).IsSemitermVec k n fun (i : Fin k) => v i
    @[simp]
    theorem LO.Arith.isUTermVec_codeIn {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {k : } {n : } (v : Fin kLO.FirstOrder.SyntacticSemiterm L n) :
    (L.codeIn V).IsUTermVec k fun (i : Fin k) => v i
    @[simp]
    theorem LO.Arith.quote_termSubst {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } {m : } (t : LO.FirstOrder.SyntacticSemiterm L n) (w : Fin nLO.FirstOrder.SyntacticSemiterm L m) :
    (LO.FirstOrder.Rew.substs w) t = (L.codeIn V).termSubst fun (i : Fin n) => w i t
    theorem LO.Arith.quote_termSubstVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {k : } {n : } {m : } (w : Fin nLO.FirstOrder.SyntacticSemiterm L m) (v : Fin kLO.FirstOrder.SyntacticSemiterm L n) :
    fun (i : Fin k) => (LO.FirstOrder.Rew.substs w) (v i) = (L.codeIn V).termSubstVec k fun (i : Fin n) => w i fun (i : Fin k) => v i
    @[simp]
    theorem LO.Arith.quote_termShift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } (t : LO.FirstOrder.SyntacticSemiterm L n) :
    LO.FirstOrder.Rew.shift t = (L.codeIn V).termShift t
    theorem LO.Arith.quote_termShiftVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {k : } {n : } (v : Fin kLO.FirstOrder.SyntacticSemiterm L n) :
    fun (i : Fin k) => LO.FirstOrder.Rew.shift (v i) = (L.codeIn V).termShiftVec k fun (i : Fin k) => v i
    @[simp]
    theorem LO.Arith.quote_termBShift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } (t : LO.FirstOrder.SyntacticSemiterm L n) :
    LO.FirstOrder.Rew.bShift t = (L.codeIn V).termBShift t
    theorem LO.Arith.quote_eterm_eq_quote_emb {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] {n : } (t : LO.FirstOrder.Semiterm L Empty n) :
    t = LO.FirstOrder.Rew.embs t
    theorem LO.FirstOrder.Semiformula.quote_rel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] {n : } {k : } (R : L.Rel k) (v : Fin kLO.FirstOrder.SyntacticSemiterm L n) :
    theorem LO.FirstOrder.Semiformula.quote_nrel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] {n : } {k : } (R : L.Rel k) (v : Fin kLO.FirstOrder.SyntacticSemiterm L n) :
    @[simp]
    theorem LO.FirstOrder.Semiformula.quote_verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] (n : ) :
    = LO.Arith.qqVerum
    @[simp]
    theorem LO.FirstOrder.Semiformula.quote_falsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] (n : ) :
    = LO.Arith.qqFalsum
    @[simp]
    theorem LO.FirstOrder.Semiformula.quote_semisentence_def {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] {n : } (p : LO.FirstOrder.Semisentence L n) :
    LO.FirstOrder.Rew.emb.hom p = p
    @[simp]
    theorem LO.Arith.semiformula_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } (p : LO.FirstOrder.SyntacticSemiformula L n) :
    (L.codeIn V).IsSemiformula n p
    @[simp]
    theorem LO.Arith.semiformula_quote0 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (p : LO.FirstOrder.SyntacticFormula L) :
    (L.codeIn V).IsFormula p
    @[simp]
    theorem LO.Arith.semiformula_quote1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (p : LO.FirstOrder.SyntacticSemiformula L 1) :
    (L.codeIn V).IsSemiformula 1 p
    @[simp]
    theorem LO.Arith.semiformula_quote2 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (p : LO.FirstOrder.SyntacticSemiformula L 2) :
    (L.codeIn V).IsSemiformula 2 p
    @[simp]
    theorem LO.Arith.isUFormula_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } (p : LO.FirstOrder.SyntacticSemiformula L n) :
    (L.codeIn V).IsUFormula p
    @[simp]
    theorem LO.Arith.semiformula_quote_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } (p : LO.FirstOrder.SyntacticSemiformula L (n + 1)) :
    (L.codeIn V).IsSemiformula (n + 1) p
    @[simp]
    theorem LO.Arith.quote_neg {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } (p : LO.FirstOrder.SyntacticSemiformula L n) :
    p = (L.codeIn V).neg p
    @[simp]
    theorem LO.Arith.quote_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } (p : LO.FirstOrder.SyntacticSemiformula L n) (q : LO.FirstOrder.SyntacticSemiformula L n) :
    p q = (L.codeIn V).iff p q
    @[simp]
    theorem LO.Arith.quote_shift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } (p : LO.FirstOrder.SyntacticSemiformula L n) :
    (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift) p = (L.codeIn V).shift p
    theorem LO.Arith.qVec_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } {m : } (w : Fin nLO.FirstOrder.SyntacticSemiterm L m) :
    (L.codeIn V).qVec fun (i : Fin n) => w i = LO.Arith.qqBvar 0 :> fun (i : Fin n) => LO.FirstOrder.Rew.bShift (w i)
    @[simp]
    theorem LO.Arith.quote_substs {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } {m : } (w : Fin nLO.FirstOrder.SyntacticSemiterm L m) (p : LO.FirstOrder.SyntacticSemiformula L n) :
    (LO.FirstOrder.Rew.substs w).hom p = (L.codeIn V).substs fun (i : Fin n) => w i p
    theorem LO.Arith.quote_sentence_eq_quote_emb {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] {n : } (σ : LO.FirstOrder.Semisentence L n) :
    σ = LO.FirstOrder.Rew.embs.hom σ
    theorem LO.Arith.quote_substs' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } {m : } (w : Fin nLO.FirstOrder.Semiterm L Empty m) (σ : LO.FirstOrder.Semisentence L n) :
    (LO.FirstOrder.Rew.substs w).hom σ = (L.codeIn V).substs fun (i : Fin n) => w i σ
    @[simp]
    theorem LO.Arith.free_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (p : LO.FirstOrder.SyntacticSemiformula L 1) :
    (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) p = (L.codeIn V).free p

    Typed #

    def LO.FirstOrder.Semiterm.codeIn' (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } (t : LO.FirstOrder.SyntacticSemiterm L n) :
    (L.codeIn V).Semiterm n
    Equations
    Instances For
      def LO.FirstOrder.Semiterm.vCodeIn' (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {k : } {n : } (v : Fin kLO.FirstOrder.SyntacticSemiterm L n) :
      (L.codeIn V).SemitermVec k n
      Equations
      Instances For
        @[simp]
        theorem LO.FirstOrder.Semiterm.vCodeIn'_val (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } {k : } (v : Fin kLO.FirstOrder.SyntacticSemiterm L n) :
        v.val = fun (i : Fin k) => v i
        @[simp]
        theorem LO.FirstOrder.Semiterm.codeIn'_bvar (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } (z : Fin n) :
        LO.FirstOrder.Semiterm.bvar z = (L.codeIn V).bvar z
        @[simp]
        theorem LO.FirstOrder.Semiterm.codeIn'_fvar (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } (x : ) :
        LO.FirstOrder.Semiterm.fvar x = (L.codeIn V).fvar x
        theorem LO.FirstOrder.Semiterm.codeIn'_func (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } {k : } (f : L.Func k) (v : Fin kLO.FirstOrder.SyntacticSemiterm L n) :
        LO.FirstOrder.Semiterm.func f v = (L.codeIn V).func v
        def LO.FirstOrder.Semiformula.codeIn' (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } (p : LO.FirstOrder.SyntacticSemiformula L n) :
        (L.codeIn V).Semiformula n
        Equations
        Instances For
          @[simp]
          theorem LO.FirstOrder.Semiformula.codeIn'_all (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } (p : LO.FirstOrder.SyntacticSemiformula L (n + 1)) :
          ∀' p = (p.cast ).all
          @[simp]
          theorem LO.FirstOrder.Semiformula.codeIn'_ex (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } (p : LO.FirstOrder.SyntacticSemiformula L (n + 1)) :
          ∃' p = (p.cast ).ex
          theorem LO.FirstOrder.Semiformula.quote_sentence_def' (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (σ : LO.FirstOrder.Sentence L) :
          σ = LO.FirstOrder.Rew.embs.hom σ
          theorem LO.Arith.mem_iff_mem_bitIndices {x : } {s : } :
          x s x s.bitIndices
          theorem LO.Arith.Language.IsSemiterm.sound {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } {t : } (ht : (L.codeIn ).IsSemiterm n t) :
          theorem LO.Arith.Language.IsSemiformula.sound {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : } {p : } (h : (L.codeIn ).IsSemiformula n p) :