| changeset 20806 | 3728dba101f1 |
| parent 20805 | 35574b9b59aa |
| child 20807 | bd3b60f9a343 |
| 20805:35574b9b59aa | 20806:3728dba101f1 |
|---|---|
1 %ID: $Id$ |
|
2 %Author: Jia Meng, NICTA |
|
3 %functional equality and extensionality for const-types-only |
|
4 |
|
5 input_clause(a9,axiom, |
|
6 [--hBOOL(hAPP(hAPP(fequal(A),X),Y)),++equal(X,Y)]). |
|
7 |
|
8 input_clause(a10,axiom, |
|
9 [++hBOOL(hAPP(hAPP(fequal(A),X),Y)),--equal(X,Y)]). |
|
10 |
|
11 input_clause(a11,axiom, |
|
12 [--equal(hAPP(F,hAPP(hAPP(hEXTENT(A,B),F),G)),hAPP(G,hAPP(hAPP(hEXTENT(A,B),F),G))), |
|
13 ++equal(F,G)]). |
|
14 |
|
15 |
|
16 |