16 |
16 |
17 rules |
17 rules |
18 |
18 |
19 sorted1_Nil "sorted1(f,[])" |
19 sorted1_Nil "sorted1(f,[])" |
20 sorted1_One "sorted1(f,[x])" |
20 sorted1_One "sorted1(f,[x])" |
21 sorted1_Cons "sorted1(f,Cons(x,Cons(y,zs))) = (f(x,y) & sorted1(f,Cons(y,zs)))" |
21 sorted1_Cons "sorted1(f,Cons(x,y#zs)) = (f(x,y) & sorted1(f,y#zs))" |
22 |
22 |
23 sorted_Nil "sorted(le,[])" |
23 sorted_Nil "sorted(le,[])" |
24 sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))" |
24 sorted_Cons "sorted(le,x#xs) = ((Alls y:xs. le(x,y)) & sorted(le,xs))" |
25 |
25 |
26 mset_Nil "mset([],y) = 0" |
26 mset_Nil "mset([],y) = 0" |
27 mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))" |
27 mset_Cons "mset(x#xs,y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))" |
28 |
28 |
29 total_def "total(r) == (!x y. r(x,y) | r(y,x))" |
29 total_def "total(r) == (!x y. r(x,y) | r(y,x))" |
30 transf_def "transf(f) == (!x y z. f(x,y) & f(y,z) --> f(x,z))" |
30 transf_def "transf(f) == (!x y z. f(x,y) & f(y,z) --> f(x,z))" |
31 end |
31 end |