Problem:
 decide x -> cmp (0s x) (1s x)
 0s nil -> nil
 0s (0 x) -> 0 (0s x)
 0s (1 x) -> 0s x
 1s nil -> nil
 1s (1 x) -> 1 (1s x)
 1s (0 x) -> 1s x
 cmp (0 x) (1 y) -> cmp x y
 cmp (0 x) nil -> false
 cmp nil y -> true

Proof:
 Higher-Order Church Rosser Processor:
  decide x -> cmp (0s x) (1s x)
  0s nil -> nil
  0s (0 x) -> 0 (0s x)
  0s (1 x) -> 0s x
  1s nil -> nil
  1s (1 x) -> 1 (1s x)
  1s (0 x) -> 1s x
  cmp (0 x) (1 y) -> cmp x y
  cmp (0 x) nil -> false
  cmp nil y -> true
  critical peaks: 0
   
   
   Higher-Order Closedness Processor:
     all critical pairs are trivial
    
    Qed