LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sav08:simple_qe_for_integer_difference_inequalities [2009/04/21 19:19]
vkuncak
sav08:simple_qe_for_integer_difference_inequalities [2009/04/22 00:04]
vkuncak
Line 1: Line 1:
 ====== Simple QE for Integer Difference Inequalities ====== ====== Simple QE for Integer Difference Inequalities ======
 +
  
  
Line 22: Line 23:
  
 ++++|It is formula with one free variable, $y$. ++++|It is formula with one free variable, $y$.
-So it must be built out of atomic formulas $y \leq y$ and $y=y$, and is therefore either true or false.+So it must be built out of atomic formulas $y \leq y$ and $y=y$, and is therefore ​it is either ​always ​true or always ​false, regardless of the value of $y$. It thus cannot be equivalent to the above formula.
 ++++ ++++
 **End.** **End.**