| changeset 33010 | 39f73a59e855 |
| 33008:b0ff69f0a248 | 33010:39f73a59e855 |
|---|---|
1 (benchmark Isabelle |
|
2 :extrasorts ( T2 T1) |
|
3 :extrafuns ( |
|
4 (uf_2 T1) |
|
5 (uf_3 T2) |
|
6 (uf_4 T1) |
|
7 ) |
|
8 :extrapreds ( |
|
9 (up_1 T1 T2) |
|
10 ) |
|
11 :assumption (forall (?x1 T1) (?x2 T2) (iff (up_1 ?x1 ?x2) (= ?x1 uf_2))) |
|
12 :assumption (iff (forall (?x3 T1) (exists (?x4 T2) (up_1 ?x3 ?x4))) (forall (?x5 T1) (up_1 ?x5 uf_3))) |
|
13 :assumption (not (iff (exists (?x6 T2) (up_1 uf_4 ?x6)) (up_1 uf_4 uf_3))) |
|
14 :formula true |
|
15 ) |