Shadow syntax of normalized terms. The first element represents the constant term and the list represents the coefficients.
@[simp]
Evaluate a term using the valuation v.
Equations
- omega.term.val v (b, as) = b + omega.coeffs.val v as
@[simp]
Equations
- omega.term.neg (b, as) = (-b, list.func.neg as)
@[simp]
Equations
- omega.term.add (c1, cfs1) (c2, cfs2) = (c1 + c2, list.func.add cfs1 cfs2)
@[simp]
Equations
- omega.term.sub (c1, cfs1) (c2, cfs2) = (c1 - c2, list.func.sub cfs1 cfs2)
@[simp]
Equations
- omega.term.mul i (b, as) = (i * b, list.map (has_mul.mul i) as)
@[simp]
theorem
omega.term.val_neg
{v : ℕ → ℤ}
{t : omega.term} :
omega.term.val v t.neg = -omega.term.val v t
@[simp]
theorem
omega.term.val_sub
{v : ℕ → ℤ}
{t1 t2 : omega.term} :
omega.term.val v (t1.sub t2) = omega.term.val v t1 - omega.term.val v t2
@[simp]
theorem
omega.term.val_add
{v : ℕ → ℤ}
{t1 t2 : omega.term} :
omega.term.val v (t1.add t2) = omega.term.val v t1 + omega.term.val v t2
@[simp]
theorem
omega.term.val_mul
{v : ℕ → ℤ}
{i : ℤ}
{t : omega.term} :
omega.term.val v (omega.term.mul i t) = i * omega.term.val v t
theorem
omega.term.val_div
{v : ℕ → ℤ}
{i b : ℤ}
{as : list ℤ} :
i ∣ b → (∀ (x : ℤ), x ∈ as → i ∣ x) → omega.term.val v (omega.term.div i (b, as)) = omega.term.val v (b, as) / i
Fresh de Brujin index not used by any variable ocurring in the term
Equations
- t.fresh_index = t.snd.length
@[instance]
Equations
Fresh de Brujin index not used by any variable ocurring in the list of terms
Equations
- omega.terms.fresh_index (t :: ts) = max t.fresh_index (omega.terms.fresh_index ts)
- omega.terms.fresh_index list.nil = 0