Typed Formalized IsSemiterm/Term

structure LO.Arith.Language.Semiterm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n : V) : Type u_1

Imported declaration from the Incompleteness formalization.

• val : V

  Imported declaration from the Incompleteness formalization.

• prop : L.IsSemiterm n self.val

structure LO.Arith.Language.SemitermVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (m n : V) : Type u_1

Imported declaration from the Incompleteness formalization.

• val : V

  Imported declaration from the Incompleteness formalization.

• prop : L.IsSemitermVec m n self.val

@[reducible, inline]

abbrev LO.Arith.Language.Term {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : Type u_1

Imported declaration from the Incompleteness formalization.

Equations

• L.Term = L.Semiterm 0

theorem LO.Arith.Language.Semiterm.ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t u : L.Semiterm n} (h : t.val = u.val) : t = u

theorem LO.Arith.Language.Semiterm.ext_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t u : L.Semiterm n} : t = u ↔ t.val = u.val

@[simp]

theorem LO.Arith.Language.Semiterm.isUTerm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) : L.IsUTerm t.val

@[simp]

theorem LO.Arith.Language.SemitermVec.isUTerm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (v : L.SemitermVec k n) : L.IsUTermVec k v.val

theorem LO.Arith.Language.SemitermVec.ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} {v w : L.SemitermVec k n} (h : v.val = w.val) : v = w

theorem LO.Arith.Language.SemitermVec.ext_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} {v w : L.SemitermVec k n} : v = w ↔ v.val = w.val

noncomputable def LO.Arith.Language.bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (z : V) (hz : z < n := by simp) : L.Semiterm n

Imported declaration from the Incompleteness formalization.

Equations

• L.bvar z hz = { val := LO.Arith.qqBvar z, prop := ⋯ }

noncomputable def LO.Arith.Language.fvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) : L.Semiterm n

Imported declaration from the Incompleteness formalization.

Equations

• L.fvar x = { val := LO.Arith.qqFvar x, prop := ⋯ }

noncomputable def LO.Arith.Language.func {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n k f : V} (hf : L.Func k f) (v : L.SemitermVec k n) : L.Semiterm n

Imported declaration from the Incompleteness formalization.

Equations

• L.func hf v = { val := LO.Arith.qqFunc k f v.val, prop := ⋯ }

@[reducible, inline]

noncomputable abbrev LO.Arith.bv {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) (h : x < n := by simp) : L.Semiterm n

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.bv x h = L.bvar x h

@[reducible, inline]

noncomputable abbrev LO.Arith.fv {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) : L.Semiterm n

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.fv x = L.fvar x

def LO.Arith.«term#'_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.«term#'_» = Lean.ParserDescr.node `LO.Arith.«term#'_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#'") (Lean.ParserDescr.cat `term 1024))

def LO.Arith.«term&'_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.«term&'_» = Lean.ParserDescr.node `LO.Arith.«term&'_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "&'") (Lean.ParserDescr.cat `term 1024))

@[simp]

theorem LO.Arith.Language.val_bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (z : V) (hz : z < n) : (L.bvar z hz).val = qqBvar z

@[simp]

theorem LO.Arith.Language.val_fvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) : (L.fvar x).val = qqFvar x

noncomputable def LO.Arith.Language.Semiterm.cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {m n : V} (t : L.Semiterm n) (v : L.SemitermVec m n) : L.SemitermVec (m + 1) n

Imported declaration from the Incompleteness formalization.

Equations

• t.cons v = { val := cons t.val v.val, prop := ⋯ }

def LO.Arith.«term_∷ᵗ_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.«term_∷ᵗ_» = Lean.ParserDescr.trailingNode `LO.Arith.«term_∷ᵗ_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∷ᵗ ") (Lean.ParserDescr.cat `term 67))

@[simp]

theorem LO.Arith.Language.Semitermvec.val_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {m n : V} (t : L.Semiterm n) (v : L.SemitermVec m n) : (t.cons v).val = cons t.val v.val

def LO.Arith.Language.SemitermVec.nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n : V) : L.SemitermVec 0 n

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.Language.SemitermVec.nil L n = { val := 0, prop := ⋯ }

@[simp]

theorem LO.Arith.Language.Semitermvec.val_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n : V) : (SemitermVec.nil L n).val = 0

@[reducible, inline]

noncomputable abbrev LO.Arith.Language.Semiterm.sing {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) : L.SemitermVec (0 + 1) n

Imported declaration from the Incompleteness formalization.

Equations

• t.sing = t.cons (LO.Arith.Language.SemitermVec.nil L n)

