author | mengj |
Wed, 20 Sep 2006 13:56:39 +0200 | |
changeset 20645 | 5e28b8f2cb52 |
parent 19717 | 2742cec21579 |
permissions | -rw-r--r-- |
19717 | 1 |
%ID: $Id$ |
2 |
%Author: Jia Meng, NICTA |
|
20645
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
3 |
%functional equality and extensionality for const-types-only |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
4 |
|
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
5 |
clause( |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
6 |
forall([A, X, Y], |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
7 |
or( not(hBOOL(hAPP(hAPP(fequal(A),X),Y))), |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
8 |
equal(X,Y))), |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
9 |
a9 ). |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
10 |
|
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
11 |
clause( |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
12 |
forall([A, X, Y], |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
13 |
or( not(equal(X,Y)), |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
14 |
hBOOL(hAPP(hAPP(fequal(A),X),Y)))), |
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
15 |
a10 ). |
19717 | 16 |
|
17 |
clause( |
|
18 |
forall([A, B, F, G], |
|
19 |
or( not(equal(hAPP(F,hAPP(hAPP(hEXTENT(A,B),F),G)),hAPP(G,hAPP(hAPP(hEXTENT(A,B),F),G)))), |
|
20 |
equal(F,G))), |
|
20645
5e28b8f2cb52
Moved the functional equality axioms to helper1 files.
mengj
parents:
19717
diff
changeset
|
21 |
a11 ). |