Problem: rec (\x y. F x y) a 0 -> a rec (\x y. F x y) a (s n) -> F n (rec (\x y. F x y) a n) add a n -> rec (\x y. s y) a n add a 0 -> a add a (s n) -> s (add a n) Proof: Higher-Order Church Rosser Processor: rec (\x y. F x y) a 0 -> a rec (\x y. F x y) a (s n) -> F n (rec (\x y. F x y) a n) add a n -> rec (\x y. s y) a n add a 0 -> a add a (s n) -> s (add a n) critical peaks: 4 rec (\x y. s y) 64 0 <-[]-> 64 rec (\x y. s y) 73 (s 74) <-[]-> s (add 73 74) 82 <-[]-> rec (\x y. s y) 82 0 s (add 99 100) <-[]-> rec (\x y. s y) 99 (s 100) Higher-Order Closedness Processor: all critical pairs are (almost) development closed Qed