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:S x:S xd:S xm:S xy:S y:S) 0.016/0.016 (STRATEGY CONTEXTSENSITIVE 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:S) -> y:S 0.016/0.016 add(s(x:S),y:S) -> s(add(x:S,y:S)) 0.016/0.016 leq(0,0) -> T 0.016/0.016 leq(0,s(y:S)) -> T 0.016/0.016 leq(s(x:S),0) -> F 0.016/0.016 leq(s(x:S),s(y:S)) -> leq(x:S,y:S) 0.016/0.016 mul(0,y:S) -> 0 0.016/0.016 mul(s(x:S),s(y:S)) -> s(add(mul(x:S,s(y:S)),y:S)) 0.016/0.016 mul(x:S,0) -> 0 0.016/0.016 n(xd:S,xm:S,xy:S) -> add(xd:S,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:S),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:S))) | leq(0,xd:S) ->* 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(s(0)))))))))))))))))))))))))))))) ->* T, leq(0,xm:S) ->* 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(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:S x:S xd:S xm:S xy:S y:S) 0.016/0.016 (STRATEGY CONTEXTSENSITIVE 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:S) -> y:S 0.016/0.016 add(s(x:S),y:S) -> s(add(x:S,y:S)) 0.016/0.016 leq(0,0) -> T 0.016/0.016 leq(0,s(y:S)) -> T 0.016/0.016 leq(s(x:S),0) -> F 0.016/0.016 leq(s(x:S),s(y:S)) -> leq(x:S,y:S) 0.016/0.016 mul(0,y:S) -> 0 0.016/0.016 mul(s(x:S),s(y:S)) -> s(add(mul(x:S,s(y:S)),y:S)) 0.016/0.016 mul(x:S,0) -> 0 0.016/0.016 n(xd:S,xm:S,xy:S) -> add(xd:S,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:S),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:S))) | leq(0,xd:S) ->* T, leq(0,xm:S) ->* 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(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(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:S x:S xd:S xm:S xy:S y:S) 0.016/0.016 (STRATEGY CONTEXTSENSITIVE 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:S) -> y:S 0.016/0.016 add(s(x:S),y:S) -> s(add(x:S,y:S)) 0.016/0.016 leq(0,0) -> T 0.016/0.016 leq(0,s(y:S)) -> T 0.016/0.016 leq(s(x:S),0) -> F 0.016/0.016 leq(s(x:S),s(y:S)) -> leq(x:S,y:S) 0.016/0.016 mul(0,y:S) -> 0 0.016/0.016 mul(s(x:S),s(y:S)) -> s(add(mul(x:S,s(y:S)),y:S)) 0.016/0.016 mul(x:S,0) -> 0 0.016/0.016 n(xd:S,xm:S,xy:S) -> add(xd:S,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:S),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:S))) | leq(0,xd:S) ->* T, leq(0,xm:S) ->* 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(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(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:S) -> y:S 0.016/0.016 add(s(x:S),y:S) -> s(add(x:S,y:S)) 0.016/0.016 leq(0,0) -> T 0.016/0.016 leq(0,s(y:S)) -> T 0.016/0.016 leq(s(x:S),0) -> F 0.016/0.016 leq(s(x:S),s(y:S)) -> leq(x:S,y:S) 0.016/0.016 mul(0,y:S) -> 0 0.016/0.016 mul(s(x:S),s(y:S)) -> s(add(mul(x:S,s(y:S)),y:S)) 0.016/0.016 mul(x:S,0) -> 0 0.016/0.016 n(xd:S,xm:S,xy:S) -> add(xd:S,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:S),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:S))) | leq(0,xd:S) ->* T, leq(0,xm:S) ->* 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(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(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ->* T 0.016/0.016 -> Vars: 0.016/0.016 "y", "x", "y", "y", "x", "x", "y", "y", "x", "y", "x", "xd", "xm", "xy" 0.016/0.016 -> FVars: 0.016/0.016 "x6", "x7", "x8", "x9", "x10", "x11", "x12", "x13", "x14", "x15", "x16", "x17", "x18", "x19" 0.016/0.016 -> PVars: 0.016/0.016 "y": ["x6", "x8", "x9", "x12", "x13", "x15"], "x": ["x7", "x10", "x11", "x14", "x16"], "xd": ["x17"], "xm": ["x18"], "xy": ["x19"] 0.016/0.016 0.016/0.016 -> Rlps: 0.016/0.016 crule: add(0,x6:S) -> x6:S, id: 1, possubterms: add(0,x6:S)-> [], 0-> [1] 0.016/0.016 crule: add(s(x7:S),x8:S) -> s(add(x7:S,x8:S)), id: 2, possubterms: add(s(x7:S),x8:S)-> [], s(x7:S)-> [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(x9:S)) -> T, id: 4, possubterms: leq(0,s(x9:S))-> [], 0-> [1], s(x9:S)-> [2] 0.016/0.016 crule: leq(s(x10:S),0) -> F, id: 5, possubterms: leq(s(x10:S),0)-> [], s(x10:S)-> [1], 0-> [2] 0.016/0.016 crule: leq(s(x11:S),s(x12:S)) -> leq(x11:S,x12:S), id: 6, possubterms: leq(s(x11:S),s(x12:S))-> [], s(x11:S)-> [1], s(x12:S)-> [2] 0.016/0.016 crule: mul(0,x13:S) -> 0, id: 7, possubterms: mul(0,x13:S)-> [], 0-> [1] 0.016/0.016 crule: mul(s(x14:S),s(x15:S)) -> s(add(mul(x14:S,s(x15:S)),x15:S)), id: 8, possubterms: mul(s(x14:S),s(x15:S))-> [], s(x14:S)-> [1], s(x15:S)-> [2] 0.016/0.016 crule: mul(x16:S,0) -> 0, id: 9, possubterms: mul(x16:S,0)-> [], 0-> [2] 0.016/0.016 crule: n(x17:S,x18:S,x19:S) -> add(x17:S,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)))))))))))))))))))))))))))))),x18:S),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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x19:S))) | leq(0,x17:S) ->* T, leq(0,x18:S) ->* T, leq(x17:S,s(s(s(s(s(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(x18:S,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(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(x17:S,x18:S,x19:S)-> [] 0.016/0.016 0.016/0.016 -> Unifications: 0.016/0.016 R9 unifies with R7 at p: [], l: mul(x16:S,0), lp: mul(x16:S,0), conds: {}, sig: {y:S -> 0,x16:S -> 0}, l': mul(0,y:S), r: 0, r': 0 0.016/0.016 0.016/0.016 -> Critical pairs info: 0.016/0.016 <0,0> => Trivial, Overlay, 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 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, 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 vNonEmpty:S x:S xd:S xm:S xy:S y:S) 0.016/0.016 (STRATEGY CONTEXTSENSITIVE 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:S) -> y:S 0.016/0.016 add(s(x:S),y:S) -> s(add(x:S,y:S)) 0.016/0.016 leq(0,0) -> T 0.016/0.016 leq(0,s(y:S)) -> T 0.016/0.016 leq(s(x:S),0) -> F 0.016/0.016 leq(s(x:S),s(y:S)) -> leq(x:S,y:S) 0.016/0.016 mul(0,y:S) -> 0 0.016/0.016 mul(s(x:S),s(y:S)) -> s(add(mul(x:S,s(y:S)),y:S)) 0.016/0.016 mul(x:S,0) -> 0 0.016/0.016 n(xd:S,xm:S,xy:S) -> add(xd:S,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:S),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:S))) | leq(0,xd:S) ->* T, leq(0,xm:S) ->* 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(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(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 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, 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.14user 0.01system 0:00.16elapsed 96%CPU (0avgtext+0avgdata 13136maxresident)k 0.016/0.016 8inputs+0outputs (0major+1692minor)pagefaults 0swaps