Changes between Version 22 and Version 23 of Fundamentals

Timestamp:

05/15/23 07:55:54 (3 years ago)

Author:

siegel

Comment:

--

Fundamentals

@@ -167 +167 @@
 int main() {
   int n=3, m=2;
-  $assert($forall (int i | 0 <= i && i < n) a[i]==0);
-  $assert($forall (int i: 0..n-1) a[i]==0);
-  $assert($forall (int i: 0..n-1 | i%2==0) a[i]==0);
-  $assert($forall (int i: 0..n-1; int j: 0..m-1) b[i][j]==0);
-  $assert($forall (int i: 0..n-1; int j | 0<=j && j<m) b[i][j]==0);
-  $assert($forall (int i: 0..n-1; int j: 0..m-1 | i<j ) b[i][j]==0);
-  $assert($forall (int i,j | 0<=i && i<n && 0<=j && j<m) b[i][j]==0);
-  $assert($exists (int i | 0<=i && i<n) a[i]==0);
+  $assert($forall (int i | 0<=i && i<n) a[i]==0); // all elements of a are 0
+  $assert($forall (int i: 0..n-1) a[i]==0); // same as above
+  $assert($forall (int i: 0..n-1 | i%2==0) a[i]==0); // even elements are 0
+  $assert($forall (int i: 0..n-1#2) a[i]==0); // same as above
+  $assert($forall (int i: 0..n-1; int j: 0..m-1) b[i][j]==0); // all elements of b are 0
+  $assert($forall (int i: 0..n-1; int j | 0<=j && j<m) b[i][j]==0); // same
+  $assert($forall (int i: 0..n-1; int j: 0..m-1 | i<j ) b[i][j]==0); // lower triangle is 0
+  $assert($forall (int i,j | 0<=i && i<n && 0<=j && j<m) b[i][j]==0); // all elements of b are 0
+  $assert($exists (int i | 0<=i && i<n) a[i]==0); // existential: some element of a is 0
+  $assert($forall (int i: 0..n-1) $exists (int j: 0..i) a[j]<=a[i]); // nested quantification
 }
 }}}