noncomputable def LO.Arith.Language.Semiterm.shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) : L.Semiterm n

Imported declaration from the Incompleteness formalization.

Equations

• t.shift = { val := L.termShift t.val, prop := ⋯ }

noncomputable def LO.Arith.Language.Semiterm.bShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) : L.Semiterm (n + 1)

Imported declaration from the Incompleteness formalization.

Equations

• t.bShift = { val := L.termBShift t.val, prop := ⋯ }

noncomputable def LO.Arith.Language.Semiterm.substs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (t : L.Semiterm n) (w : L.SemitermVec n m) : L.Semiterm m

Imported declaration from the Incompleteness formalization.

Equations

• t^ᵗ/[w] = { val := L.termSubst w.val t.val, prop := ⋯ }

@[simp]

theorem LO.Arith.Language.Semiterm.val_shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) : t.shift.val = L.termShift t.val

@[simp]

theorem LO.Arith.Language.Semiterm.val_bShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) : t.bShift.val = L.termBShift t.val

@[simp]

theorem LO.Arith.Language.Semiterm.val_substs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (w : L.SemitermVec n m) (t : L.Semiterm n) : t^ᵗ/[w].val = L.termSubst w.val t.val

def LO.Arith.«term_^ᵗ/[_]» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LO.Arith.Language.SemitermVec.shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (v : L.SemitermVec k n) : L.SemitermVec k n

Imported declaration from the Incompleteness formalization.

Equations

• v.shift = { val := L.termShiftVec k v.val, prop := ⋯ }

noncomputable def LO.Arith.Language.SemitermVec.bShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (v : L.SemitermVec k n) : L.SemitermVec k (n + 1)

Imported declaration from the Incompleteness formalization.

Equations

• v.bShift = { val := L.termBShiftVec k v.val, prop := ⋯ }

noncomputable def LO.Arith.Language.SemitermVec.substs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n m : V} (v : L.SemitermVec k n) (w : L.SemitermVec n m) : L.SemitermVec k m

Imported declaration from the Incompleteness formalization.

Equations

• v.substs w = { val := L.termSubstVec k w.val v.val, prop := ⋯ }

@[simp]

theorem LO.Arith.Language.SemitermVec.val_shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (v : L.SemitermVec k n) : v.shift.val = L.termShiftVec k v.val

@[simp]

theorem LO.Arith.Language.SemitermVec.val_bShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (v : L.SemitermVec k n) : v.bShift.val = L.termBShiftVec k v.val

@[simp]

theorem LO.Arith.Language.SemitermVec.val_substs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n m : V} (v : L.SemitermVec k n) (w : L.SemitermVec n m) : (v.substs w).val = L.termSubstVec k w.val v.val

@[simp]

theorem LO.Arith.Language.SemitermVec.bShift_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n : V) : (nil L n).bShift = nil L (n + 1)

@[simp]

theorem LO.Arith.Language.SemitermVec.bShift_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n k : V} (t : L.Semiterm n) (v : L.SemitermVec k n) : (t.cons v).bShift = t.bShift.cons v.bShift

@[simp]

theorem LO.Arith.Language.SemitermVec.shift_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n : V) : (nil L n).shift = nil L n

@[simp]

theorem LO.Arith.Language.SemitermVec.shift_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n k : V} (t : L.Semiterm n) (v : L.SemitermVec k n) : (t.cons v).shift = t.shift.cons v.shift

@[simp]

theorem LO.Arith.Language.SemitermVec.substs_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (w : L.SemitermVec n m) : (nil L n).substs w = nil L m

@[simp]

theorem LO.Arith.Language.SemitermVec.substs_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m k : V} (w : L.SemitermVec n m) (t : L.Semiterm n) (v : L.SemitermVec k n) : (t.cons v).substs w = t^ᵗ/[w].cons (v.substs w)

noncomputable def LO.Arith.Language.SemitermVec.nth {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (t : L.SemitermVec k n) (i : V) (hi : i < k := by simp) : L.Semiterm n

Imported declaration from the Incompleteness formalization.

Equations

• t.nth i hi = { val := LO.Arith.nth t.val i, prop := ⋯ }

@[simp]

theorem LO.Arith.Language.SemitermVec.nth_val {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (v : L.SemitermVec k n) (i : V) (hi : i < k) : (v.nth i hi).val = Arith.nth v.val i

@[simp]

theorem LO.Arith.Language.SemitermVec.nth_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n k : V} (t : L.Semiterm n) (v : L.SemitermVec k n) : (t.cons v).nth 0 ⋯ = t

@[simp]

theorem LO.Arith.Language.SemitermVec.nth_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n k : V} (t : L.Semiterm n) (v : L.SemitermVec k n) (i : V) (hi : i < k) : (t.cons v).nth (i + 1) ⋯ = v.nth i hi

