0.00/0.34 NO 0.00/0.35 0.00/0.35 Problem: 0.00/0.35 f x x -> a 0.00/0.35 f x (s x) -> b 0.00/0.35 mu (\x. Z x) -> Z (mu (\x. Z x)) 0.00/0.35 0.00/0.35 Proof: 0.00/0.35 Higher-Order Church Rosser Processor: 0.00/0.35 f x x -> a 0.00/0.35 f x (s x) -> b 0.00/0.35 mu (\x. Z x) -> Z (mu (\x. Z x)) 0.00/0.35 critical peaks: 0 0.00/0.35 0.00/0.35 0.00/0.35 Redundant Rules Transformation for Pattern Rewrite Systems: 0.00/0.35 f x x -> a 0.00/0.35 f x (s x) -> b 0.00/0.35 mu (\x. Z x) -> Z (mu (\x. Z x)) 0.00/0.35 mu (\x. 70 x) -> 70 (70 (mu (\x. 70 x))) 0.00/0.35 f (mu (\x. s x)) (mu (\x. s x)) -> b 0.00/0.35 Higher-Order Church Rosser Processor: 0.00/0.35 f x x -> a 0.00/0.35 f x (s x) -> b 0.00/0.35 mu (\x. Z x) -> Z (mu (\x. Z x)) 0.00/0.35 mu (\x. 70 x) -> 70 (70 (mu (\x. 70 x))) 0.00/0.35 f (mu (\x. s x)) (mu (\x. s x)) -> b 0.00/0.35 critical peaks: 8 0.00/0.35 a <-[]-> b 0.00/0.35 105 (mu (\x. 105 x)) <-[]-> 105 (105 (mu (\x. 105 x))) 0.00/0.35 f (s (mu (\x. s x))) (mu (\x. s x)) <-[0,1]-> b 0.00/0.35 f (mu (\x. s x)) (s (mu (\x. s x))) <-[1]-> b 0.00/0.35 115 (115 (mu (\x. 115 x))) <-[]-> 115 (mu (\x. 115 x)) 0.00/0.35 f (s (s (mu (\x. s x)))) (mu (\x. s x)) <-[0,1]-> b 0.00/0.35 f (mu (\x. s x)) (s (s (mu (\x. s x)))) <-[1]-> b 0.00/0.35 b <-[]-> a 0.00/0.35 0.00/0.35 Higher-Order Nonconfluence Processor: 0.00/0.35 non-joinable conversion: 0.00/0.35 a *<- a <- f (mu (\x. s x)) (mu (\x. s x)) -> b ->* b 0.00/0.35 Qed 0.00/0.35 0.00/0.35 EOF