{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses,
             RecursiveDo #-}

-- 24.12.2020

module Lazy where

import Control.Monad (msum)

foo1 :: [a1] -> Int
foo1 (x:s) = 1
foo1 _     = undefined
foo2 ~(x:s) = 1

foo3 (x,y)  = 1
foo4 ~(x,y) = 1

foo5 x = 1 where (y,z) = x
foo6 x = let (y,z) = x in 1

foo7 (x:s) = if x > 10 then s else undefined

pair = (8,9)
(x,y) = pair

fix :: (a -> a) -> a
fix f = x where x = f x

fix1 = take 11 $ fix (1:)

-- INFINITE OBJECTS

nats n = n:map (+1) (nats n)

fibs = 0:zipWith (+) fibs (1:fibs)
							
-- take 12 fibs    -->   [0,1,1,2,3,5,8,13,21,34,55,89]

fibs1 = 1:1:zipWith (+) fibs1 (tail fibs1)
							
-- take 12 fibs1   -->   [1,1,2,3,5,8,13,21,34,55,89,144]

fibs2@(1:tfibs) = 1:1:zipWith (+) fibs2 tfibs
							
-- take 12 fibs2   -->   [1,1,2,3,5,8,13,21,34,55,89,144]

concfibs = 0:concat fibs where fibs = [1]:tailfibs
	                       tailfibs = [0]:zipWith (++) tailfibs fibs
			       
concfibs2 n = fibs n where fibs 0 = [1]
	                   fibs 1 = [0]
			   fibs n = fibs (n-1)++fibs (n-2)
	    {- (fibs,concfibs) = (fibs,concfibs2 infinity)
	       is the unique solution of the equations
	       f (0:s) = 0:1:f s
	       f (1:s) = 1:f s
	       f fib   = fib   (<==> exists gib : fib = 0:gib /\ gib = 1:f(gib))
	       in (fib,f)
	       see: H. Zantema, Well-definedness of streams,...
	            and http://www.win.tue.nl/~hzantema/strfib.html -}

primes :: [Integer]
primes = sieve $ nats 2 

sieve (p:s) = p:sieve [n | n <- s, n `mod` p /= 0]
sieve _     = []

-- take 11 prims   ===>   [2,3,5,7,11,13,17,19,23,29,31]

mirps :: Int -> [Integer]
mirps upb = filter ((`elem` prims) . f) prims 
	    where prims = sieve $ take upb $ nats 2
	          f = read . reverse . show

-- take 999 mirps   
-- ===> [2,3,5,7,11,13,17,31,37,71,73,79,97,101,107,113,131,149,151,157,167,179,
--       181,191,199,311,313,337,347,353,359,373,383,389,701,709,727,733,739,
--	 743,751,757,761,769,787,797,907,919,929,937,941,953,967,971,983,991]

hamming = 1:foldl1 merge (map (\x -> map (*x) hamming) [2,3,5])
          
merge s1@(x:s2) s3@(y:s4) = if x < y then x:merge s2 s3 
			    else if x > y then y:merge s1 s4 else merge s1 s4
merge [] s 		  = s
merge s _  		  = s

-- take 30 hamming   ===>  [1,2,3,4,5,6,8,9,10,12,15,16,18,20,24,25,27,30,32,36,
--                          40,45,48,50,54,60,64,72,75,80]

hamming' = 1:map (*2) hamming`join`map (*3) hamming`join`map (*5) hamming

join s (x:s') = if x `elem` s then join s s' else x:join s s'
join s _      = s

joinMap :: Eq b => (a -> [b]) -> [a] -> [b]
joinMap = (foldl join [] .) . map

seqMap :: [a -> b] -> [a] -> [b]                       
seqMap fs = zipWith ($) fsp where fsp = fs++fsp

testsm = seqMap [(+1),(+3),(+7)] [1..9] -- > [2,5,10,5,8,13,8,11,16]

star1,star2,star3 :: [a] -> [[a]]

star1 alphabet = concatMap power [0..]
		 where power 0 = [[]]
		       power n = [x:xs | x <- alphabet, xs <- power $ n-1]

star2 alphabet = xss where xss = []:[x:xs | xs <- xss, x <- alphabet]

star3 alphabet = xss where xss = []:[x:xs | x <- alphabet, xs <- xss]	-- bad

test1 = take 111 $ star1 [1..5]
test2 = take 111 $ star2 [1..5]
test3 = take 111 $ star3 [1..5]

-- SAB grammar as iterative equations

infixr 6 ***

vs***ws = [v++w | v <- vs, w <- ws]

xS = "":["a"]***xB++["b"]***xA		-- xS accepts words with the same
xA = ["a"]***xS++["b"]***xA***xA	-- number of a's and b's
xB = ["b"]***xS++["a"]***xB***xB

test4 = "ababab" `elem` xS -- > True
test5 = take 9 xS      -- > ["","ab","abab","ababab","abababab","ababababab",
	               -- >  "abababababab","ababababababab","abababababababab"] 
test6 = take 9 [w | w <- xS, length w < 5]

sortLg :: [[a]] -> [[a]]
sortLg (x:s) = sortLg [z | z <- s, length z <= length x]++x:
	       sortLg [z | z <- s, length z > length x]
sortLg s     = s

-- MERGESORT

mergesort (x:y:s) = merge (mergesort $ x:s1) (mergesort $ y:s2) 
   		    where (s1,s2) = split s
mergesort s      = s
   
split (x:y:s) = (x:s1,y:s2) where (s1,s2) = split s
split s       = (s,[])

mergesortF (x:y:s) = (\(s1,s2) -> merge (mergesortF $ x:s1) (mergesortF $ y:s2))
		     $ splitF s
mergesortF s       = s

splitF (x:y:s) = (\(s1,s2) -> (x:s1,y:s2)) $ splitF s
splitF s       = (s,[])

-- PALINDROMES

pal,palF,palI :: Eq a => [a] -> Bool    

pal s = b where (r,b) = revEq s r   	    -- = let (r,b) = revEq s r in b   

revEq :: Eq a => [a] -> [a] -> ([a],Bool)   -- revEq s1 s2 = (reverse s1,s1==s2)

revEq [] s'    = ([],True)
revEq (x:s) s' = (fst pair++[x],x == head s' && snd pair) 
				            where pair = revEq s $ tail s'  
{-               (r++[x],x == head s' && b) where (r,b) = revEq s $ tail s'
                 (\(r,b) -> (r++[x],x == head s' && b)) $ revEq s $ tail s'
                 (r++[x],x==y && b) where y:s' = s
                 		          (r,b) = revEq s s'
                 let y:s' = s; (r,b) = revEq s s' in (r++[x], x==y && b) 
revEq (x:s) ~(y:s') = (r++[x],x==y && b) where (r,b) = revEq s s'
revEq (x:s) (y:s')  = (r++[x],x==y && b) where (r,b) = revEq s s'
                      loops if called by pal -}

palF s = f r where (r,f) = revEqF s

revEqF :: Eq a => [a] -> ([a],[a] -> Bool)
revEqF []     = ([],const True)
revEqF (x:s) = (r++[x],\(y:s') -> x==y && f s') where (r,f) = revEqF s

palI s = b where (r,b) = revEqI s r []		   -- revEqI s s' acc =
						   -- (reverse s++acc,s==s')
revEqI :: Eq a => [a] -> [a] -> [a] -> ([a],Bool)  
revEqI [] _ acc     = (acc,True)		   	
revEqI (x:s) s' acc = (r, x == head s' && b) 
		      where (r,b) = revEqI s (tail s') $ x:acc

-- pal/F/I [1,2,3,2,1] ---> True

pal1 = pal $ take 12 (nats 22) ++ reverse (take 12 $ nats 22)	      -- > True
pal2 = pal $ take 12 (nats 22) ++ 111:reverse (take 12 $ nats 22)     -- > True
pal3 = pal $ take 12 (nats 22) ++ 111:114:reverse (take 12 $ nats 22) -- > False

-- BINARY TREES

data Btree a = L a | Btree a :# Btree a

tree1 = (L 3:#(L 22:#L 4)):#(L 2:#L 11)
tree2 = (L 3:#(L 22:#L 4)):#((L 5:#L 16):#L 11)
tree3 = (L 3:#(L 22:#L 4)):#((L 3:#(L 22:#L 5)):#(L 2:#L 11))

instance Show a => Show (Btree a) 
		   where show (L a)    = show a
		   	 show (t1:#t2) = '(':show t1++'#':show t2++")"

depfront :: Ord a => Btree a -> ([a],Int)  -- depfront t x = (front t x,depth t)
depfront (L x)    = ([x],0)
depfront (t1:#t2) = (if x > y then xs else if y > x then ys else xs++ys,
		     max x y+1)
                    where (xs,x) = depfront t1
                          (ys,y) = depfront t2

-- depfront tree2 ---> ([22,4,5,16],3)
-- depfront tree3 ---> ([22,5],4)
			 			  
replace :: (a -> a -> a) -> Btree a -> Btree a
replace f t = u where (x,u) = foldRep f t x

-- replace f t = let (x,u) = foldRep f t x in u

foldRep :: (a -> a -> a) -> Btree a -> a -> (a,Btree a)
foldRep _ (L x) y    = (x,L y)     -- foldRep f t x = (foldT f t,t[x/leaves(t)])
foldRep f (t1:#t2) x = (f y z,u1:#u2) where (y,u1) = foldRep f t1 x
			                    (z,u2) = foldRep f t2 x

-- replace min tree1 ---> ((2#(2#2))#(2#2))
-- replace (+) tree1 ---> ((42#(42#42))#(42#42))
			 			  
replaceM,replaceMS :: (a -> a -> a) -> Btree a -> Maybe (Btree a)

replaceM f t  = do rec (x,u) <- foldRepM f t x
                   Just u

replaceMS f t = do rec (x,u) <- foldRepMS f t x
                   Just u

foldRepM,foldRepMS :: (a -> a -> a) -> Btree a -> a -> Maybe (a,Btree a)

foldRepM _ (L x) y    = Just (x,L y)
foldRepM f (t1:#t2) x = do (y,u1) <- foldRepM f t1 x
			   (z,u2) <- foldRepM f t2 x
			   Just (f y z,u1:#u2)
			    
foldRepMS f t x = msum [do L y <- Just t; Just (y,L x),
		        do t1:#t2 <- Just t
			   (y,u1) <- foldRepMS f t1 x
			   (z,u2) <- foldRepMS f t2 x
			   Just (f y z,u1:#u2)]

-- replaceM/S min tree1 ---> Just ((2#(2#2))#(2#2))
-- replaceM/S (+) tree1 ---> Just ((42#(42#42))#(42#42))

-- TREE SORTING

sortT,sortTF,sortTI :: Ord a => Btree a -> Btree a

sortT t = u where (ls,u,_) = leavesRep t $ sort ls

leavesRep :: Btree a -> [a] -> ([a],Btree a,[a])
leavesRep (L x) s    = ([x],L $ head s,tail s) 
                    -- ([x],L y,s') where y:s' = s
leavesRep (t1:#t2) s = (ls1++ls2,u1:#u2,s2) where (ls1,u1,s1) = leavesRep t1 s
			       	  		  (ls2,u2,s2) = leavesRep t2 s1
	         -- leavesRep t s = (leaves(t),t[take(n,s)/leaves(t)],drop(n,s))
	         --                 where n = length $ leaves t

sortTF t = fst $ f $ sort s where (s,f) = leavesRepF t

leavesRepF :: Btree a -> ([a],[a] -> (Btree a,[a]))
leavesRepF (L x)    = ([x],\(y:s) -> (L y,s))
leavesRepF (t1:#t2) = (ls1++ls2,\s -> case f1 s of 
				           (u1,s1) -> case f2 s1 of 
						      (u2,s2) -> (u1:#u2,s2))
			              where (ls1,f1) = leavesRepF t1
			                    (ls2,f2) = leavesRepF t2
			      
sortTI t = u where (ls,u,_) = leavesRepI t (sort ls) []

leavesRepI :: Btree a -> [a] -> [a] -> ([a],Btree a,[a])
       -- leavesRepI t s acc = (t[take(n,s)/leaves(t)],drop(n,s),leaves(t)++acc)
       --                       where n = length $ leaves t
leavesRepI (L x) s acc    = (x:acc,L $ head s,tail s) 
                         -- (x:acc,L y,s') where y:s' = s
leavesRepI (t1:#t2) s acc = (ls2,u1:#u2,s2)
			     where (ls1,u1,s1) = leavesRepI t1 s acc
			       	   (ls2,u2,s2) = leavesRepI t2 s1 ls1

-- sortT/F/I tree3 ---> ((2#(3#3))#((4#(5#11))#(22#22)))
				     
sort :: Ord a => [a] -> [a] 
sort (x:s) = sort [z | z <- s, z <= x]++x:sort [z | z <- s, z > x]
sort s     = s

-- CLIENT-SERVER INTERACTION

csi :: (a -> b) -> (b -> a) -> a -> [a]
csi f g a = requests where requests = client a $ map f $ requests 
            		   client a s = a:client (g $ head s) (tail s) 
{- 
client g a (b:s)  = a:client g (g b) s         does not terminate 
client g a bs     = a:client g (g b) s where b:s = bs
client g a bs     = let b:s = bs in a:client g (g b) s
client g a ~(b:s) = a:client g (g b) s -}
			    
cs1 = take 11 $ iterate ((*2) . (+1)) 0 			    
cs2 = take 11 $ csi (+1) (*2) 0      -- > [0,2,6,14,30,62,126,254,510,1022,2046]

-- LAZY MULTIPLICATION

mulL 0 _ = 0
mulL x y = x*y

foo x = if x == 0 then 0 else foo (x-1) `mulL` foo (x+1) 	

mulR _ 0 = 0
mulR x y = x*y

goo x = if x == 0 then 0 else goo (x+1) `mulR` foo (x-1) 

{- Expander2 specification with some of the above functions

constructs: leaf #
defuncts:   is_even mergesortL splitL mergeL mergesort split merge
	    mergesortF splitF mergeF replaceL replace foldRepL foldRep
            palL pal palLI palF reveqL reveqLI reveq reveqI reveqF 
	    sortTL sortT sortTI leavesRepL leavesRep leavesRepI 
	    foo goo nats nats' fibs fibs'  
	    RequestsL ClientL Requests Client CSI || tree1 tree2 tree3
preds:      even odd 
fovars:     t u r a b b1 b2 rb rc requests acc t1 t2 u1 u2 s1 s2 ls ls1 ls2
hovars:     f g h client

axioms:

(even$0 <==> True) &
(even$suc$x <==> odd$x) &
(odd$x <==> Not(even$x)) &

is_even == fun(x||even$x,1,x||odd$x,0) &

-- MERGESORT

(mergesortL(x:y:s) = mergeL(mergesortL$x:s1)$mergesortL$y:s2
   		     <=== splitL$s = (s1,s2)) & 
mergesortL[x] = [x] &
mergesortL[]  = [] &
   
(splitL$x:y:s = (x:s1,y:s2) <=== splitL$s = (s1,s2)) &
splitL[x] = ([x],[]) &
splitL[]  = ([],[]) &

(mergeL(x:s,y:s') = x:mergeL(s,y:s') <=== x <= y) &
(mergeL(x:s,y:s') = y:mergeL(x:s,s') <=== x > y) &
mergeL([],s) = s &
mergeL(s,[]) = s &

(split$s = (s1,s2) 
             ==> mergesort$x:y:s == merge(mergesort$x:s1,mergesort$y:s2)) &
mergesort(s) == s &

(split$s = (s1,s2) ==> split$x:y:s == (x:s1,y:s2)) &
split$s == (s,[]) &

(x <= y ==> merge(x:s,y:s') == x:merge(s,y:s')) &
merge(x:s,y:s') == y:merge(x:s,s') &
merge([],s)     == s &
merge(s,[])     == s &

mergesortF(x:y:s) == fun((s1,s2),mergeF(mergesortF$x:s1)$mergesortF$y:s2)
			$splitF$s &
mergesortF[x] == [x] &
mergesortF[]  == [] &

splitF(x:y:s) == fun((s1,s2),(x:s1,y:s2))$splitF$s &
(length(s) <= 1 ==> splitF(s) == (s,[])) &

mergeF(x:s)$y:s' == ite(x<=y,x:mergeF(s)$y:s',y:mergeF(x:s)$s') &
mergeF[]$s       == s &
mergeF(s)[]      == s &

-- PALINDROMES

(palL$s = b <=== reveqL(s)$r = (r,b)) &  
					
reveqL[]$s        = ([],1) &         
(reveqL(x:s)$y:s' = (r++[x],bool(x=y)*b) <=== reveqL(s)$s' = (r,b)) &

(palLI$s = b <=== reveqLI(s)(r)[] = (r,b)) &  
					
reveqLI[](s)$acc = (acc,1) &        
(reveqLI(x:s)(y:s')$acc = (r,bool(x=y)*b) <=== reveqLI(s)(s')$x:acc = (r,b)) &

pal$s == get1$mu rb.reveq(s)(get0$rb) &       -- reveq(s)$s' = (reverse$s,s=s')

reveq[]$s == ([],1) &
reveq(x:s)$s' == fun((r,b),(r++[x],bool(x=head$s')*b))$reveq(s)$tail$s' &

-- (reveq(s)$tail$s' = (r,b) 						slow
--       ==> reveq(x:s)$s' == (r++[x],bool(x=head$s')*b)) &  		

palI$s == get1$mu rb.reveqI(s)(get0$rb)[] & 
			         -- revEqI(s)(s')$acc = (reverse(s)++acc,s=s')

reveqI[](s)$acc == (acc,1) &
reveqI(x:s)(s')$acc == fun((r,b),(r,bool(x=head$s')*b))
                       $reveqI(s)(tail$s')$x:acc &

-- (reveqI(s)(tail$s')$x:acc = (r,b) 					slow
--	            ==> reveqI(x:s)(s')$acc == (r,bool(x=head$s')*b)) &

(reveqF$s = (r,f) ==> palF$s == f$r) &

reveqF[] == ([],fun(s,1)) &
reveqF$x:s == (get0(reveqF$s)++[x],fun(y:s',bool(x=y)*(get1(reveqF$s)$s'))) &

-- BINARY TREES

tree1 == leaf(3)#(leaf(2)#leaf(6)) &

tree2 == (leaf(9)#leaf(3))#leaf(2) &

tree3 == (leaf(9)#leaf(3))#(leaf(2)#leaf(6)) &

(replaceL(f)$t = u <=== foldRepL(f)(t)$x = (x,u)) &

foldRepL(f)(leaf$x)$y  = (x,leaf$y) &
(foldRepL(f)(t1#t2)$x  = (f(y,z),u1#u2) <=== foldRepL(f)(t1)$x = (y,u1) & 
					     foldRepL(f)(t2)$x = (z,u2)) &

replace(f)$t == get1$mu x u.foldRep(f)(t)(x) &

foldRep(f)(leaf$x)$y == (x,leaf(y)) &
(foldRep(f)(t1)$x = (y,u1) & foldRep(f)(t2)$x = (z,u2) 
		     ==> foldRep(f)(t1#t2)$x == (f(y,z),u1#u2)) &

(sortTL$t = u <=== leavesRepL(t)(sort$ls) = (ls,u,s)) &

(leavesRepL(leaf$x)$ls = ([x],leaf$y,s) <=== ls = y:s) &
(leavesRepL(t1#t2)$ls  = (ls1++ls2,u1#u2,s2) 
      			 <=== leavesRepL(t1)$ls = (ls1,u1,s1) & 
			      leavesRepL(t2)$s1 = (ls2,u2,s2)) &

sortT$t == get1$mu ls u s.leavesRep(t)(sort$ls) &

leavesRep(leaf$x)$ls == ([x],leaf$head$ls,tail$ls) &
(leavesRep(t1)$ls = (ls1,u1,s1) & leavesRep(t2)$s1 = (ls2,u2,s2)
   		==> leavesRep(t1#t2)$ls == (ls1++ls2,u1#u2,s2)) &

sortTI$t == get1$mu ls u s.leavesRepI(t)(sort$ls)[] &

leavesRepI(leaf$x)(ls)$acc == (x:acc,leaf$head$ls,tail$ls) &
(leavesRepI(t1)(ls)$acc = (ls1,u1,s1) & leavesRepI(t2)(s1)$ls1 = (ls2,u2,s2)
                ==> leavesRepI(t1#t2)(ls)$acc == (ls2,u1#u2,s2)) &
	     
-- INFINITE OBJECTS

nats  == 0:map(+1)$nats &

nats' == mu s.(0:map(+1)$s) &
	     
natsf == mu f.fun(n,n:f$n+1) &		   -- nats = natsf$0

fibs  == 1:1:zipWith(+)(fibs)$tail$fibs &  -- simplify breadthfirst/parallel

fibs' == mu s.(1:1:zipWith(+)(s)$tail$s) & -- simplify breadthfirst/parallel

-- CLIENT-SERVER INTERACTION

RequestsL(f)(g) = ClientL(g)(0).map(f).RequestsL(f)(g) &

(ClientL(g)(a)$s = a:ClientL(g)(g$b)$s' <=== s = b:s') &

Requests(f)(g)$a == Client(g)(a)$map(f)$Requests(f)(g)$a &

Client(g)(a)$s == a:Client(g)(g$head$s)$tail$s &

CSI(f)(g)$a == get0$mu rc.(get1(rc)(a)$map(f)$get0$rc,
                           fun(a,fun(s,a:get1(rc)(g$head$s)$tail$s))) &

-- LAZY MULTIPLICATION

foo(x) == ite(x=0,0,foo(x-1)*foo(x+1)) &
goo(x) == ite(x=0,0,goo(x+1)*goo(x-1))

theorems:

Any b b1 b2 s:map(h)$RequestsL(f)(g)$a = b:b1:b2:s     -- (*)

conjects:

mergesortL[3,2,1,4] = s 		   &   -- match and narrow
replaceL(min)$tree1 = t  		   &   -- match and narrow
replaceL(+)$tree1 = t  		           &   -- match and narrow

palL[1,1] = b 				   &   -- unify and narrow, simpl
				                   -- 4 steps           (9.3.20)      
palL[1,2] = b 				   &   -- unify and narrow, simpl
				                   -- 4 steps           (9.3.20)      
palL[2,3,2] = b 			   &   -- unify and narrow, simpl
				                   -- 5 steps         (30.10.20)      
palL[2,3,1,2] = b			   &   -- unify and narrow, simpl

palLI[2,3,2] = b 			   &   -- unify and narrow, simpl
				                   -- 5 steps          (24.1.21)      
palLI[2,3,2,1] = b 			   &   -- unify and narrow, simpl
				                   -- 6 steps          (24.1.21)      
sortTL$tree1 = t              	           &   -- match and narrow, simpl
				                   -- 6 steps          (24.1.21)      
take(3)$RequestsL(+1)(*2)(0) = s               -- match and narrow, simpl
				  	           -- 14 steps         (25.1.21)  
    						   -- uses (*)
terms: 

mergesort[3,2,1,4] 			       <+>
mergesortF[3,2,1,4] 			       <+>

replace(min)$tree1   		               <+> 
replace(+)$tree1   		               <+> 

pal[1,1] 			       	       <+> -- 22 steps        (31.12.20)
pal[1,2] 			       	       <+> -- 16 steps        (31.12.20)
pal[2,3,2] 			       	       <+> -- 24 steps         (18.3.20)
pal[2,3,3]                                     <+> -- 20 steps         (18.3.20)
pal[2,3,1,2]                                   <+> -- 29 steps        (31.12.20)
pal[2,3,3,2]                                   <+> -- 45 steps        (31.12.20)

palI[2,3,2] 			       	       <+> -- 19 steps         (22.1.21)
palI[2,3,2,1]                                  <+> -- 22 steps         (22.1.21)
palI[1,2,3,2,1]                                <+> -- 25 steps         (22.1.21)				
palF[2,3,2] 			       	       <+> -- 12 steps         (22.1.21)
palF[2,3,1,2] 			       	       <+> -- 9 steps          (18.3.20)
						   
sortT$tree1	       			       <+> -- 13 steps         (16.2.20)
sortT$tree2	       			       <+> -- 15 steps         (16.2.20)
sortT$tree3	       			       <+> -- 16 steps         (16.2.20)
						   
sortTI$tree1	      			       <+> -- 11 steps          (4.2.20)
sortTI$tree2	      			       <+> -- 11 steps          (4.2.20)
sortTI$tree3	      			       <+> -- 12 steps          (5.2.20)
						   
take(3)$nats			      	       <+> -- 21 steps         (1.11.17)

take(3)$nats'  			               <+> -- 22 steps         (1.11.17)

take(3)$Requests(+1)(*2)$0		       <+> --> [0,2,6]	      
						   -- 30 steps        (26.10.20)
take(4)$Requests(+1)(*2)$0		       <+> --> [0,2,6,14]
						   -- 47 steps        (26.10.20)
take(5)$Requests(+1)(*2)$0                     <+> --> [0,2,6,14,30]   
						   -- 66 steps         (10.2.20)
take(6)$Requests(+1)(*2)$0                     <+> --> [0,2,6,14,30,62]
						   -- 89 steps         (10.2.20)
take(3)$CSI(+1)(*2)$0                          <+> --> [0,2,6]
 						   -- 50 steps paral   (22.1.21)
 						   -- 52 steps df/bf   (22.1.21)
take(4)$CSI(+1)(*2)$0                          <+> --> [0,2,6,14]
 						   -- 93 steps paral   (23.1.21)

foo(3)					       <+> --> 0		
                  -- 15 depthfirst, 19 parallel, 27 breadthfirst steps  (4.2.20)
goo(3)					           --> 0	       
  -- depthfirst is non-terminating, 19 parallel, 48 breadthfirst steps  (4.2.20)
-}