| author | mengj |
| Fri, 28 Apr 2006 06:05:19 +0200 | |
| changeset 19492 | 29c6cba140da |
| child 20645 | 5e28b8f2cb52 |
| permissions | -rw-r--r-- |
|
19492
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
1 |
%ID: $Id$ |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
2 |
%Author: Jia Meng, NICTA |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
3 |
%extensionality for full-types |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
4 |
|
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
5 |
input_clause(a18,axiom, |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
6 |
[--equal(typeinfo(hAPP(typeinfo(F,tc_fun(A,B)),typeinfo(hAPP(typeinfo(hAPP(typeinfo(hEXTENT,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),typeinfo(F,tc_fun(A,B))),tc_fun(tc_fun(A,B),A)),typeinfo(G,tc_fun(A,B))),A)),B),typeinfo(hAPP(typeinfo(G,tc_fun(A,B)),typeinfo(hAPP(typeinfo(hAPP(typeinfo(hEXTENT,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),typeinfo(F,tc_fun(A,B))),tc_fun(tc_fun(A,B),A)),typeinfo(G,tc_fun(A,B))),A)),B)), |
|
29c6cba140da
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
mengj
parents:
diff
changeset
|
7 |
++equal(typeinfo(F,tc_fun(A,B)),typeinfo(G,tc_fun(A,B)))]). |