diff options
Diffstat (limited to 'Test/test0/Answer')
| -rw-r--r-- | Test/test0/Answer | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/Test/test0/Answer b/Test/test0/Answer index d57e7647..0eda9e2e 100644 --- a/Test/test0/Answer +++ b/Test/test0/Answer @@ -34,6 +34,12 @@ const y: int; const z: int;
+const r: real;
+
+const s: real;
+
+const t: real;
+
const P: bool;
const Q: bool;
@@ -56,6 +62,36 @@ axiom x + y mod z == y mod z + x; axiom (x + y) mod z == x mod z + y mod z;
+axiom x / y / z == x / (y / z);
+
+axiom x / y / (z / x) == x / y / z;
+
+axiom x / s / z == x / (s / z);
+
+axiom x / s / (z / x) == x / s / z;
+
+axiom r / s / t == r / (s / t);
+
+axiom r / s / (t / r) == r / s / t;
+
+axiom r * s / t == r * s / t;
+
+axiom r / s * t == r / s * t;
+
+axiom (r * s) ** t == r ** t * s ** t;
+
+axiom r ** (s + t) == r ** s * r ** t;
+
+axiom int(real(x)) == x;
+
+axiom r >= 0e0 ==> real(int(r)) <= r;
+
+axiom int(0e0 - 2e-2) == 0;
+
+axiom int(0e0 - 35e0) == -35;
+
+axiom int(27e-1) == 2;
+
axiom x - y - z == x - (y - z);
axiom x - y - (z - x) == x - y - z;
|