Documentation

Arithmetization.ISigmaOne.Metamath.Term.Typed

Typed Formalized IsSemiterm/Term #

source
structure LO.Arith.Language.Semiterm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n : V) :
Type u_1
  • val : V
  • prop : L.IsSemiterm n self.val
Instances For
source
structure LO.Arith.Language.SemitermVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (m n : V) :
Type u_1
  • val : V
  • prop : L.IsSemitermVec m n self.val
Instances For
source
@[reducible, inline]
abbrev LO.Arith.Language.Term {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
Type u_1
Equations
  • L.Term = L.Semiterm 0
source
theorem LO.Arith.Language.Semiterm.ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (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
source
@[simp]
theorem LO.Arith.Language.Semiterm.isUTerm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
L.IsUTerm t.val
source
@[simp]
theorem LO.Arith.Language.SemitermVec.isUTerm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (v : L.SemitermVec k n) :
L.IsUTermVec k v.val
source
theorem LO.Arith.Language.SemitermVec.ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (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
source
def LO.Arith.Language.bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (z : V) (hz : z < n := by simp) :
L.Semiterm n
Equations
source
def LO.Arith.Language.fvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) :
L.Semiterm n
Equations
source
def LO.Arith.Language.func {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (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
Equations
source
@[reducible, inline]
abbrev LO.Arith.bv {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) (h : x < n := by simp) :
L.Semiterm n
Equations
source
@[reducible, inline]
abbrev LO.Arith.fv {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) :
L.Semiterm n
Equations
source
def LO.Arith.«term#'_» :
Lean.ParserDescr
Equations
source
def LO.Arith.«term&'_» :
Lean.ParserDescr
Equations
source
@[simp]
theorem LO.Arith.Language.val_bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.val_fvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) :
(L.fvar x).val = qqFvar x
source
def LO.Arith.Language.Semiterm.cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
Equations
  • t.cons v = { val := cons t.val v.val, prop := ⋯ }
source
def LO.Arith.«term_∷ᵗ_» :
Lean.TrailingParserDescr
Equations
source
@[simp]
theorem LO.Arith.Language.Semitermvec.val_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
def LO.Arith.Language.SemitermVec.nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n : V) :
L.SemitermVec 0 n
Equations
source
@[simp]
theorem LO.Arith.Language.Semitermvec.val_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n : V) :
(SemitermVec.nil L n).val = 0
source
@[reducible, inline]
abbrev LO.Arith.Language.Semiterm.sing {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
L.SemitermVec (0 + 1) n
Equations
source
def LO.Arith.Language.Semiterm.shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
L.Semiterm n
Equations
  • t.shift = { val := L.termShift t.val, prop := ⋯ }
source
def LO.Arith.Language.Semiterm.bShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
L.Semiterm (n + 1)
Equations
  • t.bShift = { val := L.termBShift t.val, prop := ⋯ }
source
def LO.Arith.Language.Semiterm.substs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
Equations
  • t^ᵗ/[w] = { val := L.termSubst w.val t.val, prop := ⋯ }
source
@[simp]
theorem LO.Arith.Language.Semiterm.val_shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
t.shift.val = L.termShift t.val
source
@[simp]
theorem LO.Arith.Language.Semiterm.val_bShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
t.bShift.val = L.termBShift t.val
source
@[simp]
theorem LO.Arith.Language.Semiterm.val_substs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
def LO.Arith.«term_^ᵗ/[_]» :
Lean.TrailingParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.Arith.Language.SemitermVec.shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (v : L.SemitermVec k n) :
L.SemitermVec k n
Equations
  • v.shift = { val := L.termShiftVec k v.val, prop := ⋯ }
source
def LO.Arith.Language.SemitermVec.bShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n : V} (v : L.SemitermVec k n) :
L.SemitermVec k (n + 1)
Equations
  • v.bShift = { val := L.termBShiftVec k v.val, prop := ⋯ }
source
def LO.Arith.Language.SemitermVec.substs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
Equations
  • v.substs w = { val := L.termSubstVec k w.val v.val, prop := ⋯ }
source
@[simp]
theorem LO.Arith.Language.SemitermVec.val_shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.SemitermVec.val_bShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.SemitermVec.val_substs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.SemitermVec.bShift_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n : V) :
(nil L n).bShift = nil L (n + 1)
source
@[simp]
theorem LO.Arith.Language.SemitermVec.bShift_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.SemitermVec.shift_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n : V) :
(nil L n).shift = nil L n
source
@[simp]
theorem LO.Arith.Language.SemitermVec.shift_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.SemitermVec.substs_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.SemitermVec.substs_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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)
source
def LO.Arith.Language.SemitermVec.nth {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
Equations
source
@[simp]
theorem LO.Arith.Language.SemitermVec.nth_val {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.SemitermVec.nth_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.SemitermVec.nth_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.SemitermVec.nth_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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 ⋯
source
theorem LO.Arith.Language.SemitermVec.nth_of_pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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 ⋯ = v.nth (i - 1) ⋯
source
def LO.Arith.Language.SemitermVec.q {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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)
Equations
  • w.q = (L.bvar 0 ⋯).cons w.bShift
source
@[simp]
theorem LO.Arith.Language.SemitermVec.q_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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 ⋯
source
@[simp]
theorem LO.Arith.Language.SemitermVec.q_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.SemitermVec.q_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
theorem LO.Arith.Language.SemitermVec.q_of_pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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 ⋯ = (w.nth (i - 1) ⋯).bShift
source
@[simp]
theorem LO.Arith.Language.SemitermVec.q_val_eq_qVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.Semiterm.shift_bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.Semiterm.shift_fvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) :
(L.fvar x).shift = L.fvar (x + 1)
source
@[simp]
theorem LO.Arith.Language.Semiterm.shift_func {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.Semiterm.bShift_bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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) ⋯
source
@[simp]
theorem LO.Arith.Language.Semiterm.bShift_fvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) :
(L.fvar x).bShift = L.fvar x
source
@[simp]
theorem LO.Arith.Language.Semiterm.bShift_func {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.Semiterm.substs_bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.Semiterm.substs_fvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.Semiterm.substs_func {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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)
source
@[simp]
theorem LO.Arith.Language.Semiterm.bShift_substs_q {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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
source
@[simp]
theorem LO.Arith.Language.Semiterm.bShift_substs_sing {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (t u : L.Term) :
(bShift t)^ᵗ/[sing u] = t
source
theorem LO.Arith.Language.Semiterm.bShift_shift_comm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
t.shift.bShift = t.bShift.shift
source
def LO.Arith.Language.Semiterm.FVFree {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) :
Prop
Equations
  • t.FVFree = L.IsTermFVFree n t.val
source
theorem LO.Arith.Language.Semiterm.FVFree.iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t : L.Semiterm n} :
t.FVFree ↔ t.shift = t
source
@[simp]
theorem LO.Arith.Language.Semiterm.FVFree.bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (z : V) (h : z < n) :
(L.bvar z h).FVFree
source
@[simp]
theorem LO.Arith.Language.Semiterm.FVFree.bShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (t : L.Semiterm n) (ht : t.FVFree) :
t.bShift.FVFree
source
def LO.Arith.Formalized.typedNumeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n m : V) :
⌜ℒₒᵣ⌝.Semiterm n
Equations
source
def LO.Arith.Formalized.add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t u : ⌜ℒₒᵣ⌝.Semiterm n) :
⌜ℒₒᵣ⌝.Semiterm n
Equations
source
def LO.Arith.Formalized.mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t u : ⌜ℒₒᵣ⌝.Semiterm n) :
⌜ℒₒᵣ⌝.Semiterm n
Equations
source
instance LO.Arith.Formalized.instAddSemitermLOR {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) :
Add (⌜ℒₒᵣ⌝.Semiterm n)
Equations
source
instance LO.Arith.Formalized.instMulSemitermLOR {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) :
Mul (⌜ℒₒᵣ⌝.Semiterm n)
Equations
source
instance LO.Arith.Formalized.coeNumeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) :
Coe V (⌜ℒₒᵣ⌝.Semiterm n)
Equations
source
@[simp]
theorem LO.Arith.Formalized.val_numeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (x : V) :
(typedNumeral n x).val = numeral x
source
@[simp]
theorem LO.Arith.Formalized.val_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
(t₁ + t₂).val = t₁.val ^+ t₂.val
source
@[simp]
theorem LO.Arith.Formalized.val_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
(t₁ * t₂).val = t₁.val ^* t₂.val
source
@[simp]
theorem LO.Arith.Formalized.add_inj_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Semiterm n} :
t₁ + t₂ = u₁ + u₂ ↔ t₁ = u₁ ∧ t₂ = u₂
source
@[simp]
theorem LO.Arith.Formalized.mul_inj_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Semiterm n} :
t₁ * t₂ = u₁ * u₂ ↔ t₁ = u₁ ∧ t₂ = u₂
source
@[simp]
theorem LO.Arith.Formalized.subst_numeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m n : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (x : V) :
(typedNumeral n x)^ᵗ/[w] = typedNumeral m x
source
@[simp]
theorem LO.Arith.Formalized.subst_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m n : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
(t₁ + t₂)^ᵗ/[w] = t₁^ᵗ/[w] + t₂^ᵗ/[w]
source
@[simp]
theorem LO.Arith.Formalized.subst_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m n : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
(t₁ * t₂)^ᵗ/[w] = t₁^ᵗ/[w] * t₂^ᵗ/[w]
source
@[simp]
theorem LO.Arith.Formalized.shift_numeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (x : V) :
(typedNumeral n x).shift = typedNumeral n x
source
@[simp]
theorem LO.Arith.Formalized.shift_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
(t₁ + t₂).shift = t₁.shift + t₂.shift
source
@[simp]
theorem LO.Arith.Formalized.shift_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
(t₁ * t₂).shift = t₁.shift * t₂.shift
source
@[simp]
theorem LO.Arith.Formalized.bShift_numeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (x : V) :
(typedNumeral n x).bShift = typedNumeral (n + 1) x
source
@[simp]
theorem LO.Arith.Formalized.bShift_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
(t₁ + t₂).bShift = t₁.bShift + t₂.bShift
source
@[simp]
theorem LO.Arith.Formalized.bShift_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
(t₁ * t₂).bShift = t₁.bShift * t₂.bShift
source
@[simp]
theorem LO.Arith.Formalized.fvFree_numeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (x : V) :
(typedNumeral n x).FVFree
source
@[simp]
theorem LO.Arith.Formalized.fvFree_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
(t₁ + t₂).FVFree ↔ t₁.FVFree ∧ t₂.FVFree
source
@[simp]
theorem LO.Arith.Formalized.fvFree_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :
(t₁ * t₂).FVFree ↔ t₁.FVFree ∧ t₂.FVFree