3.42/1.88	YES
3.42/1.88	
3.42/1.88	Problem:
3.42/1.88	 nats() -> :(0(),inc(nats()))
3.42/1.88	 inc(:(x,y)) -> :(s(x),inc(y))
3.42/1.88	 inc(tl(nats())) -> tl(inc(nats()))
3.42/1.88	 hd(:(x,y)) -> x
3.42/1.88	 tl(:(x,y)) -> y
3.42/1.88	 d(:(x,y)) -> :(x,:(x,d(y)))
3.42/1.88	
3.42/1.88	Proof:
3.42/1.88	 Church Rosser Transformation Processor:
3.42/1.88	  strict:
3.42/1.88	   
3.42/1.88	  weak:
3.42/1.88	   
3.42/1.88	  critical peaks: 1
3.42/1.88	   inc(tl(:(0(),inc(nats())))) <-0|0,0[]- inc(tl(nats())) -2|[]-> tl(inc(nats()))
3.42/1.88	  Redundant Rules Transformation:
3.42/1.88	   nats() -> :(0(),inc(nats()))
3.42/1.88	   inc(:(x,y)) -> :(s(x),inc(y))
3.42/1.88	   hd(:(x,y)) -> x
3.42/1.88	   tl(:(x,y)) -> y
3.42/1.88	   d(:(x,y)) -> :(x,:(x,d(y)))
3.42/1.88	   Church Rosser Transformation Processor (no redundant rules):
3.42/1.88	    strict:
3.42/1.88	     d(:(x,y)) -> :(x,:(x,d(y)))
3.42/1.88	     tl(:(x,y)) -> y
3.42/1.88	     hd(:(x,y)) -> x
3.42/1.88	     inc(:(x,y)) -> :(s(x),inc(y))
3.42/1.88	     nats() -> :(0(),inc(nats()))
3.42/1.88	    weak:
3.42/1.88	     
3.42/1.88	    critical peaks: 0
3.42/1.88	    Closedness Processor (*feeble*):
3.42/1.88	     
3.42/1.88	     Qed
3.42/1.88	EOF