0.016/0.016 YES 0.016/0.016 0.016/0.016 Problem 1: 0.016/0.016 0.016/0.016 0.016/0.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.016/0.016 Confluence Problem: 0.016/0.016 (VAR vNonEmpty x xd xm xy y) 0.016/0.016 (REPLACEMENT-MAP 0.016/0.016 (add 1, 2) 0.016/0.016 (leq 1, 2) 0.016/0.016 (mul 1, 2) 0.016/0.016 (n 1, 2, 3) 0.016/0.016 (0) 0.016/0.016 (F) 0.016/0.016 (T) 0.016/0.016 (fSNonEmpty) 0.016/0.016 (s 1) 0.016/0.016 ) 0.016/0.016 (RULES 0.016/0.016 add(0,y) -> y 0.016/0.016 add(s(x),y) -> s(add(x,y)) 0.016/0.016 leq(0,0) -> T 0.016/0.016 leq(0,s(y)) -> T 0.016/0.016 leq(s(x),0) -> F 0.016/0.016 leq(s(x),s(y)) -> leq(x,y) 0.016/0.016 mul(0,y) -> 0 0.016/0.016 mul(s(x),s(y)) -> s(add(mul(x,s(y)),y)) 0.016/0.016 mul(x,0) -> 0 0.016/0.016 n(xd,xm,xy) -> add(xd,add(mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))),xm),mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),xy))) | leq(0,xd) ->* T, leq(xd,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))) ->* T, leq(0,xm) ->* T, leq(xm,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ->* T 0.016/0.016 ) 0.016/0.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.016/0.016 0.016/0.016 0.016/0.016 Problem 1: 0.016/0.016 0.016/0.016 Inlining of Conditions Processor [STERN17]: 0.016/0.016 0.016/0.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.016/0.016 Confluence Problem: 0.016/0.016 (VAR vNonEmpty x xd xm xy y) 0.016/0.016 (REPLACEMENT-MAP 0.016/0.016 (add 1, 2) 0.016/0.016 (leq 1, 2) 0.016/0.016 (mul 1, 2) 0.016/0.016 (n 1, 2, 3) 0.016/0.016 (0) 0.016/0.016 (F) 0.016/0.016 (T) 0.016/0.016 (fSNonEmpty) 0.016/0.016 (s 1) 0.016/0.016 ) 0.016/0.016 (RULES 0.016/0.016 add(0,y) -> y 0.016/0.016 add(s(x),y) -> s(add(x,y)) 0.016/0.016 leq(0,0) -> T 0.016/0.016 leq(0,s(y)) -> T 0.016/0.016 leq(s(x),0) -> F 0.016/0.016 leq(s(x),s(y)) -> leq(x,y) 0.016/0.016 mul(0,y) -> 0 0.016/0.016 mul(s(x),s(y)) -> s(add(mul(x,s(y)),y)) 0.016/0.016 mul(x,0) -> 0 0.016/0.016 n(xd,xm,xy) -> add(xd,add(mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))),xm),mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),xy))) | leq(0,xd) ->* T, leq(0,xm) ->* T, leq(xd,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))) ->* T, leq(xm,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ->* T 0.016/0.016 ) 0.016/0.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.016/0.016 0.016/0.016 0.016/0.016 Problem 1: 0.016/0.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.016/0.016 Confluence Problem: 0.016/0.016 (VAR vNonEmpty x xd xm xy y) 0.016/0.016 (REPLACEMENT-MAP 0.016/0.016 (add 1, 2) 0.016/0.016 (leq 1, 2) 0.016/0.016 (mul 1, 2) 0.016/0.016 (n 1, 2, 3) 0.016/0.016 (0) 0.016/0.016 (F) 0.016/0.016 (T) 0.016/0.016 (fSNonEmpty) 0.016/0.016 (s 1) 0.016/0.016 ) 0.016/0.016 (RULES 0.016/0.016 add(0,y) -> y 0.016/0.016 add(s(x),y) -> s(add(x,y)) 0.016/0.016 leq(0,0) -> T 0.016/0.016 leq(0,s(y)) -> T 0.016/0.016 leq(s(x),0) -> F 0.016/0.016 leq(s(x),s(y)) -> leq(x,y) 0.016/0.016 mul(0,y) -> 0 0.016/0.016 mul(s(x),s(y)) -> s(add(mul(x,s(y)),y)) 0.016/0.016 mul(x,0) -> 0 0.016/0.016 n(xd,xm,xy) -> add(xd,add(mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))),xm),mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),xy))) | leq(0,xd) ->* T, leq(0,xm) ->* T, leq(xd,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))) ->* T, leq(xm,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ->* T 0.016/0.016 ) 0.016/0.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.016/0.016 0.016/0.016 Critical Pairs Processor: 0.016/0.016 -> Rules: 0.016/0.016 add(0,y) -> y 0.016/0.016 add(s(x),y) -> s(add(x,y)) 0.016/0.016 leq(0,0) -> T 0.016/0.016 leq(0,s(y)) -> T 0.016/0.016 leq(s(x),0) -> F 0.016/0.016 leq(s(x),s(y)) -> leq(x,y) 0.016/0.016 mul(0,y) -> 0 0.016/0.016 mul(s(x),s(y)) -> s(add(mul(x,s(y)),y)) 0.016/0.016 mul(x,0) -> 0 0.016/0.016 n(xd,xm,xy) -> add(xd,add(mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))),xm),mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),xy))) | leq(0,xd) ->* T, leq(0,xm) ->* T, leq(xd,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))) ->* T, leq(xm,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ->* T 0.016/0.016 -> Vars: 0.016/0.016 "x", "xd", "xm", "xy", "y" 0.016/0.016 0.016/0.016 -> Rlps: 0.016/0.016 crule: add(0,y) -> y, id: 1, possubterms: add(0,y)-> [], 0-> [1] 0.016/0.016 crule: add(s(x),y) -> s(add(x,y)), id: 2, possubterms: add(s(x),y)-> [], s(x)-> [1] 0.016/0.016 crule: leq(0,0) -> T, id: 3, possubterms: leq(0,0)-> [], 0-> [1], 0-> [2] 0.016/0.016 crule: leq(0,s(y)) -> T, id: 4, possubterms: leq(0,s(y))-> [], 0-> [1], s(y)-> [2] 0.016/0.016 crule: leq(s(x),0) -> F, id: 5, possubterms: leq(s(x),0)-> [], s(x)-> [1], 0-> [2] 0.016/0.016 crule: leq(s(x),s(y)) -> leq(x,y), id: 6, possubterms: leq(s(x),s(y))-> [], s(x)-> [1], s(y)-> [2] 0.016/0.016 crule: mul(0,y) -> 0, id: 7, possubterms: mul(0,y)-> [], 0-> [1] 0.016/0.016 crule: mul(s(x),s(y)) -> s(add(mul(x,s(y)),y)), id: 8, possubterms: mul(s(x),s(y))-> [], s(x)-> [1], s(y)-> [2] 0.016/0.016 crule: mul(x,0) -> 0, id: 9, possubterms: mul(x,0)-> [], 0-> [2] 0.016/0.016 crule: n(xd,xm,xy) -> add(xd,add(mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))),xm),mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),xy))) | leq(0,xd) ->* T, leq(0,xm) ->* T, leq(xd,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))) ->* T, leq(xm,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ->* T, id: 10, possubterms: n(xd,xm,xy)-> [] 0.016/0.016 0.016/0.016 -> Unifications: 0.016/0.016 R9 unifies with R7 at p: [], l: mul(x,0), lp: mul(x,0), conds: {}, sig: {x -> 0,y -> 0}, l': mul(0,y), r: 0, r': 0 0.016/0.016 0.016/0.016 -> Critical pairs info: 0.016/0.016 <0,0> => Trivial, Overlay, NW2, N1 0.016/0.016 0.016/0.016 -> Problem conclusions: 0.016/0.016 Left linear, Not right linear, Not linear 0.016/0.016 Weakly orthogonal, Almost orthogonal, Not orthogonal 0.016/0.016 CTRS Type: 1 0.016/0.016 Deterministic, Strongly deterministic 0.016/0.016 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 0.016/0.016 Maybe right-stable CTRS, Overlay CTRS 0.016/0.016 Maybe normal CTRS, Maybe almost normal CTRS 0.016/0.016 Maybe terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 0.016/0.016 Maybe level confluent 0.016/0.016 Maybe confluent 0.016/0.016 0.016/0.016 Problem 1: 0.016/0.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.016/0.016 Confluence Problem: 0.016/0.016 (VAR x xd xm xy y) 0.016/0.016 (REPLACEMENT-MAP 0.016/0.016 (add 1, 2) 0.016/0.016 (leq 1, 2) 0.016/0.016 (mul 1, 2) 0.016/0.016 (n 1, 2, 3) 0.016/0.016 (0) 0.016/0.016 (F) 0.016/0.016 (T) 0.016/0.016 (fSNonEmpty) 0.016/0.016 (s 1) 0.016/0.016 ) 0.016/0.016 (RULES 0.016/0.016 add(0,y) -> y 0.016/0.016 add(s(x),y) -> s(add(x,y)) 0.016/0.016 leq(0,0) -> T 0.016/0.016 leq(0,s(y)) -> T 0.016/0.016 leq(s(x),0) -> F 0.016/0.016 leq(s(x),s(y)) -> leq(x,y) 0.016/0.016 mul(0,y) -> 0 0.016/0.016 mul(s(x),s(y)) -> s(add(mul(x,s(y)),y)) 0.016/0.016 mul(x,0) -> 0 0.016/0.016 n(xd,xm,xy) -> add(xd,add(mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))),xm),mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),xy))) | leq(0,xd) ->* T, leq(0,xm) ->* T, leq(xd,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))) ->* T, leq(xm,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ->* T 0.016/0.016 ) 0.016/0.016 Critical Pairs: 0.016/0.016 0.016/0.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.016/0.016 0.016/0.016 Right Stable Processor: 0.016/0.016 Right-stable CTRS 0.016/0.016 Justification: 0.016/0.016 0.016/0.016 -> Term right-stability conditions: 0.016/0.016 Term: T 0.016/0.016 Right-stable term 0.016/0.016 Linear constructor form 0.016/0.016 Don't know if term is a ground normal form (not needed) 0.016/0.016 Right-stability condition achieved 0.016/0.016 A call to InfChecker wasn't needed 0.016/0.016 0.016/0.016 0.016/0.016 -> Term right-stability conditions: 0.016/0.016 Term: T 0.016/0.016 Right-stable term 0.016/0.016 Linear constructor form 0.016/0.016 Don't know if term is a ground normal form (not needed) 0.016/0.016 Right-stability condition achieved 0.016/0.016 A call to InfChecker wasn't needed 0.016/0.016 0.016/0.016 0.016/0.016 -> Term right-stability conditions: 0.016/0.016 Term: T 0.016/0.016 Right-stable term 0.016/0.016 Linear constructor form 0.016/0.016 Don't know if term is a ground normal form (not needed) 0.016/0.016 Right-stability condition achieved 0.016/0.016 A call to InfChecker wasn't needed 0.016/0.016 0.016/0.016 0.016/0.016 -> Term right-stability conditions: 0.016/0.016 Term: T 0.016/0.016 Right-stable term 0.016/0.016 Linear constructor form 0.016/0.016 Don't know if term is a ground normal form (not needed) 0.016/0.016 Right-stability condition achieved 0.016/0.016 A call to InfChecker wasn't needed 0.016/0.016 0.016/0.016 -> Problem conclusions: 0.016/0.016 Left linear, Not right linear, Not linear 0.016/0.016 Weakly orthogonal, Almost orthogonal, Orthogonal 0.016/0.016 CTRS Type: 1 0.016/0.016 Deterministic, Strongly deterministic 0.016/0.016 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 0.016/0.016 Right-stable CTRS, Overlay CTRS 0.016/0.016 Maybe normal CTRS, Almost normal CTRS 0.016/0.016 Maybe terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 0.016/0.016 Level confluent 0.016/0.016 Confluent 0.016/0.016 0.016/0.016 The problem is joinable. 0.016/0.016 0.15user 0.00system 0:00.16elapsed 98%CPU (0avgtext+0avgdata 14104maxresident)k 0.016/0.016 8inputs+0outputs (0major+1804minor)pagefaults 0swaps