babyCalculusEqations.hs

d/dx (x ^ a) == d/dx (a -> x )

we never consider a ^ x  === x -> a ()



log_x(\nu Y -> T) ==  \mu Z  -> log_X T ,  where Z == log_X Y 
(translation: every time we see log_X Y , in T, replace taht with Z )

F   ===  Y |->  X * Y
Stream X == \nu (F     ) == \nu Y |->  X * Y  

log_X (Stream X) == log_X (\nu F) == log_X (\nu Y |-> X * Y)

      log and fixpoint exchange
      == \mu (W |-> log_X (X * W)) == \mu (W |-> log_X(X) + Log_X(W) ) == \mu (W  |-> 1 + log_X W ) 


      replaced W

codata Stream x = x * Stream x 

codata LogCo x = Log_x (Stream x) ==
type LogCo =    x |-> Log_x (Stream x) 
            == x |-> Log_x (\NUUU Y |-> x * Y)