diff options
Diffstat (limited to 'test/regress/regress0/tptp/tff0-arith.p')
| -rw-r--r-- | test/regress/regress0/tptp/tff0-arith.p | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/test/regress/regress0/tptp/tff0-arith.p b/test/regress/regress0/tptp/tff0-arith.p new file mode 100644 index 000000000..c0e9af25a --- /dev/null +++ b/test/regress/regress0/tptp/tff0-arith.p @@ -0,0 +1,27 @@ +% example from the TFF0 paper +% see https://sites.google.com/site/polymorphictptptff/relevant-links/tff-tfa +% +% Status : Theorem +% +tff(list_type,type, ( list: $tType )). +tff(nil_type,type, ( nil: list )). +tff(mycons_type,type,( mycons: ( $int * list ) > list )). +tff(sorted_type,type,( fib_sorted: list > $o )). + +tff(empty_fib_sorted,axiom,( + fib_sorted(nil) )). +tff(single_is_fib_sorted,axiom,( + ! [X: $int] : fib_sorted(mycons(X,nil)) )). +tff(double_is_fib_sorted_if_ordered,axiom,( + ! [X: $int,Y: $int] : + ( $less(X,Y) + => fib_sorted(mycons(X,mycons(Y,nil))) ) )). +tff(recursive_fib_sort,axiom,( + ! [X: $int,Y: $int,Z: $int,R: list] : + ( ( $less(X,Y) + & $greatereq(Z,$sum(X,Y)) + & fib_sorted(mycons(Y,mycons(Z,R))) ) + => fib_sorted(mycons(X,mycons(Y,mycons(Z,R)))) ) )). + +tff(check_list,conjecture,( + fib_sorted(mycons(1,mycons(2,mycons(4,nil)))) )). |