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_dense_linear_orders [2009/04/22 12:08]
vkuncak
sav08:simple_qe_for_dense_linear_orders [2015/04/21 17:30] (current)
Line 13: Line 13:
  
 **Example:​** The '​successor'​ formula: **Example:​** The '​successor'​ formula:
-\[+\begin{equation*}
    ​\forall x. \exists y.\ x < y \ \land\ (\forall z. (x < z \rightarrow z=y \lor y < z)    ​\forall x. \exists y.\ x < y \ \land\ (\forall z. (x < z \rightarrow z=y \lor y < z)
-\]+\end{equation*}
 Is this formula true in dense linear orders? Is there a non-dense linear order where its truth value is different? Is this formula true in dense linear orders? Is there a non-dense linear order where its truth value is different?