Typed Formalized IsSemiterm/Term #
structure
LO.Arith.Language.Semiterm
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(n : V)
:
Type u_1
- val : V
- prop : L.IsSemiterm n self.val
Instances For
@[simp]
theorem
LO.Arith.Language.Semiterm.prop
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
(self : L.Semiterm n)
:
L.IsSemiterm n self.val
structure
LO.Arith.Language.SemitermVec
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(m : V)
(n : V)
:
Type u_1
- val : V
- prop : L.IsSemitermVec m n self.val
Instances For
@[simp]
theorem
LO.Arith.Language.SemitermVec.prop
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{m : V}
{n : V}
(self : L.SemitermVec m n)
:
L.IsSemitermVec m n self.val
@[reducible, inline]
abbrev
LO.Arith.Language.Term
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
Type u_1
Equations
- L.Term = L.Semiterm 0
Instances For
theorem
LO.Arith.Language.Semiterm.ext
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{t : L.Semiterm n}
{u : L.Semiterm n}
(h : t.val = u.val)
:
t = u
theorem
LO.Arith.Language.Semiterm.ext_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{t : L.Semiterm n}
{u : L.Semiterm n}
:
@[simp]
theorem
LO.Arith.Language.Semiterm.isUTerm
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{n : V}
(v : L.SemitermVec k n)
:
L.IsUTermVec k v.val
theorem
LO.Arith.Language.SemitermVec.ext
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{n : V}
{v : L.SemitermVec k n}
{w : L.SemitermVec k n}
(h : v.val = w.val)
:
v = w
def
LO.Arith.Language.bvar
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
(z : V)
(hz : autoParam (z < n) _auto✝)
:
L.Semiterm n
Equations
- L.bvar z hz = { val := LO.Arith.qqBvar z, prop := ⋯ }
Instances For
def
LO.Arith.Language.fvar
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
(x : V)
:
L.Semiterm n
Equations
- L.fvar x = { val := LO.Arith.qqFvar x, prop := ⋯ }
Instances For
def
LO.Arith.Language.func
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{k : V}
{f : V}
(hf : L.Func k f)
(v : L.SemitermVec k n)
:
L.Semiterm n
Equations
- L.func hf v = { val := LO.Arith.qqFunc k f v.val, prop := ⋯ }
Instances For
@[reducible, inline]
abbrev
LO.Arith.bv
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
(x : V)
(h : autoParam (x < n) _auto✝)
:
L.Semiterm n
Equations
- LO.Arith.bv x h = L.bvar x h
Instances For
@[reducible, inline]
abbrev
LO.Arith.fv
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
(x : V)
:
L.Semiterm n
Equations
- LO.Arith.fv x = L.fvar x
Instances For
Equations
- LO.Arith.«term#'_» = Lean.ParserDescr.node `LO.Arith.term#'_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#'") (Lean.ParserDescr.cat `term 1024))
Instances For
Equations
- LO.Arith.«term&'_» = Lean.ParserDescr.node `LO.Arith.term&'_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "&'") (Lean.ParserDescr.cat `term 1024))
Instances For
@[simp]
theorem
LO.Arith.Language.val_bvar
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
(z : V)
(hz : z < n)
:
(L.bvar z hz).val = LO.Arith.qqBvar z
@[simp]
theorem
LO.Arith.Language.val_fvar
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
(x : V)
:
(L.fvar x).val = LO.Arith.qqFvar x
def
LO.Arith.Language.Semiterm.cons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{m : V}
{n : V}
(t : L.Semiterm n)
(v : L.SemitermVec m n)
:
L.SemitermVec (m + 1) n
Instances For
Equations
- LO.Arith.«term_∷ᵗ_» = Lean.ParserDescr.trailingNode `LO.Arith.term_∷ᵗ_ 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∷ᵗ ") (Lean.ParserDescr.cat `term 67))
Instances For
@[simp]
theorem
LO.Arith.Language.Semitermvec.val_cons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{m : V}
{n : V}
(t : L.Semiterm n)
(v : L.SemitermVec m n)
:
def
LO.Arith.Language.SemitermVec.nil
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(n : V)
:
L.SemitermVec 0 n
Equations
- LO.Arith.Language.SemitermVec.nil L n = { val := 0, prop := ⋯ }
Instances For
@[simp]
theorem
LO.Arith.Language.Semitermvec.val_nil
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(n : V)
:
(LO.Arith.Language.SemitermVec.nil L n).val = 0
@[reducible, inline]
abbrev
LO.Arith.Language.Semiterm.sing
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
(t : L.Semiterm n)
:
L.SemitermVec (0 + 1) n
Equations
- t.sing = t.cons (LO.Arith.Language.SemitermVec.nil L n)
Instances For
def
LO.Arith.Language.Semiterm.shift
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
(t : L.Semiterm n)
:
L.Semiterm n
Equations
- t.shift = { val := L.termShift t.val, prop := ⋯ }
Instances For
def
LO.Arith.Language.Semiterm.bShift
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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 := ⋯ }
Instances For
def
LO.Arith.Language.Semiterm.substs
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{m : V}
(t : L.Semiterm n)
(w : L.SemitermVec n m)
:
L.Semiterm m
Instances For
@[simp]
theorem
LO.Arith.Language.Semiterm.val_shift
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{m : V}
(w : L.SemitermVec n m)
(t : L.Semiterm n)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Arith.Language.SemitermVec.shift
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{n : V}
(v : L.SemitermVec k n)
:
L.SemitermVec k n
Equations
- v.shift = { val := L.termShiftVec k v.val, prop := ⋯ }
Instances For
def
LO.Arith.Language.SemitermVec.bShift
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{n : V}
(v : L.SemitermVec k n)
:
L.SemitermVec k (n + 1)
Equations
- v.bShift = { val := L.termBShiftVec k v.val, prop := ⋯ }
Instances For
def
LO.Arith.Language.SemitermVec.substs
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{n : V}
{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 := ⋯ }
Instances For
@[simp]
theorem
LO.Arith.Language.SemitermVec.val_shift
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{n : V}
{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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(n : V)
:
(LO.Arith.Language.SemitermVec.nil L n).bShift = LO.Arith.Language.SemitermVec.nil L (n + 1)
@[simp]
theorem
LO.Arith.Language.SemitermVec.bShift_cons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{k : V}
(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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(n : V)
:
(LO.Arith.Language.SemitermVec.nil L n).shift = LO.Arith.Language.SemitermVec.nil L n
@[simp]
theorem
LO.Arith.Language.SemitermVec.shift_cons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{k : V}
(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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{m : V}
(w : L.SemitermVec n m)
:
(LO.Arith.Language.SemitermVec.nil L n).substs w = LO.Arith.Language.SemitermVec.nil L m
@[simp]
theorem
LO.Arith.Language.SemitermVec.substs_cons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{m : V}
{k : V}
(w : L.SemitermVec n m)
(t : L.Semiterm n)
(v : L.SemitermVec k n)
:
def
LO.Arith.Language.SemitermVec.nth
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{n : V}
(t : L.SemitermVec k n)
(i : V)
(hi : autoParam (i < k) _auto✝)
:
L.Semiterm n
Equations
- t.nth i hi = { val := LO.Arith.nth t.val i, prop := ⋯ }
Instances For
@[simp]
theorem
LO.Arith.Language.SemitermVec.nth_val
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{n : V}
(v : L.SemitermVec k n)
(i : V)
(hi : i < k)
:
(v.nth i hi).val = LO.Arith.nth v.val i
@[simp]
theorem
LO.Arith.Language.SemitermVec.nth_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{k : V}
(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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{k : V}
(t : L.Semiterm n)
(v : L.SemitermVec k n)
(i : V)
(hi : i < k)
:
@[simp]
theorem
LO.Arith.Language.SemitermVec.nth_one
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{k : V}
(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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{k : V}
(t : L.Semiterm n)
(v : L.SemitermVec k n)
(i : V)
(ipos : 0 < i)
(hi : i < k + 1)
:
def
LO.Arith.Language.SemitermVec.q
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{n : V}
(w : L.SemitermVec k n)
:
Equations
- w.q = (L.bvar 0 ⋯).cons w.bShift
Instances For
@[simp]
theorem
LO.Arith.Language.SemitermVec.q_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{n : V}
(w : L.SemitermVec k n)
{i : V}
(hi : i < k)
:
@[simp]
theorem
LO.Arith.Language.SemitermVec.q_one
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{n : V}
(w : L.SemitermVec k n)
(i : V)
(ipos : 0 < i)
(hi : i < k + 1)
:
@[simp]
theorem
LO.Arith.Language.SemitermVec.q_val_eq_qVec
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{z : V}
{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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
(x : V)
:
@[simp]
theorem
LO.Arith.Language.Semiterm.shift_func
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{k : V}
{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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{z : V}
{n : V}
(hz : z < n)
:
@[simp]
theorem
LO.Arith.Language.Semiterm.bShift_fvar
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{k : V}
{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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{z : V}
{m : V}
(w : L.SemitermVec n m)
(hz : z < n)
:
@[simp]
theorem
LO.Arith.Language.Semiterm.substs_fvar
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{m : V}
(w : L.SemitermVec n m)
(x : V)
:
@[simp]
theorem
LO.Arith.Language.Semiterm.substs_func
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{m : V}
{k : V}
{f : V}
(w : L.SemitermVec n m)
(hf : L.Func k f)
(v : L.SemitermVec k n)
:
@[simp]
theorem
LO.Arith.Language.Semiterm.bShift_substs_q
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{m : V}
(t : L.Semiterm n)
(w : L.SemitermVec n m)
:
@[simp]
theorem
LO.Arith.Language.Semiterm.bShift_substs_sing
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(t : L.Term)
(u : L.Term)
:
theorem
LO.Arith.Language.Semiterm.bShift_shift_comm
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
(t : L.Semiterm n)
:
Equations
- t.FVFree = L.IsTermFVFree n t.val
Instances For
theorem
LO.Arith.Language.Semiterm.FVFree.iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{t : L.Semiterm n}
:
@[simp]
theorem
LO.Arith.Language.Semiterm.FVFree.bvar
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
(t : L.Semiterm n)
(ht : t.FVFree)
:
t.bShift.FVFree
def
LO.Arith.Formalized.typedNumeral
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(n : V)
(m : V)
:
⌜ℒₒᵣ⌝.Semiterm n
Equations
- LO.Arith.Formalized.typedNumeral n m = { val := LO.Arith.Formalized.numeral m, prop := ⋯ }
Instances For
def
LO.Arith.Formalized.add
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : V}
(t : ⌜ℒₒᵣ⌝.Semiterm n)
(u : ⌜ℒₒᵣ⌝.Semiterm n)
:
⌜ℒₒᵣ⌝.Semiterm n
Equations
- LO.Arith.Formalized.add t u = { val := t.val ^+ u.val, prop := ⋯ }
Instances For
def
LO.Arith.Formalized.mul
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : V}
(t : ⌜ℒₒᵣ⌝.Semiterm n)
(u : ⌜ℒₒᵣ⌝.Semiterm n)
:
⌜ℒₒᵣ⌝.Semiterm n
Equations
- LO.Arith.Formalized.mul t u = { val := t.val ^* u.val, prop := ⋯ }
Instances For
instance
LO.Arith.Formalized.instAddSemitermLOR
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(n : V)
:
Equations
- LO.Arith.Formalized.instAddSemitermLOR n = { add := LO.Arith.Formalized.add }
instance
LO.Arith.Formalized.instMulSemitermLOR
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(n : V)
:
Equations
- LO.Arith.Formalized.instMulSemitermLOR n = { mul := LO.Arith.Formalized.mul }
Equations
- LO.Arith.Formalized.coeNumeral n = { coe := LO.Arith.Formalized.typedNumeral n }
@[simp]
theorem
LO.Arith.Formalized.val_numeral
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : V}
(x : V)
:
@[simp]
theorem
LO.Arith.Formalized.subst_numeral
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{m : V}
{n : V}
(w : ⌜ℒₒᵣ⌝.SemitermVec n m)
(x : V)
:
@[simp]
theorem
LO.Arith.Formalized.shift_numeral
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : V}
(x : V)
:
(LO.Arith.Formalized.typedNumeral n x).shift = LO.Arith.Formalized.typedNumeral n x
@[simp]
theorem
LO.Arith.Formalized.bShift_numeral
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : V}
(x : V)
:
(LO.Arith.Formalized.typedNumeral n x).bShift = LO.Arith.Formalized.typedNumeral (n + 1) x
@[simp]
theorem
LO.Arith.Formalized.fvFree_numeral
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : V}
(x : V)
:
(LO.Arith.Formalized.typedNumeral n x).FVFree