Problem:
 f x -> g x
 g x -> h x
 a -> b

Proof:
 Modularity Decomposition: 
 0:f x -> g x
   g x -> h x
 1:a -> b
 -----
 0:f x -> g x
   g x -> h x
   Higher-Order Church Rosser Processor:
    f x -> g x
    g x -> h x
    critical peaks: 0
     
     
     Higher-Order Closedness Processor:
       all critical pairs are trivial
      
      Qed
   
   
   1:a -> b
     Higher-Order Church Rosser Processor:
      a -> b
      critical peaks: 0
       
       
       Higher-Order Closedness Processor:
         all critical pairs are trivial
        
        Qed