0.004/0.004 NO 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Confluence Problem: 0.004/0.004 (VAR vNonEmpty:S X:S Y:S Z:S) 0.004/0.004 (STRATEGY CONTEXTSENSITIVE 0.004/0.004 (fcons 1 2) 0.004/0.004 (first 1 2) 0.004/0.004 (first1 1 2) 0.004/0.004 (from 1) 0.004/0.004 (quote) 0.004/0.004 (quote1) 0.004/0.004 (sel 1 2) 0.004/0.004 (sel1 1 2) 0.004/0.004 (unquote 1) 0.004/0.004 (unquote1 1) 0.004/0.004 (0) 0.004/0.004 (01) 0.004/0.004 (cons 1) 0.004/0.004 (cons1 1 2) 0.004/0.004 (fSNonEmpty) 0.004/0.004 (nil) 0.004/0.004 (nil1) 0.004/0.004 (s 1) 0.004/0.004 (s1 1) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 fcons(X:S,Z:S) -> cons(X:S,Z:S) 0.004/0.004 first(0,Z:S) -> nil 0.004/0.004 first(s(X:S),cons(Y:S,Z:S)) -> cons(Y:S,first(X:S,Z:S)) 0.004/0.004 first1(0,Z:S) -> nil1 0.004/0.004 first1(s(X:S),cons(Y:S,Z:S)) -> cons1(quote(Y:S),first1(X:S,Z:S)) 0.004/0.004 from(X:S) -> cons(X:S,from(s(X:S))) 0.004/0.004 quote(sel(X:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 quote(0) -> 01 0.004/0.004 quote(s(X:S)) -> s1(quote(X:S)) 0.004/0.004 quote1(first(X:S,Z:S)) -> first1(X:S,Z:S) 0.004/0.004 quote1(cons(X:S,Z:S)) -> cons1(quote(X:S),quote1(Z:S)) 0.004/0.004 quote1(nil) -> nil1 0.004/0.004 sel(0,cons(X:S,Z:S)) -> X:S 0.004/0.004 sel(s(X:S),cons(Y:S,Z:S)) -> sel(X:S,Z:S) 0.004/0.004 sel1(0,cons(X:S,Z:S)) -> quote(X:S) 0.004/0.004 sel1(s(X:S),cons(Y:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 unquote(01) -> 0 0.004/0.004 unquote(s1(X:S)) -> s(unquote(X:S)) 0.004/0.004 unquote1(cons1(X:S,Z:S)) -> fcons(unquote(X:S),unquote1(Z:S)) 0.004/0.004 unquote1(nil1) -> nil 0.004/0.004 ) 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 CleanTRS Processor: 0.004/0.004 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Confluence Problem: 0.004/0.004 (VAR vNonEmpty:S X:S Y:S Z:S) 0.004/0.004 (STRATEGY CONTEXTSENSITIVE 0.004/0.004 (fcons 1 2) 0.004/0.004 (first 1 2) 0.004/0.004 (first1 1 2) 0.004/0.004 (from 1) 0.004/0.004 (quote) 0.004/0.004 (quote1) 0.004/0.004 (sel 1 2) 0.004/0.004 (sel1 1 2) 0.004/0.004 (unquote 1) 0.004/0.004 (unquote1 1) 0.004/0.004 (0) 0.004/0.004 (01) 0.004/0.004 (cons 1) 0.004/0.004 (cons1 1 2) 0.004/0.004 (fSNonEmpty) 0.004/0.004 (nil) 0.004/0.004 (nil1) 0.004/0.004 (s 1) 0.004/0.004 (s1 1) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 fcons(X:S,Z:S) -> cons(X:S,Z:S) 0.004/0.004 first(0,Z:S) -> nil 0.004/0.004 first(s(X:S),cons(Y:S,Z:S)) -> cons(Y:S,first(X:S,Z:S)) 0.004/0.004 first1(0,Z:S) -> nil1 0.004/0.004 first1(s(X:S),cons(Y:S,Z:S)) -> cons1(quote(Y:S),first1(X:S,Z:S)) 0.004/0.004 from(X:S) -> cons(X:S,from(s(X:S))) 0.004/0.004 quote(sel(X:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 quote(0) -> 01 0.004/0.004 quote(s(X:S)) -> s1(quote(X:S)) 0.004/0.004 quote1(first(X:S,Z:S)) -> first1(X:S,Z:S) 0.004/0.004 quote1(cons(X:S,Z:S)) -> cons1(quote(X:S),quote1(Z:S)) 0.004/0.004 quote1(nil) -> nil1 0.004/0.004 sel(0,cons(X:S,Z:S)) -> X:S 0.004/0.004 sel(s(X:S),cons(Y:S,Z:S)) -> sel(X:S,Z:S) 0.004/0.004 sel1(0,cons(X:S,Z:S)) -> quote(X:S) 0.004/0.004 sel1(s(X:S),cons(Y:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 unquote(01) -> 0 0.004/0.004 unquote(s1(X:S)) -> s(unquote(X:S)) 0.004/0.004 unquote1(cons1(X:S,Z:S)) -> fcons(unquote(X:S),unquote1(Z:S)) 0.004/0.004 unquote1(nil1) -> nil 0.004/0.004 ) 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 Modular Confluence Combinations Decomposition Processor: 0.004/0.004 It is a CTRS -> No modular confluence 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 CS-TRS Processor: 0.004/0.004 R is a CS-TRS 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Confluence Problem: 0.004/0.004 (VAR vNonEmpty:S X:S Y:S Z:S) 0.004/0.004 (STRATEGY CONTEXTSENSITIVE 0.004/0.004 (fcons 1 2) 0.004/0.004 (first 1 2) 0.004/0.004 (first1 1 2) 0.004/0.004 (from 1) 0.004/0.004 (quote) 0.004/0.004 (quote1) 0.004/0.004 (sel 1 2) 0.004/0.004 (sel1 1 2) 0.004/0.004 (unquote 1) 0.004/0.004 (unquote1 1) 0.004/0.004 (0) 0.004/0.004 (01) 0.004/0.004 (cons 1) 0.004/0.004 (cons1 1 2) 0.004/0.004 (fSNonEmpty) 0.004/0.004 (nil) 0.004/0.004 (nil1) 0.004/0.004 (s 1) 0.004/0.004 (s1 1) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 fcons(X:S,Z:S) -> cons(X:S,Z:S) 0.004/0.004 first(0,Z:S) -> nil 0.004/0.004 first(s(X:S),cons(Y:S,Z:S)) -> cons(Y:S,first(X:S,Z:S)) 0.004/0.004 first1(0,Z:S) -> nil1 0.004/0.004 first1(s(X:S),cons(Y:S,Z:S)) -> cons1(quote(Y:S),first1(X:S,Z:S)) 0.004/0.004 from(X:S) -> cons(X:S,from(s(X:S))) 0.004/0.004 quote(sel(X:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 quote(0) -> 01 0.004/0.004 quote(s(X:S)) -> s1(quote(X:S)) 0.004/0.004 quote1(first(X:S,Z:S)) -> first1(X:S,Z:S) 0.004/0.004 quote1(cons(X:S,Z:S)) -> cons1(quote(X:S),quote1(Z:S)) 0.004/0.004 quote1(nil) -> nil1 0.004/0.004 sel(0,cons(X:S,Z:S)) -> X:S 0.004/0.004 sel(s(X:S),cons(Y:S,Z:S)) -> sel(X:S,Z:S) 0.004/0.004 sel1(0,cons(X:S,Z:S)) -> quote(X:S) 0.004/0.004 sel1(s(X:S),cons(Y:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 unquote(01) -> 0 0.004/0.004 unquote(s1(X:S)) -> s(unquote(X:S)) 0.004/0.004 unquote1(cons1(X:S,Z:S)) -> fcons(unquote(X:S),unquote1(Z:S)) 0.004/0.004 unquote1(nil1) -> nil 0.004/0.004 ) 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 0.004/0.004 Extended u-Critical Pairs NonLHRV Processor [JLAMP21]: 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 1 (l' :-> r') => fcons(X:S,Z:S) -> cons(X:S,Z:S) 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> fcons(X:S,Z:S)} 0.004/0.004 s => cons(x4:S,fcons(X:S,Z:S)) 0.004/0.004 t => fcons(x4:S,cons(X:S,Z:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 2 (l' :-> r') => first(0,Z:S) -> nil 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> first(0,Z:S)} 0.004/0.004 s => cons(x4:S,first(0,Z:S)) 0.004/0.004 t => fcons(x4:S,nil) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 3 (l' :-> r') => first(s(X:S),cons(Y:S,Z:S)) -> cons(Y:S,first(X:S,Z:S)) 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> first(s(X:S),cons(Y:S,Z:S))} 0.004/0.004 s => cons(x4:S,first(s(X:S),cons(Y:S,Z:S))) 0.004/0.004 t => fcons(x4:S,cons(Y:S,first(X:S,Z:S))) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 4 (l' :-> r') => first1(0,Z:S) -> nil1 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> first1(0,Z:S)} 0.004/0.004 s => cons(x4:S,first1(0,Z:S)) 0.004/0.004 t => fcons(x4:S,nil1) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 5 (l' :-> r') => first1(s(X:S),cons(Y:S,Z:S)) -> cons1(quote(Y:S),first1(X:S,Z:S)) 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> first1(s(X:S),cons(Y:S,Z:S))} 0.004/0.004 s => cons(x4:S,first1(s(X:S),cons(Y:S,Z:S))) 0.004/0.004 t => fcons(x4:S,cons1(quote(Y:S),first1(X:S,Z:S))) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 6 (l' :-> r') => from(X:S) -> cons(X:S,from(s(X:S))) 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> from(X:S)} 0.004/0.004 s => cons(x4:S,from(X:S)) 0.004/0.004 t => fcons(x4:S,cons(X:S,from(s(X:S)))) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 7 (l' :-> r') => quote(sel(X:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> quote(sel(X:S,Z:S))} 0.004/0.004 s => cons(x4:S,quote(sel(X:S,Z:S))) 0.004/0.004 t => fcons(x4:S,sel1(X:S,Z:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 8 (l' :-> r') => quote(0) -> 01 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> quote(0)} 0.004/0.004 s => cons(x4:S,quote(0)) 0.004/0.004 t => fcons(x4:S,01) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 9 (l' :-> r') => quote(s(X:S)) -> s1(quote(X:S)) 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> quote(s(X:S))} 0.004/0.004 s => cons(x4:S,quote(s(X:S))) 0.004/0.004 t => fcons(x4:S,s1(quote(X:S))) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 10 (l' :-> r') => quote1(first(X:S,Z:S)) -> first1(X:S,Z:S) 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> quote1(first(X:S,Z:S))} 0.004/0.004 s => cons(x4:S,quote1(first(X:S,Z:S))) 0.004/0.004 t => fcons(x4:S,first1(X:S,Z:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 11 (l' :-> r') => quote1(cons(X:S,Z:S)) -> cons1(quote(X:S),quote1(Z:S)) 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> quote1(cons(X:S,Z:S))} 0.004/0.004 s => cons(x4:S,quote1(cons(X:S,Z:S))) 0.004/0.004 t => fcons(x4:S,cons1(quote(X:S),quote1(Z:S))) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 12 (l' :-> r') => quote1(nil) -> nil1 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> quote1(nil)} 0.004/0.004 s => cons(x4:S,quote1(nil)) 0.004/0.004 t => fcons(x4:S,nil1) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 13 (l' :-> r') => sel(0,cons(X:S,Z:S)) -> X:S 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> sel(0,cons(X:S,Z:S))} 0.004/0.004 s => cons(x4:S,sel(0,cons(X:S,Z:S))) 0.004/0.004 t => fcons(x4:S,X:S) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 14 (l' :-> r') => sel(s(X:S),cons(Y:S,Z:S)) -> sel(X:S,Z:S) 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> sel(s(X:S),cons(Y:S,Z:S))} 0.004/0.004 s => cons(x4:S,sel(s(X:S),cons(Y:S,Z:S))) 0.004/0.004 t => fcons(x4:S,sel(X:S,Z:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 15 (l' :-> r') => sel1(0,cons(X:S,Z:S)) -> quote(X:S) 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> sel1(0,cons(X:S,Z:S))} 0.004/0.004 s => cons(x4:S,sel1(0,cons(X:S,Z:S))) 0.004/0.004 t => fcons(x4:S,quote(X:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 16 (l' :-> r') => sel1(s(X:S),cons(Y:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> sel1(s(X:S),cons(Y:S,Z:S))} 0.004/0.004 s => cons(x4:S,sel1(s(X:S),cons(Y:S,Z:S))) 0.004/0.004 t => fcons(x4:S,sel1(X:S,Z:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 17 (l' :-> r') => unquote(01) -> 0 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> unquote(01)} 0.004/0.004 s => cons(x4:S,unquote(01)) 0.004/0.004 t => fcons(x4:S,0) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 18 (l' :-> r') => unquote(s1(X:S)) -> s(unquote(X:S)) 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> unquote(s1(X:S))} 0.004/0.004 s => cons(x4:S,unquote(s1(X:S))) 0.004/0.004 t => fcons(x4:S,s(unquote(X:S))) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 19 (l' :-> r') => unquote1(cons1(X:S,Z:S)) -> fcons(unquote(X:S),unquote1(Z:S)) 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> unquote1(cons1(X:S,Z:S))} 0.004/0.004 s => cons(x4:S,unquote1(cons1(X:S,Z:S))) 0.004/0.004 t => fcons(x4:S,fcons(unquote(X:S),unquote1(Z:S))) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => fcons(x4:S,x5:S) -> cons(x4:S,x5:S) 0.004/0.004 Rule 20 (l' :-> r') => unquote1(nil1) -> nil 0.004/0.004 Var => x5:S 0.004/0.004 Pos x5:S in l => [2] 0.004/0.004 Sigma => {x5:S -> unquote1(nil1)} 0.004/0.004 s => cons(x4:S,unquote1(nil1)) 0.004/0.004 t => fcons(x4:S,nil) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 3 (l' :-> r') => first(s(X:S),cons(Y:S,Z:S)) -> cons(Y:S,first(X:S,Z:S)) 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> first(s(X:S),cons(Y:S,Z:S))} 0.004/0.004 s => cons(x8:S,first(first(s(X:S),cons(Y:S,Z:S)),x9:S)) 0.004/0.004 t => first(s(cons(Y:S,first(X:S,Z:S))),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 4 (l' :-> r') => first1(0,Z:S) -> nil1 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> first1(0,Z:S)} 0.004/0.004 s => cons(x8:S,first(first1(0,Z:S),x9:S)) 0.004/0.004 t => first(s(nil1),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 5 (l' :-> r') => first1(s(X:S),cons(Y:S,Z:S)) -> cons1(quote(Y:S),first1(X:S,Z:S)) 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> first1(s(X:S),cons(Y:S,Z:S))} 0.004/0.004 s => cons(x8:S,first(first1(s(X:S),cons(Y:S,Z:S)),x9:S)) 0.004/0.004 t => first(s(cons1(quote(Y:S),first1(X:S,Z:S))),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 6 (l' :-> r') => from(X:S) -> cons(X:S,from(s(X:S))) 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> from(X:S)} 0.004/0.004 s => cons(x8:S,first(from(X:S),x9:S)) 0.004/0.004 t => first(s(cons(X:S,from(s(X:S)))),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 7 (l' :-> r') => quote(sel(X:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> quote(sel(X:S,Z:S))} 0.004/0.004 s => cons(x8:S,first(quote(sel(X:S,Z:S)),x9:S)) 0.004/0.004 t => first(s(sel1(X:S,Z:S)),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 8 (l' :-> r') => quote(0) -> 01 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> quote(0)} 0.004/0.004 s => cons(x8:S,first(quote(0),x9:S)) 0.004/0.004 t => first(s(01),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 9 (l' :-> r') => quote(s(X:S)) -> s1(quote(X:S)) 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> quote(s(X:S))} 0.004/0.004 s => cons(x8:S,first(quote(s(X:S)),x9:S)) 0.004/0.004 t => first(s(s1(quote(X:S))),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 10 (l' :-> r') => quote1(first(X:S,Z:S)) -> first1(X:S,Z:S) 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> quote1(first(X:S,Z:S))} 0.004/0.004 s => cons(x8:S,first(quote1(first(X:S,Z:S)),x9:S)) 0.004/0.004 t => first(s(first1(X:S,Z:S)),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 11 (l' :-> r') => quote1(cons(X:S,Z:S)) -> cons1(quote(X:S),quote1(Z:S)) 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> quote1(cons(X:S,Z:S))} 0.004/0.004 s => cons(x8:S,first(quote1(cons(X:S,Z:S)),x9:S)) 0.004/0.004 t => first(s(cons1(quote(X:S),quote1(Z:S))),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 12 (l' :-> r') => quote1(nil) -> nil1 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> quote1(nil)} 0.004/0.004 s => cons(x8:S,first(quote1(nil),x9:S)) 0.004/0.004 t => first(s(nil1),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 13 (l' :-> r') => sel(0,cons(X:S,Z:S)) -> X:S 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> sel(0,cons(X:S,Z:S))} 0.004/0.004 s => cons(x8:S,first(sel(0,cons(X:S,Z:S)),x9:S)) 0.004/0.004 t => first(s(X:S),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 14 (l' :-> r') => sel(s(X:S),cons(Y:S,Z:S)) -> sel(X:S,Z:S) 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> sel(s(X:S),cons(Y:S,Z:S))} 0.004/0.004 s => cons(x8:S,first(sel(s(X:S),cons(Y:S,Z:S)),x9:S)) 0.004/0.004 t => first(s(sel(X:S,Z:S)),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 15 (l' :-> r') => sel1(0,cons(X:S,Z:S)) -> quote(X:S) 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> sel1(0,cons(X:S,Z:S))} 0.004/0.004 s => cons(x8:S,first(sel1(0,cons(X:S,Z:S)),x9:S)) 0.004/0.004 t => first(s(quote(X:S)),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 16 (l' :-> r') => sel1(s(X:S),cons(Y:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> sel1(s(X:S),cons(Y:S,Z:S))} 0.004/0.004 s => cons(x8:S,first(sel1(s(X:S),cons(Y:S,Z:S)),x9:S)) 0.004/0.004 t => first(s(sel1(X:S,Z:S)),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 17 (l' :-> r') => unquote(01) -> 0 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> unquote(01)} 0.004/0.004 s => cons(x8:S,first(unquote(01),x9:S)) 0.004/0.004 t => first(s(0),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 18 (l' :-> r') => unquote(s1(X:S)) -> s(unquote(X:S)) 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> unquote(s1(X:S))} 0.004/0.004 s => cons(x8:S,first(unquote(s1(X:S)),x9:S)) 0.004/0.004 t => first(s(s(unquote(X:S))),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 19 (l' :-> r') => unquote1(cons1(X:S,Z:S)) -> fcons(unquote(X:S),unquote1(Z:S)) 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> unquote1(cons1(X:S,Z:S))} 0.004/0.004 s => cons(x8:S,first(unquote1(cons1(X:S,Z:S)),x9:S)) 0.004/0.004 t => first(s(fcons(unquote(X:S),unquote1(Z:S))),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)) 0.004/0.004 Rule 20 (l' :-> r') => unquote1(nil1) -> nil 0.004/0.004 Var => x7:S 0.004/0.004 Pos x7:S in l => [1,1] 0.004/0.004 Sigma => {x7:S -> unquote1(nil1)} 0.004/0.004 s => cons(x8:S,first(unquote1(nil1),x9:S)) 0.004/0.004 t => first(s(nil),cons(x8:S,x9:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 5 (l' :-> r') => first1(s(X:S),cons(Y:S,Z:S)) -> cons1(quote(Y:S),first1(X:S,Z:S)) 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> first1(s(X:S),cons(Y:S,Z:S))} 0.004/0.004 s => cons1(quote(first1(s(X:S),cons(Y:S,Z:S))),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(cons1(quote(Y:S),first1(X:S,Z:S)),x13:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 6 (l' :-> r') => from(X:S) -> cons(X:S,from(s(X:S))) 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> from(X:S)} 0.004/0.004 s => cons1(quote(from(X:S)),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(cons(X:S,from(s(X:S))),x13:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 7 (l' :-> r') => quote(sel(X:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> quote(sel(X:S,Z:S))} 0.004/0.004 s => cons1(quote(quote(sel(X:S,Z:S))),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(sel1(X:S,Z:S),x13:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 8 (l' :-> r') => quote(0) -> 01 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> quote(0)} 0.004/0.004 s => cons1(quote(quote(0)),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(01,x13:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 9 (l' :-> r') => quote(s(X:S)) -> s1(quote(X:S)) 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> quote(s(X:S))} 0.004/0.004 s => cons1(quote(quote(s(X:S))),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(s1(quote(X:S)),x13:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 10 (l' :-> r') => quote1(first(X:S,Z:S)) -> first1(X:S,Z:S) 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> quote1(first(X:S,Z:S))} 0.004/0.004 s => cons1(quote(quote1(first(X:S,Z:S))),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(first1(X:S,Z:S),x13:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 11 (l' :-> r') => quote1(cons(X:S,Z:S)) -> cons1(quote(X:S),quote1(Z:S)) 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> quote1(cons(X:S,Z:S))} 0.004/0.004 s => cons1(quote(quote1(cons(X:S,Z:S))),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(cons1(quote(X:S),quote1(Z:S)),x13:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 12 (l' :-> r') => quote1(nil) -> nil1 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> quote1(nil)} 0.004/0.004 s => cons1(quote(quote1(nil)),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(nil1,x13:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 13 (l' :-> r') => sel(0,cons(X:S,Z:S)) -> X:S 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> sel(0,cons(X:S,Z:S))} 0.004/0.004 s => cons1(quote(sel(0,cons(X:S,Z:S))),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(X:S,x13:S)) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 14 (l' :-> r') => sel(s(X:S),cons(Y:S,Z:S)) -> sel(X:S,Z:S) 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> sel(s(X:S),cons(Y:S,Z:S))} 0.004/0.004 s => cons1(quote(sel(s(X:S),cons(Y:S,Z:S))),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(sel(X:S,Z:S),x13:S)) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 15 (l' :-> r') => sel1(0,cons(X:S,Z:S)) -> quote(X:S) 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> sel1(0,cons(X:S,Z:S))} 0.004/0.004 s => cons1(quote(sel1(0,cons(X:S,Z:S))),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(quote(X:S),x13:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 16 (l' :-> r') => sel1(s(X:S),cons(Y:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> sel1(s(X:S),cons(Y:S,Z:S))} 0.004/0.004 s => cons1(quote(sel1(s(X:S),cons(Y:S,Z:S))),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(sel1(X:S,Z:S),x13:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 17 (l' :-> r') => unquote(01) -> 0 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> unquote(01)} 0.004/0.004 s => cons1(quote(unquote(01)),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(0,x13:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 18 (l' :-> r') => unquote(s1(X:S)) -> s(unquote(X:S)) 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> unquote(s1(X:S))} 0.004/0.004 s => cons1(quote(unquote(s1(X:S))),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(s(unquote(X:S)),x13:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 19 (l' :-> r') => unquote1(cons1(X:S,Z:S)) -> fcons(unquote(X:S),unquote1(Z:S)) 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> unquote1(cons1(X:S,Z:S))} 0.004/0.004 s => cons1(quote(unquote1(cons1(X:S,Z:S))),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(fcons(unquote(X:S),unquote1(Z:S)),x13:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)) 0.004/0.004 Rule 20 (l' :-> r') => unquote1(nil1) -> nil 0.004/0.004 Var => x12:S 0.004/0.004 Pos x12:S in l => [2,1] 0.004/0.004 Sigma => {x12:S -> unquote1(nil1)} 0.004/0.004 s => cons1(quote(unquote1(nil1)),first1(x11:S,x13:S)) 0.004/0.004 t => first1(s(x11:S),cons(nil,x13:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => from(x14:S) -> cons(x14:S,from(s(x14:S))) 0.004/0.004 Rule 6 (l' :-> r') => from(X:S) -> cons(X:S,from(s(X:S))) 0.004/0.004 Var => x14:S 0.004/0.004 Pos x14:S in l => [1] 0.004/0.004 Sigma => {x14:S -> from(X:S)} 0.004/0.004 s => cons(from(X:S),from(s(from(X:S)))) 0.004/0.004 t => from(cons(X:S,from(s(X:S)))) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => from(x14:S) -> cons(x14:S,from(s(x14:S))) 0.004/0.004 Rule 7 (l' :-> r') => quote(sel(X:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 Var => x14:S 0.004/0.004 Pos x14:S in l => [1] 0.004/0.004 Sigma => {x14:S -> quote(sel(X:S,Z:S))} 0.004/0.004 s => cons(quote(sel(X:S,Z:S)),from(s(quote(sel(X:S,Z:S))))) 0.004/0.004 t => from(sel1(X:S,Z:S)) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => from(x14:S) -> cons(x14:S,from(s(x14:S))) 0.004/0.004 Rule 8 (l' :-> r') => quote(0) -> 01 0.004/0.004 Var => x14:S 0.004/0.004 Pos x14:S in l => [1] 0.004/0.004 Sigma => {x14:S -> quote(0)} 0.004/0.004 s => cons(quote(0),from(s(quote(0)))) 0.004/0.004 t => from(01) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => from(x14:S) -> cons(x14:S,from(s(x14:S))) 0.004/0.004 Rule 9 (l' :-> r') => quote(s(X:S)) -> s1(quote(X:S)) 0.004/0.004 Var => x14:S 0.004/0.004 Pos x14:S in l => [1] 0.004/0.004 Sigma => {x14:S -> quote(s(X:S))} 0.004/0.004 s => cons(quote(s(X:S)),from(s(quote(s(X:S))))) 0.004/0.004 t => from(s1(quote(X:S))) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => from(x14:S) -> cons(x14:S,from(s(x14:S))) 0.004/0.004 Rule 10 (l' :-> r') => quote1(first(X:S,Z:S)) -> first1(X:S,Z:S) 0.004/0.004 Var => x14:S 0.004/0.004 Pos x14:S in l => [1] 0.004/0.004 Sigma => {x14:S -> quote1(first(X:S,Z:S))} 0.004/0.004 s => cons(quote1(first(X:S,Z:S)),from(s(quote1(first(X:S,Z:S))))) 0.004/0.004 t => from(first1(X:S,Z:S)) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => from(x14:S) -> cons(x14:S,from(s(x14:S))) 0.004/0.004 Rule 11 (l' :-> r') => quote1(cons(X:S,Z:S)) -> cons1(quote(X:S),quote1(Z:S)) 0.004/0.004 Var => x14:S 0.004/0.004 Pos x14:S in l => [1] 0.004/0.004 Sigma => {x14:S -> quote1(cons(X:S,Z:S))} 0.004/0.004 s => cons(quote1(cons(X:S,Z:S)),from(s(quote1(cons(X:S,Z:S))))) 0.004/0.004 t => from(cons1(quote(X:S),quote1(Z:S))) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => from(x14:S) -> cons(x14:S,from(s(x14:S))) 0.004/0.004 Rule 12 (l' :-> r') => quote1(nil) -> nil1 0.004/0.004 Var => x14:S 0.004/0.004 Pos x14:S in l => [1] 0.004/0.004 Sigma => {x14:S -> quote1(nil)} 0.004/0.004 s => cons(quote1(nil),from(s(quote1(nil)))) 0.004/0.004 t => from(nil1) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => from(x14:S) -> cons(x14:S,from(s(x14:S))) 0.004/0.004 Rule 13 (l' :-> r') => sel(0,cons(X:S,Z:S)) -> X:S 0.004/0.004 Var => x14:S 0.004/0.004 Pos x14:S in l => [1] 0.004/0.004 Sigma => {x14:S -> sel(0,cons(X:S,Z:S))} 0.004/0.004 s => cons(sel(0,cons(X:S,Z:S)),from(s(sel(0,cons(X:S,Z:S))))) 0.004/0.004 t => from(X:S) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => from(x14:S) -> cons(x14:S,from(s(x14:S))) 0.004/0.004 Rule 14 (l' :-> r') => sel(s(X:S),cons(Y:S,Z:S)) -> sel(X:S,Z:S) 0.004/0.004 Var => x14:S 0.004/0.004 Pos x14:S in l => [1] 0.004/0.004 Sigma => {x14:S -> sel(s(X:S),cons(Y:S,Z:S))} 0.004/0.004 s => cons(sel(s(X:S),cons(Y:S,Z:S)),from(s(sel(s(X:S),cons(Y:S,Z:S))))) 0.004/0.004 t => from(sel(X:S,Z:S)) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => from(x14:S) -> cons(x14:S,from(s(x14:S))) 0.004/0.004 Rule 15 (l' :-> r') => sel1(0,cons(X:S,Z:S)) -> quote(X:S) 0.004/0.004 Var => x14:S 0.004/0.004 Pos x14:S in l => [1] 0.004/0.004 Sigma => {x14:S -> sel1(0,cons(X:S,Z:S))} 0.004/0.004 s => cons(sel1(0,cons(X:S,Z:S)),from(s(sel1(0,cons(X:S,Z:S))))) 0.004/0.004 t => from(quote(X:S)) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => from(x14:S) -> cons(x14:S,from(s(x14:S))) 0.004/0.004 Rule 16 (l' :-> r') => sel1(s(X:S),cons(Y:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 Var => x14:S 0.004/0.004 Pos x14:S in l => [1] 0.004/0.004 Sigma => {x14:S -> sel1(s(X:S),cons(Y:S,Z:S))} 0.004/0.004 s => cons(sel1(s(X:S),cons(Y:S,Z:S)),from(s(sel1(s(X:S),cons(Y:S,Z:S))))) 0.004/0.004 t => from(sel1(X:S,Z:S)) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => from(x14:S) -> cons(x14:S,from(s(x14:S))) 0.004/0.004 Rule 17 (l' :-> r') => unquote(01) -> 0 0.004/0.004 Var => x14:S 0.004/0.004 Pos x14:S in l => [1] 0.004/0.004 Sigma => {x14:S -> unquote(01)} 0.004/0.004 s => cons(unquote(01),from(s(unquote(01)))) 0.004/0.004 t => from(0) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => from(x14:S) -> cons(x14:S,from(s(x14:S))) 0.004/0.004 Rule 18 (l' :-> r') => unquote(s1(X:S)) -> s(unquote(X:S)) 0.004/0.004 Var => x14:S 0.004/0.004 Pos x14:S in l => [1] 0.004/0.004 Sigma => {x14:S -> unquote(s1(X:S))} 0.004/0.004 s => cons(unquote(s1(X:S)),from(s(unquote(s1(X:S))))) 0.004/0.004 t => from(s(unquote(X:S))) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => from(x14:S) -> cons(x14:S,from(s(x14:S))) 0.004/0.004 Rule 19 (l' :-> r') => unquote1(cons1(X:S,Z:S)) -> fcons(unquote(X:S),unquote1(Z:S)) 0.004/0.004 Var => x14:S 0.004/0.004 Pos x14:S in l => [1] 0.004/0.004 Sigma => {x14:S -> unquote1(cons1(X:S,Z:S))} 0.004/0.004 s => cons(unquote1(cons1(X:S,Z:S)),from(s(unquote1(cons1(X:S,Z:S))))) 0.004/0.004 t => from(fcons(unquote(X:S),unquote1(Z:S))) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => from(x14:S) -> cons(x14:S,from(s(x14:S))) 0.004/0.004 Rule 20 (l' :-> r') => unquote1(nil1) -> nil 0.004/0.004 Var => x14:S 0.004/0.004 Pos x14:S in l => [1] 0.004/0.004 Sigma => {x14:S -> unquote1(nil1)} 0.004/0.004 s => cons(unquote1(nil1),from(s(unquote1(nil1)))) 0.004/0.004 t => from(nil) 0.004/0.004 NW => 0 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => sel1(0,cons(x27:S,x28:S)) -> quote(x27:S) 0.004/0.004 Rule 15 (l' :-> r') => sel1(0,cons(X:S,Z:S)) -> quote(X:S) 0.004/0.004 Var => x27:S 0.004/0.004 Pos x27:S in l => [2,1] 0.004/0.004 Sigma => {x27:S -> sel1(0,cons(X:S,Z:S))} 0.004/0.004 s => quote(sel1(0,cons(X:S,Z:S))) 0.004/0.004 t => sel1(0,cons(quote(X:S),x28:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => sel1(0,cons(x27:S,x28:S)) -> quote(x27:S) 0.004/0.004 Rule 16 (l' :-> r') => sel1(s(X:S),cons(Y:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 Var => x27:S 0.004/0.004 Pos x27:S in l => [2,1] 0.004/0.004 Sigma => {x27:S -> sel1(s(X:S),cons(Y:S,Z:S))} 0.004/0.004 s => quote(sel1(s(X:S),cons(Y:S,Z:S))) 0.004/0.004 t => sel1(0,cons(sel1(X:S,Z:S),x28:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => sel1(0,cons(x27:S,x28:S)) -> quote(x27:S) 0.004/0.004 Rule 17 (l' :-> r') => unquote(01) -> 0 0.004/0.004 Var => x27:S 0.004/0.004 Pos x27:S in l => [2,1] 0.004/0.004 Sigma => {x27:S -> unquote(01)} 0.004/0.004 s => quote(unquote(01)) 0.004/0.004 t => sel1(0,cons(0,x28:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => sel1(0,cons(x27:S,x28:S)) -> quote(x27:S) 0.004/0.004 Rule 18 (l' :-> r') => unquote(s1(X:S)) -> s(unquote(X:S)) 0.004/0.004 Var => x27:S 0.004/0.004 Pos x27:S in l => [2,1] 0.004/0.004 Sigma => {x27:S -> unquote(s1(X:S))} 0.004/0.004 s => quote(unquote(s1(X:S))) 0.004/0.004 t => sel1(0,cons(s(unquote(X:S)),x28:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => sel1(0,cons(x27:S,x28:S)) -> quote(x27:S) 0.004/0.004 Rule 19 (l' :-> r') => unquote1(cons1(X:S,Z:S)) -> fcons(unquote(X:S),unquote1(Z:S)) 0.004/0.004 Var => x27:S 0.004/0.004 Pos x27:S in l => [2,1] 0.004/0.004 Sigma => {x27:S -> unquote1(cons1(X:S,Z:S))} 0.004/0.004 s => quote(unquote1(cons1(X:S,Z:S))) 0.004/0.004 t => sel1(0,cons(fcons(unquote(X:S),unquote1(Z:S)),x28:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 ->Extended u-Critical Pair: 0.004/0.004 Rule 1 (l :-> r) => sel1(0,cons(x27:S,x28:S)) -> quote(x27:S) 0.004/0.004 Rule 20 (l' :-> r') => unquote1(nil1) -> nil 0.004/0.004 Var => x27:S 0.004/0.004 Pos x27:S in l => [2,1] 0.004/0.004 Sigma => {x27:S -> unquote1(nil1)} 0.004/0.004 s => quote(unquote1(nil1)) 0.004/0.004 t => sel1(0,cons(nil,x28:S)) 0.004/0.004 NW => 1 0.004/0.004 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Confluence Problem: 0.004/0.004 (VAR vNonEmpty:S X:S Y:S Z:S) 0.004/0.004 (STRATEGY CONTEXTSENSITIVE 0.004/0.004 (fcons 1 2) 0.004/0.004 (first 1 2) 0.004/0.004 (first1 1 2) 0.004/0.004 (from 1) 0.004/0.004 (quote) 0.004/0.004 (quote1) 0.004/0.004 (sel 1 2) 0.004/0.004 (sel1 1 2) 0.004/0.004 (unquote 1) 0.004/0.004 (unquote1 1) 0.004/0.004 (0) 0.004/0.004 (01) 0.004/0.004 (cons 1) 0.004/0.004 (cons1 1 2) 0.004/0.004 (fSNonEmpty) 0.004/0.004 (nil) 0.004/0.004 (nil1) 0.004/0.004 (s 1) 0.004/0.004 (s1 1) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 fcons(X:S,Z:S) -> cons(X:S,Z:S) 0.004/0.004 first(0,Z:S) -> nil 0.004/0.004 first(s(X:S),cons(Y:S,Z:S)) -> cons(Y:S,first(X:S,Z:S)) 0.004/0.004 first1(0,Z:S) -> nil1 0.004/0.004 first1(s(X:S),cons(Y:S,Z:S)) -> cons1(quote(Y:S),first1(X:S,Z:S)) 0.004/0.004 from(X:S) -> cons(X:S,from(s(X:S))) 0.004/0.004 quote(sel(X:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 quote(0) -> 01 0.004/0.004 quote(s(X:S)) -> s1(quote(X:S)) 0.004/0.004 quote1(first(X:S,Z:S)) -> first1(X:S,Z:S) 0.004/0.004 quote1(cons(X:S,Z:S)) -> cons1(quote(X:S),quote1(Z:S)) 0.004/0.004 quote1(nil) -> nil1 0.004/0.004 sel(0,cons(X:S,Z:S)) -> X:S 0.004/0.004 sel(s(X:S),cons(Y:S,Z:S)) -> sel(X:S,Z:S) 0.004/0.004 sel1(0,cons(X:S,Z:S)) -> quote(X:S) 0.004/0.004 sel1(s(X:S),cons(Y:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 unquote(01) -> 0 0.004/0.004 unquote(s1(X:S)) -> s(unquote(X:S)) 0.004/0.004 unquote1(cons1(X:S,Z:S)) -> fcons(unquote(X:S),unquote1(Z:S)) 0.004/0.004 unquote1(nil1) -> nil 0.004/0.004 ) 0.004/0.004 Critical Pairs: 0.004/0.004 => Not trivial, Not overlay, NW1, N1 0.004/0.004 => Not trivial, Not overlay, NW1, N2 0.004/0.004 => Not trivial, Not overlay, NW1, N3 0.004/0.004 => Not trivial, Not overlay, NW1, N4 0.004/0.004 => Not trivial, Not overlay, NW1, N5 0.004/0.004 => Not trivial, Not overlay, NW1, N6 0.004/0.004 => Not trivial, Not overlay, NW1, N7 0.004/0.004 => Not trivial, Not overlay, NW1, N8 0.004/0.004 => Not trivial, Not overlay, NW1, N9 0.004/0.004 => Not trivial, Not overlay, NW1, N10 0.004/0.004 => Not trivial, Not overlay, NW1, N11 0.004/0.004 => Not trivial, Not overlay, NW1, N12 0.004/0.004 => Not trivial, Not overlay, NW1, N13 0.004/0.004 => Not trivial, Not overlay, NW1, N14 0.004/0.004 => Not trivial, Not overlay, NW1, N15 0.004/0.004 => Not trivial, Not overlay, NW1, N16 0.004/0.004 => Not trivial, Not overlay, NW1, N17 0.004/0.004 => Not trivial, Not overlay, NW1, N18 0.004/0.004 => Not trivial, Not overlay, NW1, N19 0.004/0.004 => Not trivial, Not overlay, NW1, N20 0.004/0.004 => Not trivial, Not overlay, NW1, N21 0.004/0.004 => Not trivial, Not overlay, NW1, N22 0.004/0.004 => Not trivial, Not overlay, NW1, N23 0.004/0.004 => Not trivial, Not overlay, NW1, N24 0.004/0.004 => Not trivial, Not overlay, NW1, N25 0.004/0.004 => Not trivial, Not overlay, NW1, N26 0.004/0.004 => Not trivial, Not overlay, NW1, N27 0.004/0.004 => Not trivial, Not overlay, NW1, N28 0.004/0.004 => Not trivial, Not overlay, NW1, N29 0.004/0.004 => Not trivial, Not overlay, NW1, N30 0.004/0.004 => Not trivial, Not overlay, NW1, N31 0.004/0.004 => Not trivial, Not overlay, NW1, N32 0.004/0.004 => Not trivial, Not overlay, NW1, N33 0.004/0.004 => Not trivial, Not overlay, NW1, N34 0.004/0.004 => Not trivial, Not overlay, NW1, N35 0.004/0.004 => Not trivial, Not overlay, NW1, N36 0.004/0.004 => Not trivial, Not overlay, NW1, N37 0.004/0.004 => Not trivial, Not overlay, NW1, N38 0.004/0.004 => Not trivial, Not overlay, NW1, N39 0.004/0.004 => Not trivial, Not overlay, NW1, N40 0.004/0.004 => Not trivial, Not overlay, NW1, N41 0.004/0.004 => Not trivial, Not overlay, NW1, N42 0.004/0.004 => Not trivial, Not overlay, NW1, N43 0.004/0.004 => Not trivial, Not overlay, NW1, N44 0.004/0.004 => Not trivial, Not overlay, NW1, N45 0.004/0.004 => Not trivial, Not overlay, NW1, N46 0.004/0.004 => Not trivial, Not overlay, NW0, N47 0.004/0.004 => Not trivial, Not overlay, NW0, N48 0.004/0.004 => Not trivial, Not overlay, NW1, N49 0.004/0.004 => Not trivial, Not overlay, NW1, N50 0.004/0.004 => Not trivial, Not overlay, NW1, N51 0.004/0.004 => Not trivial, Not overlay, NW1, N52 0.004/0.004 => Not trivial, Not overlay, NW1, N53 0.004/0.004 => Not trivial, Not overlay, NW1, N54 0.004/0.004 => Not trivial, Not overlay, NW0, N55 0.004/0.004 => Not trivial, Not overlay, NW0, N56 0.004/0.004 => Not trivial, Not overlay, NW0, N57 0.004/0.004 => Not trivial, Not overlay, NW0, N58 0.004/0.004 => Not trivial, Not overlay, NW0, N59 0.004/0.004 => Not trivial, Not overlay, NW0, N60 0.004/0.004 => Not trivial, Not overlay, NW0, N61 0.004/0.004 => Not trivial, Not overlay, NW0, N62 0.004/0.004 => Not trivial, Not overlay, NW0, N63 0.004/0.004 => Not trivial, Not overlay, NW0, N64 0.004/0.004 => Not trivial, Not overlay, NW0, N65 0.004/0.004 => Not trivial, Not overlay, NW0, N66 0.004/0.004 => Not trivial, Not overlay, NW0, N67 0.004/0.004 => Not trivial, Not overlay, NW0, N68 0.004/0.004 => Not trivial, Not overlay, NW0, N69 0.004/0.004 => Not trivial, Not overlay, NW1, N70 0.004/0.004 => Not trivial, Not overlay, NW1, N71 0.004/0.004 => Not trivial, Not overlay, NW1, N72 0.004/0.004 => Not trivial, Not overlay, NW1, N73 0.004/0.004 => Not trivial, Not overlay, NW1, N74 0.004/0.004 => Not trivial, Not overlay, NW1, N75 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 0.004/0.004 Huet Levy Processor: 0.004/0.004 -> Rules: 0.004/0.004 fcons(X:S,Z:S) -> cons(X:S,Z:S) 0.004/0.004 first(0,Z:S) -> nil 0.004/0.004 first(s(X:S),cons(Y:S,Z:S)) -> cons(Y:S,first(X:S,Z:S)) 0.004/0.004 first1(0,Z:S) -> nil1 0.004/0.004 first1(s(X:S),cons(Y:S,Z:S)) -> cons1(quote(Y:S),first1(X:S,Z:S)) 0.004/0.004 from(X:S) -> cons(X:S,from(s(X:S))) 0.004/0.004 quote(sel(X:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 quote(0) -> 01 0.004/0.004 quote(s(X:S)) -> s1(quote(X:S)) 0.004/0.004 quote1(first(X:S,Z:S)) -> first1(X:S,Z:S) 0.004/0.004 quote1(cons(X:S,Z:S)) -> cons1(quote(X:S),quote1(Z:S)) 0.004/0.004 quote1(nil) -> nil1 0.004/0.004 sel(0,cons(X:S,Z:S)) -> X:S 0.004/0.004 sel(s(X:S),cons(Y:S,Z:S)) -> sel(X:S,Z:S) 0.004/0.004 sel1(0,cons(X:S,Z:S)) -> quote(X:S) 0.004/0.004 sel1(s(X:S),cons(Y:S,Z:S)) -> sel1(X:S,Z:S) 0.004/0.004 unquote(01) -> 0 0.004/0.004 unquote(s1(X:S)) -> s(unquote(X:S)) 0.004/0.004 unquote1(cons1(X:S,Z:S)) -> fcons(unquote(X:S),unquote1(Z:S)) 0.004/0.004 unquote1(nil1) -> nil 0.004/0.004 -> Vars: 0.004/0.004 X, Z, Z, X, Y, Z, Z, X, Y, Z, X, X, Z, X, X, Z, X, Z, X, Z, X, Y, Z, X, Z, X, Y, Z, X, X, Z 0.004/0.004 -> UVars: 0.004/0.004 (UV-RuleId: 1, UV-LActive: [X, Z], UV-RActive: [X], UV-LFrozen: [], UV-RFrozen: [Z]) 0.004/0.004 (UV-RuleId: 2, UV-LActive: [Z], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.004/0.004 (UV-RuleId: 3, UV-LActive: [X, Y], UV-RActive: [Y], UV-LFrozen: [Z], UV-RFrozen: [X, Z]) 0.004/0.004 (UV-RuleId: 4, UV-LActive: [Z], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.004/0.004 (UV-RuleId: 5, UV-LActive: [X, Y], UV-RActive: [X, Z], UV-LFrozen: [Z], UV-RFrozen: [Y]) 0.004/0.004 (UV-RuleId: 6, UV-LActive: [X], UV-RActive: [X], UV-LFrozen: [], UV-RFrozen: [X]) 0.004/0.004 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [X, Z], UV-LFrozen: [X, Z], UV-RFrozen: []) 0.004/0.004 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.004/0.004 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X], UV-RFrozen: [X]) 0.004/0.004 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [X, Z], UV-LFrozen: [X, Z], UV-RFrozen: []) 0.004/0.004 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X, Z], UV-RFrozen: [X, Z]) 0.004/0.004 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.004/0.004 (UV-RuleId: 13, UV-LActive: [X], UV-RActive: [X], UV-LFrozen: [Z], UV-RFrozen: []) 0.004/0.004 (UV-RuleId: 14, UV-LActive: [X, Y], UV-RActive: [X, Z], UV-LFrozen: [Z], UV-RFrozen: []) 0.004/0.004 (UV-RuleId: 15, UV-LActive: [X], UV-RActive: [], UV-LFrozen: [Z], UV-RFrozen: [X]) 0.004/0.004 (UV-RuleId: 16, UV-LActive: [X, Y], UV-RActive: [X, Z], UV-LFrozen: [Z], UV-RFrozen: []) 0.004/0.004 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.004/0.004 (UV-RuleId: 18, UV-LActive: [X], UV-RActive: [X], UV-LFrozen: [], UV-RFrozen: []) 0.004/0.004 (UV-RuleId: 19, UV-LActive: [X, Z], UV-RActive: [X, Z], UV-LFrozen: [], UV-RFrozen: []) 0.004/0.004 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.004/0.004 -> FVars: 0.004/0.004 x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34 0.004/0.004 -> PVars: 0.004/0.004 X: [x4, x7, x11, x14, x15, x17, x18, x20, x22, x24, x27, x29, x32, x33], Z: [x5, x6, x9, x10, x13, x16, x19, x21, x23, x26, x28, x31, x34], Y: [x8, x12, x25, x30] 0.004/0.004 0.004/0.004 -> Rlps: 0.004/0.004 (rule: fcons(x4:S,x5:S) -> cons(x4:S,x5:S), id: 1, possubterms: fcons(x4:S,x5:S)->[]) 0.004/0.004 (rule: first(0,x6:S) -> nil, id: 2, possubterms: first(0,x6:S)->[], 0->[1]) 0.004/0.004 (rule: first(s(x7:S),cons(x8:S,x9:S)) -> cons(x8:S,first(x7:S,x9:S)), id: 3, possubterms: first(s(x7:S),cons(x8:S,x9:S))->[], s(x7:S)->[1], cons(x8:S,x9:S)->[2]) 0.004/0.004 (rule: first1(0,x10:S) -> nil1, id: 4, possubterms: first1(0,x10:S)->[], 0->[1]) 0.004/0.004 (rule: first1(s(x11:S),cons(x12:S,x13:S)) -> cons1(quote(x12:S),first1(x11:S,x13:S)), id: 5, possubterms: first1(s(x11:S),cons(x12:S,x13:S))->[], s(x11:S)->[1], cons(x12:S,x13:S)->[2]) 0.004/0.004 (rule: from(x14:S) -> cons(x14:S,from(s(x14:S))), id: 6, possubterms: from(x14:S)->[]) 0.004/0.004 (rule: quote(sel(x15:S,x16:S)) -> sel1(x15:S,x16:S), id: 7, possubterms: quote(sel(x15:S,x16:S))->[]) 0.004/0.004 (rule: quote(0) -> 01, id: 8, possubterms: quote(0)->[]) 0.004/0.004 (rule: quote(s(x17:S)) -> s1(quote(x17:S)), id: 9, possubterms: quote(s(x17:S))->[]) 0.004/0.004 (rule: quote1(first(x18:S,x19:S)) -> first1(x18:S,x19:S), id: 10, possubterms: quote1(first(x18:S,x19:S))->[]) 0.004/0.004 (rule: quote1(cons(x20:S,x21:S)) -> cons1(quote(x20:S),quote1(x21:S)), id: 11, possubterms: quote1(cons(x20:S,x21:S))->[]) 0.004/0.004 (rule: quote1(nil) -> nil1, id: 12, possubterms: quote1(nil)->[]) 0.004/0.004 (rule: sel(0,cons(x22:S,x23:S)) -> x22:S, id: 13, possubterms: sel(0,cons(x22:S,x23:S))->[], 0->[1], cons(x22:S,x23:S)->[2]) 0.004/0.004 (rule: sel(s(x24:S),cons(x25:S,x26:S)) -> sel(x24:S,x26:S), id: 14, possubterms: sel(s(x24:S),cons(x25:S,x26:S))->[], s(x24:S)->[1], cons(x25:S,x26:S)->[2]) 0.004/0.004 (rule: sel1(0,cons(x27:S,x28:S)) -> quote(x27:S), id: 15, possubterms: sel1(0,cons(x27:S,x28:S))->[], 0->[1], cons(x27:S,x28:S)->[2]) 0.004/0.004 (rule: sel1(s(x29:S),cons(x30:S,x31:S)) -> sel1(x29:S,x31:S), id: 16, possubterms: sel1(s(x29:S),cons(x30:S,x31:S))->[], s(x29:S)->[1], cons(x30:S,x31:S)->[2]) 0.004/0.004 (rule: unquote(01) -> 0, id: 17, possubterms: unquote(01)->[], 01->[1]) 0.004/0.004 (rule: unquote(s1(x32:S)) -> s(unquote(x32:S)), id: 18, possubterms: unquote(s1(x32:S))->[], s1(x32:S)->[1]) 0.004/0.004 (rule: unquote1(cons1(x33:S,x34:S)) -> fcons(unquote(x33:S),unquote1(x34:S)), id: 19, possubterms: unquote1(cons1(x33:S,x34:S))->[], cons1(x33:S,x34:S)->[1]) 0.004/0.004 (rule: unquote1(nil1) -> nil, id: 20, possubterms: unquote1(nil1)->[], nil1->[1]) 0.004/0.004 0.004/0.004 -> Unifications: 0.004/0.004 0.004/0.004 0.004/0.004 -> Critical pairs info: 0.004/0.004 => Not trivial, Not overlay, NW1, N1 0.004/0.004 => Not trivial, Not overlay, NW0, N2 0.004/0.004 => Not trivial, Not overlay, NW0, N3 0.004/0.004 => Not trivial, Not overlay, NW0, N4 0.004/0.004 => Not trivial, Not overlay, NW1, N5 0.004/0.004 => Not trivial, Not overlay, NW1, N6 0.004/0.004 => Not trivial, Not overlay, NW1, N7 0.004/0.004 => Not trivial, Not overlay, NW1, N8 0.004/0.004 => Not trivial, Not overlay, NW1, N9 0.004/0.004 => Not trivial, Not overlay, NW1, N10 0.004/0.004 => Not trivial, Not overlay, NW1, N11 0.004/0.004 => Not trivial, Not overlay, NW1, N12 0.004/0.004 => Not trivial, Not overlay, NW0, N13 0.004/0.004 => Not trivial, Not overlay, NW1, N14 0.004/0.004 => Not trivial, Not overlay, NW1, N15 0.004/0.004 => Not trivial, Not overlay, NW1, N16 0.004/0.004 => Not trivial, Not overlay, NW1, N17 0.004/0.004 => Not trivial, Not overlay, NW1, N18 0.004/0.004 => Not trivial, Not overlay, NW1, N19 0.004/0.004 => Not trivial, Not overlay, NW1, N20 0.004/0.004 => Not trivial, Not overlay, NW1, N21 0.004/0.004 => Not trivial, Not overlay, NW1, N22 0.004/0.004 => Not trivial, Not overlay, NW0, N23 0.004/0.004 => Not trivial, Not overlay, NW0, N24 0.004/0.004 => Not trivial, Not overlay, NW1, N25 0.004/0.004 => Not trivial, Not overlay, NW1, N26 0.004/0.004 => Not trivial, Not overlay, NW0, N27 0.004/0.004 => Not trivial, Not overlay, NW1, N28 0.004/0.004 => Not trivial, Not overlay, NW0, N29 0.004/0.004 => Not trivial, Not overlay, NW1, N30 0.004/0.004 => Not trivial, Not overlay, NW1, N31 0.004/0.004 => Not trivial, Not overlay, NW1, N32 0.004/0.004 => Not trivial, Not overlay, NW1, N33 0.004/0.004 => Not trivial, Not overlay, NW1, N34 0.004/0.004 => Not trivial, Not overlay, NW1, N35 0.004/0.004 => Not trivial, Not overlay, NW1, N36 0.004/0.004 => Not trivial, Not overlay, NW0, N37 0.004/0.004 => Not trivial, Not overlay, NW1, N38 0.004/0.004 => Not trivial, Not overlay, NW1, N39 0.004/0.004 => Not trivial, Not overlay, NW1, N40 0.004/0.004 => Not trivial, Not overlay, NW1, N41 0.004/0.004 => Not trivial, Not overlay, NW1, N42 0.004/0.004 => Not trivial, Not overlay, NW0, N43 0.004/0.004 => Not trivial, Not overlay, NW1, N44 0.004/0.004 => Not trivial, Not overlay, NW1, N45 0.004/0.004 => Not trivial, Not overlay, NW1, N46 0.004/0.004 => Not trivial, Not overlay, NW0, N47 0.004/0.004 => Not trivial, Not overlay, NW0, N48 0.004/0.004 => Not trivial, Not overlay, NW1, N49 0.004/0.004 => Not trivial, Not overlay, NW1, N50 0.004/0.004 => Not trivial, Not overlay, NW1, N51 0.004/0.004 => Not trivial, Not overlay, NW1, N52 0.004/0.004 => Not trivial, Not overlay, NW1, N53 0.004/0.004 => Not trivial, Not overlay, NW1, N54 0.004/0.004 => Not trivial, Not overlay, NW1, N55 0.004/0.004 => Not trivial, Not overlay, NW1, N56 0.004/0.004 => Not trivial, Not overlay, NW0, N57 0.004/0.004 => Not trivial, Not overlay, NW0, N58 0.004/0.004 => Not trivial, Not overlay, NW1, N59 0.004/0.004 => Not trivial, Not overlay, NW1, N60 0.004/0.004 => Not trivial, Not overlay, NW1, N61 0.004/0.004 => Not trivial, Not overlay, NW0, N62 0.004/0.004 => Not trivial, Not overlay, NW1, N63 0.004/0.004 => Not trivial, Not overlay, NW1, N64 0.004/0.004 => Not trivial, Not overlay, NW1, N65 0.004/0.004 => Not trivial, Not overlay, NW1, N66 0.004/0.004 => Not trivial, Not overlay, NW1, N67 0.004/0.004 => Not trivial, Not overlay, NW1, N68 0.004/0.004 => Not trivial, Not overlay, NW0, N69 0.004/0.004 => Not trivial, Not overlay, NW1, N70 0.004/0.004 => Not trivial, Not overlay, NW1, N71 0.004/0.004 => Not trivial, Not overlay, NW1, N72 0.004/0.004 => Not trivial, Not overlay, NW1, N73 0.004/0.004 => Not trivial, Not overlay, NW1, N74 0.004/0.004 => Not trivial, Not overlay, NW0, N75 0.004/0.004 0.004/0.004 -> Problem conclusions: 0.004/0.004 Left linear, Not right linear, Not linear 0.004/0.004 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.004/0.004 Not Huet-Levy confluent, Not Newman confluent 0.004/0.004 R is a CS-TRS, Not left-homogeneous u-replacing variables 0.004/0.004 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 No Convergence Brute Force Processor: 0.004/0.004 -> Rewritings: 0.004/0.004 s: cons(X:S,unquote(s1(X:S))) 0.004/0.004 Nodes: [0] 0.004/0.004 Edges: [] 0.004/0.004 ID: 0 => ('cons(X:S,unquote(s1(X:S)))', D0) 0.004/0.004 t: fcons(X:S,s(unquote(X:S))) 0.004/0.004 Nodes: [0,1] 0.004/0.004 Edges: [(0,1)] 0.004/0.004 ID: 0 => ('fcons(X:S,s(unquote(X:S)))', D0) 0.004/0.004 ID: 1 => ('cons(X:S,s(unquote(X:S)))', D1, R1, P[], S{x4:S -> X:S, x5:S -> s(unquote(X:S))}), NR: 'cons(X:S,s(unquote(X:S)))' 0.004/0.004 cons(X:S,unquote(s1(X:S))) ->* no union *<- fcons(X:S,s(unquote(X:S))) 0.004/0.004 "Not joinable" 0.004/0.004 0.004/0.004 The problem is not joinable. 0.004/0.004 0.04user 0.00system 0:00.04elapsed 95%CPU (0avgtext+0avgdata 15632maxresident)k 0.004/0.004 0inputs+0outputs (0major+2195minor)pagefaults 0swaps