Find subtraction inside preterm and return its operands
Equations
- (t.sub s).sub_terms = (t.sub_terms <|> s.sub_terms <|> option.some (t, s))
- (t.add s).sub_terms = (t.sub_terms <|> s.sub_terms)
- (omega.nat.preterm.var i n).sub_terms = option.none
- (omega.nat.preterm.cst i).sub_terms = option.none
Find (t - s) inside a preterm and replace it with variable k
Equations
- t.sub_subst s k (x.sub y) = ite (x = t ∧ y = s) (omega.nat.preterm.var 1 k) ((t.sub_subst s k x).sub (t.sub_subst s k y))
- t.sub_subst s k (x.add y) = (t.sub_subst s k x).add (t.sub_subst s k y)
- t.sub_subst s k (omega.nat.preterm.var m n) = omega.nat.preterm.var m n
- t.sub_subst s k (omega.nat.preterm.cst m) = omega.nat.preterm.cst m
theorem
omega.nat.preterm.val_sub_subst
{k : ℕ}
{x y : omega.nat.preterm}
{v : ℕ → ℕ}
{t : omega.nat.preterm} :
t.fresh_index ≤ k → omega.nat.preterm.val (omega.update k (omega.nat.preterm.val v x - omega.nat.preterm.val v y) v) (x.sub_subst y k t) = omega.nat.preterm.val v t
Find subtraction inside preform and return its operands
@[simp]
Find (t - s) inside a preform and replace it with variable k
Equations
- omega.nat.preform.sub_subst x y k (p.and q) = (omega.nat.preform.sub_subst x y k p).and (omega.nat.preform.sub_subst x y k q)
- omega.nat.preform.sub_subst x y k (p.or q) = (omega.nat.preform.sub_subst x y k p).or (omega.nat.preform.sub_subst x y k q)
- omega.nat.preform.sub_subst x y k p.not = (omega.nat.preform.sub_subst x y k p).not
- omega.nat.preform.sub_subst x y k (omega.nat.preform.le t s) = omega.nat.preform.le (x.sub_subst y k t) (x.sub_subst y k s)
- omega.nat.preform.sub_subst x y k (omega.nat.preform.eq t s) = omega.nat.preform.eq (x.sub_subst y k t) (x.sub_subst y k s)
Preform which asserts that the value of variable k is the truncated difference between preterms t and s
Equations
- omega.nat.is_diff t s k = (omega.nat.preform.eq t (s.add (omega.nat.preterm.var 1 k))).or ((omega.nat.preform.le t s).and (omega.nat.preform.eq (omega.nat.preterm.var 1 k) (omega.nat.preterm.cst 0)))
theorem
omega.nat.holds_is_diff
{t s : omega.nat.preterm}
{k : ℕ}
{v : ℕ → ℕ} :
v k = omega.nat.preterm.val v t - omega.nat.preterm.val v s → omega.nat.preform.holds v (omega.nat.is_diff t s k)
Helper function for sub_elim
Equations
- omega.nat.sub_elim_core t s k p = (omega.nat.preform.sub_subst t s k p).and (omega.nat.is_diff t s k)
Return de Brujin index of fresh variable that does not occur in any of the arguments
Equations
- omega.nat.sub_fresh_index t s p = max p.fresh_index (max t.fresh_index s.fresh_index)
Return a new preform with all subtractions eliminated
Equations
- omega.nat.sub_elim t s p = omega.nat.sub_elim_core t s (omega.nat.sub_fresh_index t s p) p
theorem
omega.nat.sub_subst_equiv
{k : ℕ}
{x y : omega.nat.preterm}
{v : ℕ → ℕ}
(p : omega.nat.preform) :
p.fresh_index ≤ k → (omega.nat.preform.holds (omega.update k (omega.nat.preterm.val v x - omega.nat.preterm.val v y) v) (omega.nat.preform.sub_subst x y k p) ↔ omega.nat.preform.holds v p)
theorem
omega.nat.sat_sub_elim
{t s : omega.nat.preterm}
{p : omega.nat.preform} :
p.sat → (omega.nat.sub_elim t s p).sat
theorem
omega.nat.unsat_of_unsat_sub_elim
(t s : omega.nat.preterm)
(p : omega.nat.preform) :
(omega.nat.sub_elim t s p).unsat → p.unsat