Differences

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

--- sav08:exists-forall_class_definition [2008/04/03 13:41]
vkuncak created
+++ sav08:exists-forall_class_definition [2008/04/03 13:42]
vkuncak
@@ Line 21: / Line 21: @@
 \]
-Relation $r$ is a partial function
+List contains no duplicates:
 \[
-    \forall x, y_1, y_1. R(x,y_1) \land R(x,y_2) \rightarrow y_1=y_2
+   \forall x,y. ListNode(x) \land ListNode(y) \land data(x) = data(y) \rightarrow x=y
 \]
-List contains no duplicates:
+Relation $r$ is a partial function
 \[
-   \forall x,y. ListNode(x) \land ListNode(y) \land data(x) = data(y) \rightarrow x=y
+    \forall x, y_1, y_1. R(x,y_1) \land R(x,y_2) \rightarrow y_1=y_2
 \]
+We **cannot** express in this class that $R$ is a total function, or property like $\forall x. \exists y. R(x,y)$ because we need an existential quantifier after a universal one.