29 Rep_Forest :: 'a forest => 'a item |
29 Rep_Forest :: 'a forest => 'a item |
30 Abs_Forest :: 'a item => 'a forest |
30 Abs_Forest :: 'a item => 'a forest |
31 Tcons :: ['a, 'a forest] => 'a tree |
31 Tcons :: ['a, 'a forest] => 'a tree |
32 Fcons :: ['a tree, 'a forest] => 'a forest |
32 Fcons :: ['a tree, 'a forest] => 'a forest |
33 Fnil :: 'a forest |
33 Fnil :: 'a forest |
34 TF_rec :: "['a item, ['a item , 'a item, 'b]=>'b, |
34 TF_rec :: ['a item, ['a item , 'a item, 'b]=>'b, |
35 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b" |
35 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b |
36 tree_rec :: "['a tree, ['a, 'a forest, 'b]=>'b, |
36 tree_rec :: ['a tree, ['a, 'a forest, 'b]=>'b, |
37 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b" |
37 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b |
38 forest_rec :: "['a forest, ['a, 'a forest, 'b]=>'b, |
38 forest_rec :: ['a forest, ['a, 'a forest, 'b]=>'b, |
39 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b" |
39 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b |
40 |
40 |
41 defs |
41 defs |
42 (*the concrete constants*) |
42 (*the concrete constants*) |
43 TCONS_def "TCONS M N == In0(M $ N)" |
43 TCONS_def "TCONS M N == In0(M $ N)" |
44 FNIL_def "FNIL == In1(NIL)" |
44 FNIL_def "FNIL == In1(NIL)" |