| changeset 20645 | 5e28b8f2cb52 |
| parent 19717 | 2742cec21579 |
| 20644:ff938c7b15e8 | 20645:5e28b8f2cb52 |
|---|---|
1 %ID: $Id$ |
1 %ID: $Id$ |
2 %Author: Jia Meng, NICTA |
2 %Author: Jia Meng, NICTA |
3 %extensionality for partial types |
3 %functional equality and extensionality for partial types |
4 |
|
5 clause( |
|
6 forall([A, X, Y], |
|
7 or( not(hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool)))), |
|
8 equal(X,Y))), |
|
9 a9 ). |
|
10 |
|
11 clause( |
|
12 forall([A, X, Y], |
|
13 or( not(equal(X,Y)), |
|
14 hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))))), |
|
15 a10 ). |
|
4 |
16 |
5 clause( |
17 clause( |
6 forall([A, B, F, G], |
18 forall([A, B, F, G], |
7 or( not(equal(hAPP(F,hAPP(hAPP(hEXTENT,F,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),G,tc_fun(tc_fun(A,B),A)),tc_fun(A,B)),hAPP(G,hAPP(hAPP(hEXTENT,F,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),G,tc_fun(tc_fun(A,B),A)),tc_fun(A,B)))), |
19 or( not(equal(hAPP(F,hAPP(hAPP(hEXTENT,F,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),G,tc_fun(tc_fun(A,B),A)),tc_fun(A,B)),hAPP(G,hAPP(hAPP(hEXTENT,F,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),G,tc_fun(tc_fun(A,B),A)),tc_fun(A,B)))), |
8 equal(F,G))), |
20 equal(F,G))), |
9 a18 ). |
21 a11 ). |