16 TF_of_list :: "i=>i" |
16 TF_of_list :: "i=>i" |
17 |
17 |
18 rules |
18 rules |
19 TF_rec_def |
19 TF_rec_def |
20 "TF_rec(z,b,c,d) == Vrec(z, \ |
20 "TF_rec(z,b,c,d) == Vrec(z, \ |
21 \ %z r. tree_forest_case(%x tf. b(x, tf, r`tf), \ |
21 \ %z r. tree_forest_case(%x f. b(x, f, r`f), \ |
22 \ c, \ |
22 \ c, \ |
23 \ %t tf. d(t, tf, r`t, r`tf), z))" |
23 \ %t f. d(t, f, r`t, r`f), z))" |
24 |
24 |
25 list_of_TF_def |
25 list_of_TF_def |
26 "list_of_TF(z) == TF_rec(z, %x tf r. [Tcons(x,tf)], [], \ |
26 "list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [], \ |
27 \ %t tf r1 r2. Cons(t, r2))" |
27 \ %t f r1 r2. Cons(t, r2))" |
28 |
28 |
29 TF_of_list_def |
29 TF_of_list_def |
30 "TF_of_list(tf) == list_rec(tf, Fnil, %t tf r. Fcons(t,r))" |
30 "TF_of_list(f) == list_rec(f, Fnil, %t f r. Fcons(t,r))" |
31 |
31 |
32 TF_map_def |
32 TF_map_def |
33 "TF_map(h,z) == TF_rec(z, %x tf r.Tcons(h(x),r), Fnil, \ |
33 "TF_map(h,z) == TF_rec(z, %x f r.Tcons(h(x),r), Fnil, \ |
34 \ %t tf r1 r2. Fcons(r1,r2))" |
34 \ %t f r1 r2. Fcons(r1,r2))" |
35 |
35 |
36 TF_size_def |
36 TF_size_def |
37 "TF_size(z) == TF_rec(z, %x tf r.succ(r), 0, %t tf r1 r2. r1#+r2)" |
37 "TF_size(z) == TF_rec(z, %x f r.succ(r), 0, %t f r1 r2. r1#+r2)" |
38 |
38 |
39 TF_preorder_def |
39 TF_preorder_def |
40 "TF_preorder(z) == TF_rec(z, %x tf r.Cons(x,r), Nil, %t tf r1 r2. r1@r2)" |
40 "TF_preorder(z) == TF_rec(z, %x f r.Cons(x,r), Nil, %t f r1 r2. r1@r2)" |
41 |
41 |
42 end |
42 end |