@[simp]

theorem LO.Arith.Language.SemitermVec.nth_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n k : V} (t : L.Semiterm n) (v : L.SemitermVec (k + 1) n) : (t.cons v).nth 1 ⋯ = v.nth 0 ⋯

theorem LO.Arith.Language.SemitermVec.nth_of_pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n k : V} (t : L.Semiterm n) (v : L.SemitermVec k n) (i : V) (ipos : 0 < i) (hi : i < k + 1) : (t.cons v).nth i hi = v.nth (i - 1) ⋯

noncomputable def LO.Arith.Language.SemitermVec.q {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (w : L.SemitermVec k n) : L.SemitermVec (k + 1) (n + 1)

Imported declaration from the Incompleteness formalization.

Equations

• w.q = (L.bvar 0 ⋯).cons w.bShift

@[simp]

theorem LO.Arith.Language.SemitermVec.q_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (w : L.SemitermVec k n) : w.q.nth 0 ⋯ = L.bvar 0 ⋯

@[simp]

theorem LO.Arith.Language.SemitermVec.q_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (w : L.SemitermVec k n) {i : V} (hi : i < k) : w.q.nth (i + 1) ⋯ = (w.nth i hi).bShift

@[simp]

theorem LO.Arith.Language.SemitermVec.q_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (w : L.SemitermVec k n) (h : 0 < k) : w.q.nth 1 ⋯ = (w.nth 0 h).bShift

theorem LO.Arith.Language.SemitermVec.q_of_pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (w : L.SemitermVec k n) (i : V) (ipos : 0 < i) (hi : i < k + 1) : w.q.nth i hi = (w.nth (i - 1) ⋯).bShift

@[simp]

theorem LO.Arith.Language.SemitermVec.q_val_eq_qVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (w : L.SemitermVec k n) : w.q.val = L.qVec w.val

@[simp]

theorem LO.Arith.Language.Semiterm.shift_bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {z n : V} (hz : z < n) : (L.bvar z hz).shift = L.bvar z hz

@[simp]

theorem LO.Arith.Language.Semiterm.shift_fvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) : (L.fvar x).shift = L.fvar (x + 1)

@[simp]

theorem LO.Arith.Language.Semiterm.shift_func {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n k f : V} (hf : L.Func k f) (v : L.SemitermVec k n) : (L.func hf v).shift = L.func hf v.shift

@[simp]

theorem LO.Arith.Language.Semiterm.bShift_bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {z n : V} (hz : z < n) : (L.bvar z hz).bShift = L.bvar (z + 1) ⋯

@[simp]

theorem LO.Arith.Language.Semiterm.bShift_fvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) : (L.fvar x).bShift = L.fvar x

@[simp]

theorem LO.Arith.Language.Semiterm.bShift_func {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n k f : V} (hf : L.Func k f) (v : L.SemitermVec k n) : (L.func hf v).bShift = L.func hf v.bShift

@[simp]

theorem LO.Arith.Language.Semiterm.substs_bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n z m : V} (w : L.SemitermVec n m) (hz : z < n) : (L.bvar z hz)^ᵗ/[w] = w.nth z hz

@[simp]

theorem LO.Arith.Language.Semiterm.substs_fvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (w : L.SemitermVec n m) (x : V) : (L.fvar x)^ᵗ/[w] = L.fvar x

@[simp]

theorem LO.Arith.Language.Semiterm.substs_func {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m k f : V} (w : L.SemitermVec n m) (hf : L.Func k f) (v : L.SemitermVec k n) : (L.func hf v)^ᵗ/[w] = L.func hf (v.substs w)

@[simp]

theorem LO.Arith.Language.Semiterm.bShift_substs_q {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (t : L.Semiterm n) (w : L.SemitermVec n m) : t.bShift^ᵗ/[w.q] = t^ᵗ/[w].bShift

@[simp]

theorem LO.Arith.Language.Semiterm.bShift_substs_sing {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (t u : L.Term) : (bShift t)^ᵗ/[sing u] = t

theorem LO.Arith.Language.Semiterm.bShift_shift_comm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) : t.shift.bShift = t.bShift.shift

def LO.Arith.Language.Semiterm.FVFree {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• t.FVFree = L.IsTermFVFree n t.val

theorem LO.Arith.Language.Semiterm.FVFree.iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t : L.Semiterm n} : t.FVFree ↔ t.shift = t

@[simp]

theorem LO.Arith.Language.Semiterm.FVFree.bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (z : V) (h : z < n) : (L.bvar z h).FVFree

@[simp]

theorem LO.Arith.Language.Semiterm.FVFree.bShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) (ht : t.FVFree) : t.bShift.FVFree

