1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
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)))) )).
|
