NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (0 1) (p 1) (sq 1) (twice 1) (fSNonEmpty) (s 1) ) (RULES 0(x) -> x p(0(x)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x)))))))))))) p(p(s(x))) -> p(x) p(s(x)) -> x sq(0(x)) -> p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x))))))))))))))))) sq(s(x)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x))))))))))))))))))))))))))))))))) twice(0(x)) -> p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x))))))))))))))))))))))))))) twice(s(x)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x))))))))))))))) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (0 1) (p 1) (sq 1) (twice 1) (fSNonEmpty) (s 1) ) (RULES 0(x) -> x p(0(x)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x)))))))))))) p(p(s(x))) -> p(x) p(s(x)) -> x sq(0(x)) -> p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x))))))))))))))))) sq(s(x)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x))))))))))))))))))))))))))))))))) twice(0(x)) -> p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x))))))))))))))))))))))))))) twice(s(x)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x))))))))))))))) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: 0(x) -> x p(0(x)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x)))))))))))) p(p(s(x))) -> p(x) p(s(x)) -> x sq(0(x)) -> p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x))))))))))))))))) sq(s(x)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x))))))))))))))))))))))))))))))))) twice(0(x)) -> p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x))))))))))))))))))))))))))) twice(s(x)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x))))))))))))))) -> Vars: x, x, x, x, x, x, x, x -> Rlps: (rule: 0(x) -> x, id: 1, possubterms: 0(x)->[]) (rule: p(0(x)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x)))))))))))), id: 2, possubterms: p(0(x))->[], 0(x)->[1]) (rule: p(p(s(x))) -> p(x), id: 3, possubterms: p(p(s(x)))->[], p(s(x))->[1], s(x)->[1, 1]) (rule: p(s(x)) -> x, id: 4, possubterms: p(s(x))->[], s(x)->[1]) (rule: sq(0(x)) -> p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x))))))))))))))))), id: 5, possubterms: sq(0(x))->[], 0(x)->[1]) (rule: sq(s(x)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x))))))))))))))))))))))))))))))))), id: 6, possubterms: sq(s(x))->[], s(x)->[1]) (rule: twice(0(x)) -> p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x))))))))))))))))))))))))))), id: 7, possubterms: twice(0(x))->[], 0(x)->[1]) (rule: twice(s(x)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x))))))))))))))), id: 8, possubterms: twice(s(x))->[], s(x)->[1]) -> Unifications: (R2 unifies with R1 at p: [1], l: p(0(x)), lp: 0(x), sig: {x -> x'}, l': 0(x'), r: 0(s(s(s(s(s(s(s(s(s(s(s(x)))))))))))), r': x') (R3 unifies with R4 at p: [1], l: p(p(s(x))), lp: p(s(x)), sig: {x -> x'}, l': p(s(x')), r: p(x), r': x') (R5 unifies with R1 at p: [1], l: sq(0(x)), lp: 0(x), sig: {x -> x'}, l': 0(x'), r: p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x))))))))))))))))), r': x') (R7 unifies with R1 at p: [1], l: twice(0(x)), lp: 0(x), sig: {x -> x'}, l': 0(x'), r: p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x))))))))))))))))))))))))))), r': x') -> Critical pairs info: => Not trivial, Not overlay, Proper, NW0, N1 => Not trivial, Not overlay, Proper, NW0, N2 => Trivial, Not overlay, Proper, NW0, N3 => Not trivial, Not overlay, Proper, NW0, N4 -> Problem conclusions: Left linear, Right linear, Linear Not weakly orthogonal, Not almost orthogonal, Not orthogonal Not Huet-Levy confluent, Not Newman confluent R is a TRS Problem 1: No Convergence Brute Force Procedure: -> Rewritings: s: p(x') Nodes: [0] Edges: [] ID: 0 => ('p(x')', D0) t: 0(s(s(s(s(s(s(s(s(s(s(s(x')))))))))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('0(s(s(s(s(s(s(s(s(s(s(s(x'))))))))))))', D0) ID: 1 => ('s(s(s(s(s(s(s(s(s(s(s(x')))))))))))', D1, R1, P[], S{x4 -> s(s(s(s(s(s(s(s(s(s(s(x')))))))))))}), NR: 's(s(s(s(s(s(s(s(s(s(s(x')))))))))))' p(x') ->* no union *<- 0(s(s(s(s(s(s(s(s(s(s(s(x')))))))))))) "Not joinable" The problem is not confluent.