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
 0 (1 y) -> 1 (0 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 (1 y) -> 1 (0 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
     0 (1 y) -> 1 (0 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
      0 (1 y) -> 1 (0 y)
      critical peaks: 1
       fold (\x. F x) (\x. G x) z (1 (0 214)) <-[1]-> fold (\x. F x) (\x. G x) (F z) (1 214)
       
       Higher-Order Nonconfluence Processor:
        non-joinable conversion:
        fold (\x. F x) (\x. G x) (F (G z)) 214 *<- fold (\x. F x) (\x. G x) z (1 (0 214)) <- . -> 
        fold (\x. F x) (\x. G x) (F z) (1 214) ->* fold (\x. F x) (\x. G x) (G (F z)) 214
        Qed