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