0.002/0.002 NO 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S N:S X:S XS:S Y:S YS:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (incr 1) 0.002/0.002 (oddNs) 0.002/0.002 (pairNs) 0.002/0.002 (repItems 1) 0.002/0.002 (tail 1) 0.002/0.002 (take 1 2) 0.002/0.002 (zip 1 2) 0.002/0.002 (0) 0.002/0.002 (cons 1) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (pair 1 2) 0.002/0.002 (s 1) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 incr(cons(X:S,XS:S)) -> cons(s(X:S),incr(XS:S)) 0.002/0.002 oddNs -> incr(pairNs) 0.002/0.002 pairNs -> cons(0,incr(oddNs)) 0.002/0.002 repItems(cons(X:S,XS:S)) -> cons(X:S,cons(X:S,repItems(XS:S))) 0.002/0.002 repItems(nil) -> nil 0.002/0.002 tail(cons(X:S,XS:S)) -> XS:S 0.002/0.002 take(0,XS:S) -> nil 0.002/0.002 take(s(N:S),cons(X:S,XS:S)) -> cons(X:S,take(N:S,XS:S)) 0.002/0.002 zip(cons(X:S,XS:S),cons(Y:S,YS:S)) -> cons(pair(X:S,Y:S),zip(XS:S,YS:S)) 0.002/0.002 zip(nil,XS:S) -> nil 0.002/0.002 zip(X:S,nil) -> nil 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 CleanTRS Processor: 0.002/0.002 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S N:S X:S XS:S Y:S YS:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (incr 1) 0.002/0.002 (oddNs) 0.002/0.002 (pairNs) 0.002/0.002 (repItems 1) 0.002/0.002 (tail 1) 0.002/0.002 (take 1 2) 0.002/0.002 (zip 1 2) 0.002/0.002 (0) 0.002/0.002 (cons 1) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (pair 1 2) 0.002/0.002 (s 1) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 incr(cons(X:S,XS:S)) -> cons(s(X:S),incr(XS:S)) 0.002/0.002 oddNs -> incr(pairNs) 0.002/0.002 pairNs -> cons(0,incr(oddNs)) 0.002/0.002 repItems(cons(X:S,XS:S)) -> cons(X:S,cons(X:S,repItems(XS:S))) 0.002/0.002 repItems(nil) -> nil 0.002/0.002 tail(cons(X:S,XS:S)) -> XS:S 0.002/0.002 take(0,XS:S) -> nil 0.002/0.002 take(s(N:S),cons(X:S,XS:S)) -> cons(X:S,take(N:S,XS:S)) 0.002/0.002 zip(cons(X:S,XS:S),cons(Y:S,YS:S)) -> cons(pair(X:S,Y:S),zip(XS:S,YS:S)) 0.002/0.002 zip(nil,XS:S) -> nil 0.002/0.002 zip(X:S,nil) -> nil 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 Modular Confluence Combinations Decomposition Processor: 0.002/0.002 It is a CTRS -> No modular confluence 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 CS-TRS Processor: 0.002/0.002 R is a CS-TRS 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S N:S X:S XS:S Y:S YS:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (incr 1) 0.002/0.002 (oddNs) 0.002/0.002 (pairNs) 0.002/0.002 (repItems 1) 0.002/0.002 (tail 1) 0.002/0.002 (take 1 2) 0.002/0.002 (zip 1 2) 0.002/0.002 (0) 0.002/0.002 (cons 1) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (pair 1 2) 0.002/0.002 (s 1) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 incr(cons(X:S,XS:S)) -> cons(s(X:S),incr(XS:S)) 0.002/0.002 oddNs -> incr(pairNs) 0.002/0.002 pairNs -> cons(0,incr(oddNs)) 0.002/0.002 repItems(cons(X:S,XS:S)) -> cons(X:S,cons(X:S,repItems(XS:S))) 0.002/0.002 repItems(nil) -> nil 0.002/0.002 tail(cons(X:S,XS:S)) -> XS:S 0.002/0.002 take(0,XS:S) -> nil 0.002/0.002 take(s(N:S),cons(X:S,XS:S)) -> cons(X:S,take(N:S,XS:S)) 0.002/0.002 zip(cons(X:S,XS:S),cons(Y:S,YS:S)) -> cons(pair(X:S,Y:S),zip(XS:S,YS:S)) 0.002/0.002 zip(nil,XS:S) -> nil 0.002/0.002 zip(X:S,nil) -> nil 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 Extended u-Critical Pairs NonLHRV Processor [JLAMP21]: 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => repItems(cons(x8:S,x9:S)) -> cons(x8:S,cons(x8:S,repItems(x9:S))) 0.002/0.002 Rule 4 (l' :-> r') => repItems(cons(X:S,XS:S)) -> cons(X:S,cons(X:S,repItems(XS:S))) 0.002/0.002 Var => x8:S 0.002/0.002 Pos x8:S in l => [1,1] 0.002/0.002 Sigma => {x8:S -> repItems(cons(X:S,XS:S))} 0.002/0.002 s => cons(repItems(cons(X:S,XS:S)),cons(repItems(cons(X:S,XS:S)),repItems(x9:S))) 0.002/0.002 t => repItems(cons(cons(X:S,cons(X:S,repItems(XS:S))),x9:S)) 0.002/0.002 NW => 0 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => repItems(cons(x8:S,x9:S)) -> cons(x8:S,cons(x8:S,repItems(x9:S))) 0.002/0.002 Rule 5 (l' :-> r') => repItems(nil) -> nil 0.002/0.002 Var => x8:S 0.002/0.002 Pos x8:S in l => [1,1] 0.002/0.002 Sigma => {x8:S -> repItems(nil)} 0.002/0.002 s => cons(repItems(nil),cons(repItems(nil),repItems(x9:S))) 0.002/0.002 t => repItems(cons(nil,x9:S)) 0.002/0.002 NW => 0 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => repItems(cons(x8:S,x9:S)) -> cons(x8:S,cons(x8:S,repItems(x9:S))) 0.002/0.002 Rule 6 (l' :-> r') => tail(cons(X:S,XS:S)) -> XS:S 0.002/0.002 Var => x8:S 0.002/0.002 Pos x8:S in l => [1,1] 0.002/0.002 Sigma => {x8:S -> tail(cons(X:S,XS:S))} 0.002/0.002 s => cons(tail(cons(X:S,XS:S)),cons(tail(cons(X:S,XS:S)),repItems(x9:S))) 0.002/0.002 t => repItems(cons(XS:S,x9:S)) 0.002/0.002 NW => 0 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => repItems(cons(x8:S,x9:S)) -> cons(x8:S,cons(x8:S,repItems(x9:S))) 0.002/0.002 Rule 7 (l' :-> r') => take(0,XS:S) -> nil 0.002/0.002 Var => x8:S 0.002/0.002 Pos x8:S in l => [1,1] 0.002/0.002 Sigma => {x8:S -> take(0,XS:S)} 0.002/0.002 s => cons(take(0,XS:S),cons(take(0,XS:S),repItems(x9:S))) 0.002/0.002 t => repItems(cons(nil,x9:S)) 0.002/0.002 NW => 0 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => repItems(cons(x8:S,x9:S)) -> cons(x8:S,cons(x8:S,repItems(x9:S))) 0.002/0.002 Rule 8 (l' :-> r') => take(s(N:S),cons(X:S,XS:S)) -> cons(X:S,take(N:S,XS:S)) 0.002/0.002 Var => x8:S 0.002/0.002 Pos x8:S in l => [1,1] 0.002/0.002 Sigma => {x8:S -> take(s(N:S),cons(X:S,XS:S))} 0.002/0.002 s => cons(take(s(N:S),cons(X:S,XS:S)),cons(take(s(N:S),cons(X:S,XS:S)),repItems(x9:S))) 0.002/0.002 t => repItems(cons(cons(X:S,take(N:S,XS:S)),x9:S)) 0.002/0.002 NW => 0 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => repItems(cons(x8:S,x9:S)) -> cons(x8:S,cons(x8:S,repItems(x9:S))) 0.002/0.002 Rule 9 (l' :-> r') => zip(cons(X:S,XS:S),cons(Y:S,YS:S)) -> cons(pair(X:S,Y:S),zip(XS:S,YS:S)) 0.002/0.002 Var => x8:S 0.002/0.002 Pos x8:S in l => [1,1] 0.002/0.002 Sigma => {x8:S -> zip(cons(X:S,XS:S),cons(Y:S,YS:S))} 0.002/0.002 s => cons(zip(cons(X:S,XS:S),cons(Y:S,YS:S)),cons(zip(cons(X:S,XS:S),cons(Y:S,YS:S)),repItems(x9:S))) 0.002/0.002 t => repItems(cons(cons(pair(X:S,Y:S),zip(XS:S,YS:S)),x9:S)) 0.002/0.002 NW => 0 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => repItems(cons(x8:S,x9:S)) -> cons(x8:S,cons(x8:S,repItems(x9:S))) 0.002/0.002 Rule 10 (l' :-> r') => zip(nil,XS:S) -> nil 0.002/0.002 Var => x8:S 0.002/0.002 Pos x8:S in l => [1,1] 0.002/0.002 Sigma => {x8:S -> zip(nil,XS:S)} 0.002/0.002 s => cons(zip(nil,XS:S),cons(zip(nil,XS:S),repItems(x9:S))) 0.002/0.002 t => repItems(cons(nil,x9:S)) 0.002/0.002 NW => 0 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => repItems(cons(x8:S,x9:S)) -> cons(x8:S,cons(x8:S,repItems(x9:S))) 0.002/0.002 Rule 11 (l' :-> r') => zip(X:S,nil) -> nil 0.002/0.002 Var => x8:S 0.002/0.002 Pos x8:S in l => [1,1] 0.002/0.002 Sigma => {x8:S -> zip(X:S,nil)} 0.002/0.002 s => cons(zip(X:S,nil),cons(zip(X:S,nil),repItems(x9:S))) 0.002/0.002 t => repItems(cons(nil,x9:S)) 0.002/0.002 NW => 0 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => take(s(x13:S),cons(x14:S,x15:S)) -> cons(x14:S,take(x13:S,x15:S)) 0.002/0.002 Rule 8 (l' :-> r') => take(s(N:S),cons(X:S,XS:S)) -> cons(X:S,take(N:S,XS:S)) 0.002/0.002 Var => x13:S 0.002/0.002 Pos x13:S in l => [1,1] 0.002/0.002 Sigma => {x13:S -> take(s(N:S),cons(X:S,XS:S))} 0.002/0.002 s => cons(x14:S,take(take(s(N:S),cons(X:S,XS:S)),x15:S)) 0.002/0.002 t => take(s(cons(X:S,take(N:S,XS:S))),cons(x14:S,x15:S)) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => take(s(x13:S),cons(x14:S,x15:S)) -> cons(x14:S,take(x13:S,x15:S)) 0.002/0.002 Rule 9 (l' :-> r') => zip(cons(X:S,XS:S),cons(Y:S,YS:S)) -> cons(pair(X:S,Y:S),zip(XS:S,YS:S)) 0.002/0.002 Var => x13:S 0.002/0.002 Pos x13:S in l => [1,1] 0.002/0.002 Sigma => {x13:S -> zip(cons(X:S,XS:S),cons(Y:S,YS:S))} 0.002/0.002 s => cons(x14:S,take(zip(cons(X:S,XS:S),cons(Y:S,YS:S)),x15:S)) 0.002/0.002 t => take(s(cons(pair(X:S,Y:S),zip(XS:S,YS:S))),cons(x14:S,x15:S)) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => take(s(x13:S),cons(x14:S,x15:S)) -> cons(x14:S,take(x13:S,x15:S)) 0.002/0.002 Rule 10 (l' :-> r') => zip(nil,XS:S) -> nil 0.002/0.002 Var => x13:S 0.002/0.002 Pos x13:S in l => [1,1] 0.002/0.002 Sigma => {x13:S -> zip(nil,XS:S)} 0.002/0.002 s => cons(x14:S,take(zip(nil,XS:S),x15:S)) 0.002/0.002 t => take(s(nil),cons(x14:S,x15:S)) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => take(s(x13:S),cons(x14:S,x15:S)) -> cons(x14:S,take(x13:S,x15:S)) 0.002/0.002 Rule 11 (l' :-> r') => zip(X:S,nil) -> nil 0.002/0.002 Var => x13:S 0.002/0.002 Pos x13:S in l => [1,1] 0.002/0.002 Sigma => {x13:S -> zip(X:S,nil)} 0.002/0.002 s => cons(x14:S,take(zip(X:S,nil),x15:S)) 0.002/0.002 t => take(s(nil),cons(x14:S,x15:S)) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S N:S X:S XS:S Y:S YS:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (incr 1) 0.002/0.002 (oddNs) 0.002/0.002 (pairNs) 0.002/0.002 (repItems 1) 0.002/0.002 (tail 1) 0.002/0.002 (take 1 2) 0.002/0.002 (zip 1 2) 0.002/0.002 (0) 0.002/0.002 (cons 1) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (pair 1 2) 0.002/0.002 (s 1) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 incr(cons(X:S,XS:S)) -> cons(s(X:S),incr(XS:S)) 0.002/0.002 oddNs -> incr(pairNs) 0.002/0.002 pairNs -> cons(0,incr(oddNs)) 0.002/0.002 repItems(cons(X:S,XS:S)) -> cons(X:S,cons(X:S,repItems(XS:S))) 0.002/0.002 repItems(nil) -> nil 0.002/0.002 tail(cons(X:S,XS:S)) -> XS:S 0.002/0.002 take(0,XS:S) -> nil 0.002/0.002 take(s(N:S),cons(X:S,XS:S)) -> cons(X:S,take(N:S,XS:S)) 0.002/0.002 zip(cons(X:S,XS:S),cons(Y:S,YS:S)) -> cons(pair(X:S,Y:S),zip(XS:S,YS:S)) 0.002/0.002 zip(nil,XS:S) -> nil 0.002/0.002 zip(X:S,nil) -> nil 0.002/0.002 ) 0.002/0.002 Critical Pairs: 0.002/0.002 => Not trivial, Not overlay, NW0, N1 0.002/0.002 => Not trivial, Not overlay, NW0, N2 0.002/0.002 => Not trivial, Not overlay, NW0, N3 0.002/0.002 => Not trivial, Not overlay, NW0, N4 0.002/0.002 => Not trivial, Not overlay, NW0, N5 0.002/0.002 => Not trivial, Not overlay, NW0, N6 0.002/0.002 => Not trivial, Not overlay, NW0, N7 0.002/0.002 => Not trivial, Not overlay, NW0, N8 0.002/0.002 => Not trivial, Not overlay, NW1, N9 0.002/0.002 => Not trivial, Not overlay, NW1, N10 0.002/0.002 => Not trivial, Not overlay, NW1, N11 0.002/0.002 => Not trivial, Not overlay, NW1, N12 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 Huet Levy Processor: 0.002/0.002 -> Rules: 0.002/0.002 incr(cons(X:S,XS:S)) -> cons(s(X:S),incr(XS:S)) 0.002/0.002 oddNs -> incr(pairNs) 0.002/0.002 pairNs -> cons(0,incr(oddNs)) 0.002/0.002 repItems(cons(X:S,XS:S)) -> cons(X:S,cons(X:S,repItems(XS:S))) 0.002/0.002 repItems(nil) -> nil 0.002/0.002 tail(cons(X:S,XS:S)) -> XS:S 0.002/0.002 take(0,XS:S) -> nil 0.002/0.002 take(s(N:S),cons(X:S,XS:S)) -> cons(X:S,take(N:S,XS:S)) 0.002/0.002 zip(cons(X:S,XS:S),cons(Y:S,YS:S)) -> cons(pair(X:S,Y:S),zip(XS:S,YS:S)) 0.002/0.002 zip(nil,XS:S) -> nil 0.002/0.002 zip(X:S,nil) -> nil 0.002/0.002 -> Vars: 0.002/0.002 X, XS, X, XS, X, XS, XS, N, X, XS, X, XS, Y, YS, XS, X 0.002/0.002 -> UVars: 0.002/0.002 (UV-RuleId: 1, UV-LActive: [X], UV-RActive: [X], UV-LFrozen: [XS], UV-RFrozen: [XS]) 0.002/0.002 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 4, UV-LActive: [X], UV-RActive: [X], UV-LFrozen: [XS], UV-RFrozen: [X, XS]) 0.002/0.002 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 6, UV-LActive: [X], UV-RActive: [XS], UV-LFrozen: [XS], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 7, UV-LActive: [XS], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 8, UV-LActive: [N, X], UV-RActive: [X], UV-LFrozen: [XS], UV-RFrozen: [N, XS]) 0.002/0.002 (UV-RuleId: 9, UV-LActive: [X, Y], UV-RActive: [X, Y], UV-LFrozen: [XS, YS], UV-RFrozen: [XS, YS]) 0.002/0.002 (UV-RuleId: 10, UV-LActive: [XS], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 11, UV-LActive: [X], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 -> FVars: 0.002/0.002 x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21 0.002/0.002 -> PVars: 0.002/0.002 X: [x6, x8, x10, x14, x16, x21], XS: [x7, x9, x11, x12, x15, x17, x20], N: [x13], Y: [x18], YS: [x19] 0.002/0.002 0.002/0.002 -> Rlps: 0.002/0.002 (rule: incr(cons(x6:S,x7:S)) -> cons(s(x6:S),incr(x7:S)), id: 1, possubterms: incr(cons(x6:S,x7:S))->[], cons(x6:S,x7:S)->[1]) 0.002/0.002 (rule: oddNs -> incr(pairNs), id: 2, possubterms: oddNs->[]) 0.002/0.002 (rule: pairNs -> cons(0,incr(oddNs)), id: 3, possubterms: pairNs->[]) 0.002/0.002 (rule: repItems(cons(x8:S,x9:S)) -> cons(x8:S,cons(x8:S,repItems(x9:S))), id: 4, possubterms: repItems(cons(x8:S,x9:S))->[], cons(x8:S,x9:S)->[1]) 0.002/0.002 (rule: repItems(nil) -> nil, id: 5, possubterms: repItems(nil)->[], nil->[1]) 0.002/0.002 (rule: tail(cons(x10:S,x11:S)) -> x11:S, id: 6, possubterms: tail(cons(x10:S,x11:S))->[], cons(x10:S,x11:S)->[1]) 0.002/0.002 (rule: take(0,x12:S) -> nil, id: 7, possubterms: take(0,x12:S)->[], 0->[1]) 0.002/0.002 (rule: take(s(x13:S),cons(x14:S,x15:S)) -> cons(x14:S,take(x13:S,x15:S)), id: 8, possubterms: take(s(x13:S),cons(x14:S,x15:S))->[], s(x13:S)->[1], cons(x14:S,x15:S)->[2]) 0.002/0.002 (rule: zip(cons(x16:S,x17:S),cons(x18:S,x19:S)) -> cons(pair(x16:S,x18:S),zip(x17:S,x19:S)), id: 9, possubterms: zip(cons(x16:S,x17:S),cons(x18:S,x19:S))->[], cons(x16:S,x17:S)->[1], cons(x18:S,x19:S)->[2]) 0.002/0.002 (rule: zip(nil,x20:S) -> nil, id: 10, possubterms: zip(nil,x20:S)->[], nil->[1]) 0.002/0.002 (rule: zip(x21:S,nil) -> nil, id: 11, possubterms: zip(x21:S,nil)->[], nil->[2]) 0.002/0.002 0.002/0.002 -> Unifications: 0.002/0.002 (R11 unifies with R10 at p: [], l: zip(x21:S,nil), lp: zip(x21:S,nil), sig: {XS:S -> nil,x21:S -> nil}, l': zip(nil,XS:S), r: nil, r': nil) 0.002/0.002 0.002/0.002 -> Critical pairs info: 0.002/0.002 => Not trivial, Not overlay, NW0, N1 0.002/0.002 => Not trivial, Not overlay, NW1, N2 0.002/0.002 => Not trivial, Not overlay, NW0, N3 0.002/0.002 => Not trivial, Not overlay, NW1, N4 0.002/0.002 => Not trivial, Not overlay, NW0, N5 0.002/0.002 => Not trivial, Not overlay, NW0, N6 0.002/0.002 => Not trivial, Not overlay, NW1, N7 0.002/0.002 => Not trivial, Not overlay, NW1, N8 0.002/0.002 => Not trivial, Not overlay, NW0, N9 0.002/0.002 => Not trivial, Not overlay, NW0, N10 0.002/0.002 => Trivial, Overlay, NW0, N11 0.002/0.002 => Not trivial, Not overlay, NW0, N12 0.002/0.002 => Not trivial, Not overlay, NW0, N13 0.002/0.002 0.002/0.002 -> Problem conclusions: 0.002/0.002 Left linear, Not right linear, Not linear 0.002/0.002 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.002/0.002 Not Huet-Levy confluent, Not Newman confluent 0.002/0.002 R is a CS-TRS, Not left-homogeneous u-replacing variables 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 No Convergence Brute Force Processor: 0.002/0.002 -> Rewritings: 0.002/0.002 s: cons(zip(cons(X:S,XS:S),cons(Y:S,YS:S)),cons(zip(cons(X:S,XS:S),cons(Y:S,YS:S)),repItems(XS:S))) 0.002/0.002 Nodes: [0,1] 0.002/0.002 Edges: [(0,1)] 0.002/0.002 ID: 0 => ('cons(zip(cons(X:S,XS:S),cons(Y:S,YS:S)),cons(zip(cons(X:S,XS:S),cons(Y:S,YS:S)),repItems(XS:S)))', D0) 0.002/0.002 ID: 1 => ('cons(cons(pair(X:S,Y:S),zip(XS:S,YS:S)),cons(zip(cons(X:S,XS:S),cons(Y:S,YS:S)),repItems(XS:S)))', D1, R9, P[1], S{x16:S -> X:S, x17:S -> XS:S, x18:S -> Y:S, x19:S -> YS:S}), NR: 'cons(pair(X:S,Y:S),zip(XS:S,YS:S))' 0.002/0.002 t: repItems(cons(cons(pair(X:S,Y:S),zip(XS:S,YS:S)),XS:S)) 0.002/0.002 Nodes: [0,1] 0.002/0.002 Edges: [(0,1)] 0.002/0.002 ID: 0 => ('repItems(cons(cons(pair(X:S,Y:S),zip(XS:S,YS:S)),XS:S))', D0) 0.002/0.002 ID: 1 => ('cons(cons(pair(X:S,Y:S),zip(XS:S,YS:S)),cons(cons(pair(X:S,Y:S),zip(XS:S,YS:S)),repItems(XS:S)))', D1, R4, P[], S{x8:S -> cons(pair(X:S,Y:S),zip(XS:S,YS:S)), x9:S -> XS:S}), NR: 'cons(cons(pair(X:S,Y:S),zip(XS:S,YS:S)),cons(cons(pair(X:S,Y:S),zip(XS:S,YS:S)),repItems(XS:S)))' 0.002/0.002 cons(zip(cons(X:S,XS:S),cons(Y:S,YS:S)),cons(zip(cons(X:S,XS:S),cons(Y:S,YS:S)),repItems(XS:S))) ->* no union *<- repItems(cons(cons(pair(X:S,Y:S),zip(XS:S,YS:S)),XS:S)) 0.002/0.002 "Not joinable" 0.002/0.002 0.002/0.002 The problem is not joinable. 0.002/0.002 0.01user 0.00system 0:00.02elapsed 63%CPU (0avgtext+0avgdata 11444maxresident)k 0.002/0.002 0inputs+0outputs (0major+1164minor)pagefaults 0swaps