noncomputable def LO.Arith.Formalized.typedNumeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (n m : V) : ⌜ℒₒᵣ⌝.Semiterm n

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.Formalized.typedNumeral n m = { val := LO.Arith.Formalized.numeral m, prop := ⋯ }

noncomputable def LO.Arith.Formalized.add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} (t u : ⌜ℒₒᵣ⌝.Semiterm n) : ⌜ℒₒᵣ⌝.Semiterm n

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.Formalized.add t u = { val := t.val ^+ u.val, prop := ⋯ }

noncomputable def LO.Arith.Formalized.mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} (t u : ⌜ℒₒᵣ⌝.Semiterm n) : ⌜ℒₒᵣ⌝.Semiterm n

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.Formalized.mul t u = { val := t.val ^* u.val, prop := ⋯ }

@[implicit_reducible]

noncomputable instance LO.Arith.Formalized.instAddSemitermLOR {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (n : V) : Add (⌜ℒₒᵣ⌝.Semiterm n)

Equations

• LO.Arith.Formalized.instAddSemitermLOR n = { add := LO.Arith.Formalized.add }

@[implicit_reducible]

noncomputable instance LO.Arith.Formalized.instMulSemitermLOR {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (n : V) : Mul (⌜ℒₒᵣ⌝.Semiterm n)

Equations

• LO.Arith.Formalized.instMulSemitermLOR n = { mul := LO.Arith.Formalized.mul }

@[implicit_reducible]

noncomputable instance LO.Arith.Formalized.coeNumeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (n : V) : Coe V (⌜ℒₒᵣ⌝.Semiterm n)

Equations

• LO.Arith.Formalized.coeNumeral n = { coe := LO.Arith.Formalized.typedNumeral n }

@[simp]

theorem LO.Arith.Formalized.val_numeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} (x : V) : (typedNumeral n x).val = numeral x

@[simp]

theorem LO.Arith.Formalized.val_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁ + t₂).val = t₁.val ^+ t₂.val

@[simp]

theorem LO.Arith.Formalized.val_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁ * t₂).val = t₁.val ^* t₂.val

@[simp]

theorem LO.Arith.Formalized.add_inj_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} {t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Semiterm n} : t₁ + t₂ = u₁ + u₂ ↔ t₁ = u₁ ∧ t₂ = u₂

@[simp]

theorem LO.Arith.Formalized.mul_inj_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} {t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Semiterm n} : t₁ * t₂ = u₁ * u₂ ↔ t₁ = u₁ ∧ t₂ = u₂

@[simp]

theorem LO.Arith.Formalized.subst_numeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {m n : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (x : V) : (typedNumeral n x)^ᵗ/[w] = typedNumeral m x

@[simp]

theorem LO.Arith.Formalized.subst_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {m n : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁ + t₂)^ᵗ/[w] = t₁^ᵗ/[w] + t₂^ᵗ/[w]

@[simp]

theorem LO.Arith.Formalized.subst_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {m n : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁ * t₂)^ᵗ/[w] = t₁^ᵗ/[w] * t₂^ᵗ/[w]

@[simp]

theorem LO.Arith.Formalized.shift_numeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} (x : V) : (typedNumeral n x).shift = typedNumeral n x

@[simp]

theorem LO.Arith.Formalized.shift_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁ + t₂).shift = t₁.shift + t₂.shift

@[simp]

theorem LO.Arith.Formalized.shift_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁ * t₂).shift = t₁.shift * t₂.shift

@[simp]

theorem LO.Arith.Formalized.bShift_numeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} (x : V) : (typedNumeral n x).bShift = typedNumeral (n + 1) x

@[simp]

theorem LO.Arith.Formalized.bShift_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁ + t₂).bShift = t₁.bShift + t₂.bShift

@[simp]

theorem LO.Arith.Formalized.bShift_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁ * t₂).bShift = t₁.bShift * t₂.bShift

@[simp]

theorem LO.Arith.Formalized.fvFree_numeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} (x : V) : (typedNumeral n x).FVFree

@[simp]

theorem LO.Arith.Formalized.fvFree_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁ + t₂).FVFree ↔ t₁.FVFree ∧ t₂.FVFree

@[simp]

theorem LO.Arith.Formalized.fvFree_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁ * t₂).FVFree ↔ t₁.FVFree ∧ t₂.FVFree