introduces: item . 

item = ž .
open .

introduces: flat-list, list of _  .

needs:      Tuples/Basics.  item <= component .
flat-list = list of item* .
list of _ ::item* -> flat-list (total, injective) . 
(1)  item & flat-list = nothing . 

closed except Generics .

introduces:  _[ _ ] , items_ , head_ , tail_ , empty-list , concatenation_ . 

includes:    Instant/Distinction ( list for s , _is_ ) . 

needs:       Tuples . flat-list <= component . 

 _[ _ ]		:: flat-list, item -> flat-list .
 items_		:: flat-list -> item* (total, injective) .
 head_		:: flat-list -> item (partial) .
 tail_		:: flat-list -> flat-list (partial) .
 empty-list	 : flat-list .
 concatenation_	:: flat-list* -> flat-list (total, associative, unit is empty-list). 
needs:	Numbers/Naturals .

(1) (l <= flat-list) [i <= item ] = l & list of i* .
(2) l = list of i => items l:flat-list = i . 
(3) head of l:flat-list = component#1 items l . 
(4) tail of l:flat-list = list of components from #2 items l . 
(5) empty-list = list of ( ) . 
(6) concatenation (l1:flat-list, l2:flat-list) = list of (items l1, items l2). 
(7) l1:flat-list is l2:flat-list = items l1 is items l2 .

introduces: leaf . 
leaf = item | ž .
open .

introduces: list ,tree . 

needs:     Tuples/Basics . tree <= component .
 list 		= list of tree* .
 tree 		= leaf | list (disjoint) .
 list of_ 	:: tree* -> list (total, injective) . 
closed except Generics .

introduces: _ [ _ ], branches_, leaves_, head _, tail _ , empty-list, concatenation_ .

includes:   Instant/Distinction ( tree for s , _is_ ) .

needs:      Tuples .
_ [ _ ]		:: list, tree -> list . 
branches_		:: list -> tree* (total, injective) . 
leaves_		:: tree* -> leaf* (total) .
head_		:: list -> tree (partial) .
tail_ 		:: list -> list (partial) . 
empty-list	 : list .
concatenation_	:: list* -> list  (total, associative, unit is empty-list) .
needs:  Numbers/Naturals .

(1) (l <= list) [ t <= tree ]	= l&list of t* .
(2) branches list of t:tree*	= t .
(3) leaves l:leaf = l ; leaves list of t:tree* = leaves t .    
	leaves ( ) = ( ) ;  leaves (t1:tree*, t2:tree*) =
		(leaves t1, leaves t2) .
(4) head l:list = component#1 branches l .
(5) tail l:list = list of components from #2 branches l .
(6) empty-list = list of ( ) .
(7) concatenation (l1:list, l2:list) = list of (branches l1, branches l2) .
(8) l1:list is l2:list = branches l1 is branches l2 ;
    	x:leaf is l:list = false .