Problem:
 not true -> false
 not false -> true
 fold (\x. F x) (\x. G x) z nil -> z
 fold (\x. F x) (\x. G x) z (0 y) -> fold (\x. F x) (\x. G x) (F z) y
 fold (\x. F x) (\x. G x) z (1 y) -> fold (\x. F x) (\x. G x) (G z) y

Proof:
 Modularity Decomposition: 
 0:not true -> false
   not false -> true
 1:fold (\x. F x) (\x. G x) z nil -> z
   fold (\x. F x) (\x. G x) z (0 y) -> fold (\x. F x) (\x. G x) (F z) y
   fold (\x. F x) (\x. G x) z (1 y) -> fold (\x. F x) (\x. G x) (G z) y
 -----
 0:not true -> false
   not false -> true
   Higher-Order Church Rosser Processor:
    not true -> false
    not false -> true
    critical peaks: 0
     
     
     Higher-Order Closedness Processor:
       all critical pairs are trivial
      
      Qed
   
   
   1:fold (\x. F x) (\x. G x) z nil -> z
     fold (\x. F x) (\x. G x) z (0 y) -> fold (\x. F x) (\x. G x) (F z) y
     fold (\x. F x) (\x. G x) z (1 y) -> fold (\x. F x) (\x. G x) (G z) y
     Higher-Order Church Rosser Processor:
      fold (\x. F x) (\x. G x) z nil -> z
      fold (\x. F x) (\x. G x) z (0 y) -> fold (\x. F x) (\x. G x) (F z) y
      fold (\x. F x) (\x. G x) z (1 y) -> fold (\x. F x) (\x. G x) (G z) y
      critical peaks: 0
       
       
       Higher-Order Closedness Processor:
         all critical pairs are trivial
        
        Qed