@[simp]
val_between v as l o is the value (under valuation v) of the term
obtained taking the term represented by (0, as) and dropping all
subterms that include variables outside the range [l,l+o)
Equations
- omega.coeffs.val_between v as l (o + 1) = omega.coeffs.val_between v as l o + list.func.get (l + o) as * v (l + o)
- omega.coeffs.val_between v as l 0 = 0
@[simp]
theorem
omega.coeffs.val_between_nil
{v : ℕ → ℤ}
{l : ℕ}
(m : ℕ) :
omega.coeffs.val_between v list.nil l m = 0
Evaluation of the nonconstant component of a normalized linear arithmetic term.
Equations
- omega.coeffs.val v as = omega.coeffs.val_between v as 0 as.length
theorem
omega.coeffs.val_eq_of_le
{v : ℕ → ℤ}
{as : list ℤ}
{k : ℕ} :
as.length ≤ k → omega.coeffs.val v as = omega.coeffs.val_between v as 0 k
theorem
omega.coeffs.val_between_eq_val_between
{v w : ℕ → ℤ}
{as bs : list ℤ}
{l m : ℕ} :
(∀ (x : ℕ), l ≤ x → x < l + m → v x = w x) → (∀ (x : ℕ), l ≤ x → x < l + m → list.func.get x as = list.func.get x bs) → omega.coeffs.val_between v as l m = omega.coeffs.val_between w bs l m
theorem
omega.coeffs.val_between_set
{v : ℕ → ℤ}
{a : ℤ}
{l n m : ℕ} :
l ≤ n → n < l + m → omega.coeffs.val_between v (list.func.set a list.nil n) l m = a * v n
@[simp]
theorem
omega.coeffs.val_set
{v : ℕ → ℤ}
{m : ℕ}
{a : ℤ} :
omega.coeffs.val v (list.func.set a list.nil m) = a * v m
theorem
omega.coeffs.val_between_neg
{v : ℕ → ℤ}
{as : list ℤ}
{l o : ℕ} :
omega.coeffs.val_between v (list.func.neg as) l o = -omega.coeffs.val_between v as l o
@[simp]
theorem
omega.coeffs.val_neg
{v : ℕ → ℤ}
{as : list ℤ} :
omega.coeffs.val v (list.func.neg as) = -omega.coeffs.val v as
theorem
omega.coeffs.val_between_add
{v : ℕ → ℤ}
{is js : list ℤ}
{l : ℕ}
(m : ℕ) :
omega.coeffs.val_between v (list.func.add is js) l m = omega.coeffs.val_between v is l m + omega.coeffs.val_between v js l m
@[simp]
theorem
omega.coeffs.val_add
{v : ℕ → ℤ}
{is js : list ℤ} :
omega.coeffs.val v (list.func.add is js) = omega.coeffs.val v is + omega.coeffs.val v js
theorem
omega.coeffs.val_between_sub
{v : ℕ → ℤ}
{is js : list ℤ}
{l : ℕ}
(m : ℕ) :
omega.coeffs.val_between v (list.func.sub is js) l m = omega.coeffs.val_between v is l m - omega.coeffs.val_between v js l m
@[simp]
theorem
omega.coeffs.val_sub
{v : ℕ → ℤ}
{is js : list ℤ} :
omega.coeffs.val v (list.func.sub is js) = omega.coeffs.val v is - omega.coeffs.val v js
val_except k v as is the value (under valuation v) of the term
obtained taking the term represented by (0, as) and dropping the
subterm that includes the kth variable.
Equations
- omega.coeffs.val_except k v as = omega.coeffs.val_between v as 0 k + omega.coeffs.val_between v as (k + 1) (as.length - (k + 1))
theorem
omega.coeffs.val_except_eq_val_except
{k : ℕ}
{is js : list ℤ}
{v w : ℕ → ℤ} :
(∀ (x : ℕ), x ≠ k → v x = w x) → (∀ (x : ℕ), x ≠ k → list.func.get x is = list.func.get x js) → omega.coeffs.val_except k v is = omega.coeffs.val_except k w js
theorem
omega.coeffs.val_except_update_set
{v : ℕ → ℤ}
{n : ℕ}
{as : list ℤ}
{i j : ℤ} :
omega.coeffs.val_except n (omega.update n i v) (list.func.set j as n) = omega.coeffs.val_except n v as
theorem
omega.coeffs.val_between_add_val_between
{v : ℕ → ℤ}
{as : list ℤ}
{l m n : ℕ} :
omega.coeffs.val_between v as l m + omega.coeffs.val_between v as (l + m) n = omega.coeffs.val_between v as l (m + n)
theorem
omega.coeffs.val_except_add_eq
{v : ℕ → ℤ}
(n : ℕ)
{as : list ℤ} :
omega.coeffs.val_except n v as + list.func.get n as * v n = omega.coeffs.val v as
@[simp]
theorem
omega.coeffs.val_between_map_mul
{v : ℕ → ℤ}
{i : ℤ}
{as : list ℤ}
{l m : ℕ} :
omega.coeffs.val_between v (list.map (has_mul.mul i) as) l m = i * omega.coeffs.val_between v as l m