NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x y) (REPLACEMENT-MAP (inv 1) (minus 1, 2) (p 1) (s 1) (0) (fSNonEmpty) ) (RULES inv(p(x)) -> s(inv(x)) inv(s(x)) -> p(inv(x)) inv(0) -> 0 inv(x) -> minus(0,x) minus(p(x),p(y)) -> minus(x,y) minus(s(x),s(y)) -> minus(x,y) minus(0,x) -> inv(x) minus(x,p(y)) -> s(minus(x,y)) minus(x,s(y)) -> p(minus(x,y)) minus(x,0) -> x p(s(x)) -> x s(p(x)) -> x ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x y) (REPLACEMENT-MAP (inv 1) (minus 1, 2) (p 1) (s 1) (0) (fSNonEmpty) ) (RULES inv(p(x)) -> s(inv(x)) inv(s(x)) -> p(inv(x)) inv(0) -> 0 inv(x) -> minus(0,x) minus(p(x),p(y)) -> minus(x,y) minus(s(x),s(y)) -> minus(x,y) minus(0,x) -> inv(x) minus(x,p(y)) -> s(minus(x,y)) minus(x,s(y)) -> p(minus(x,y)) minus(x,0) -> x p(s(x)) -> x s(p(x)) -> x ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: inv(p(x)) -> s(inv(x)) inv(s(x)) -> p(inv(x)) inv(0) -> 0 inv(x) -> minus(0,x) minus(p(x),p(y)) -> minus(x,y) minus(s(x),s(y)) -> minus(x,y) minus(0,x) -> inv(x) minus(x,p(y)) -> s(minus(x,y)) minus(x,s(y)) -> p(minus(x,y)) minus(x,0) -> x p(s(x)) -> x s(p(x)) -> x -> Vars: x, x, x, x, y, x, y, x, x, y, x, y, x, x, x -> Rlps: (rule: inv(p(x)) -> s(inv(x)), id: 1, possubterms: inv(p(x))->[], p(x)->[1]) (rule: inv(s(x)) -> p(inv(x)), id: 2, possubterms: inv(s(x))->[], s(x)->[1]) (rule: inv(0) -> 0, id: 3, possubterms: inv(0)->[], 0->[1]) (rule: inv(x) -> minus(0,x), id: 4, possubterms: inv(x)->[]) (rule: minus(p(x),p(y)) -> minus(x,y), id: 5, possubterms: minus(p(x),p(y))->[], p(x)->[1], p(y)->[2]) (rule: minus(s(x),s(y)) -> minus(x,y), id: 6, possubterms: minus(s(x),s(y))->[], s(x)->[1], s(y)->[2]) (rule: minus(0,x) -> inv(x), id: 7, possubterms: minus(0,x)->[], 0->[1]) (rule: minus(x,p(y)) -> s(minus(x,y)), id: 8, possubterms: minus(x,p(y))->[], p(y)->[2]) (rule: minus(x,s(y)) -> p(minus(x,y)), id: 9, possubterms: minus(x,s(y))->[], s(y)->[2]) (rule: minus(x,0) -> x, id: 10, possubterms: minus(x,0)->[], 0->[2]) (rule: p(s(x)) -> x, id: 11, possubterms: p(s(x))->[], s(x)->[1]) (rule: s(p(x)) -> x, id: 12, possubterms: s(p(x))->[], p(x)->[1]) -> Unifications: (R1 unifies with R11 at p: [1], l: inv(p(x)), lp: p(x), sig: {x -> s(x')}, l': p(s(x')), r: s(inv(x)), r': x') (R2 unifies with R12 at p: [1], l: inv(s(x)), lp: s(x), sig: {x -> p(x')}, l': s(p(x')), r: p(inv(x)), r': x') (R4 unifies with R1 at p: [], l: inv(x), lp: inv(x), sig: {x -> p(x')}, l': inv(p(x')), r: minus(0,x), r': s(inv(x'))) (R4 unifies with R2 at p: [], l: inv(x), lp: inv(x), sig: {x -> s(x')}, l': inv(s(x')), r: minus(0,x), r': p(inv(x'))) (R4 unifies with R3 at p: [], l: inv(x), lp: inv(x), sig: {x -> 0}, l': inv(0), r: minus(0,x), r': 0) (R5 unifies with R11 at p: [1], l: minus(p(x),p(y)), lp: p(x), sig: {x -> s(x')}, l': p(s(x')), r: minus(x,y), r': x') (R5 unifies with R11 at p: [2], l: minus(p(x),p(y)), lp: p(y), sig: {y -> s(x')}, l': p(s(x')), r: minus(x,y), r': x') (R6 unifies with R12 at p: [1], l: minus(s(x),s(y)), lp: s(x), sig: {x -> p(x')}, l': s(p(x')), r: minus(x,y), r': x') (R6 unifies with R12 at p: [2], l: minus(s(x),s(y)), lp: s(y), sig: {y -> p(x')}, l': s(p(x')), r: minus(x,y), r': x') (R8 unifies with R5 at p: [], l: minus(x,p(y)), lp: minus(x,p(y)), sig: {x -> p(x'),y -> y'}, l': minus(p(x'),p(y')), r: s(minus(x,y)), r': minus(x',y')) (R8 unifies with R7 at p: [], l: minus(x,p(y)), lp: minus(x,p(y)), sig: {x -> 0,x' -> p(y)}, l': minus(0,x'), r: s(minus(x,y)), r': inv(x')) (R8 unifies with R11 at p: [2], l: minus(x,p(y)), lp: p(y), sig: {y -> s(x')}, l': p(s(x')), r: s(minus(x,y)), r': x') (R9 unifies with R6 at p: [], l: minus(x,s(y)), lp: minus(x,s(y)), sig: {x -> s(x'),y -> y'}, l': minus(s(x'),s(y')), r: p(minus(x,y)), r': minus(x',y')) (R9 unifies with R7 at p: [], l: minus(x,s(y)), lp: minus(x,s(y)), sig: {x -> 0,x' -> s(y)}, l': minus(0,x'), r: p(minus(x,y)), r': inv(x')) (R9 unifies with R12 at p: [2], l: minus(x,s(y)), lp: s(y), sig: {y -> p(x')}, l': s(p(x')), r: p(minus(x,y)), r': x') (R10 unifies with R7 at p: [], l: minus(x,0), lp: minus(x,0), sig: {x -> 0,x' -> 0}, l': minus(0,x'), r: x, r': inv(x')) (R11 unifies with R12 at p: [1], l: p(s(x)), lp: s(x), sig: {x -> p(x')}, l': s(p(x')), r: x, r': x') (R12 unifies with R11 at p: [1], l: s(p(x)), lp: p(x), sig: {x -> s(x')}, l': p(s(x')), r: x, r': x') -> Critical pairs info: => Not trivial, Overlay, Proper, NW0, N1 => Not trivial, Not overlay, Proper, NW0, N2 => Trivial, Not overlay, Proper, NW0, N3 => Not trivial, Not overlay, Proper, NW0, N4 => Not trivial, Not overlay, Proper, NW0, N5 => Not trivial, Overlay, Proper, NW0, N6 => Not trivial, Not overlay, Proper, NW0, N7 => Not trivial, Overlay, Proper, NW0, N8 => Not trivial, Not overlay, Proper, NW0, N9 => Not trivial, Overlay, Proper, NW0, N10 <0,minus(0,0)> => Not trivial, Overlay, Proper, NW0, N11 => Not trivial, Not overlay, Proper, NW0, N12 => Not trivial, Overlay, Proper, NW0, N13 => Not trivial, Not overlay, Proper, NW0, N14 => Not trivial, Not overlay, Proper, NW0, N15 => Trivial, Not overlay, Proper, NW0, N16 => Not trivial, Overlay, Proper, NW0, N17 => Not trivial, Overlay, Proper, NW0, N18 -> 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: minus(s(x),x') Nodes: [0] Edges: [] ID: 0 => ('minus(s(x),x')', D0) t: minus(x,p(x')) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('minus(x,p(x'))', D0) ID: 1 => ('s(minus(x,x'))', D1, R8, P[], S{x14 -> x, x15 -> x'}), NR: 's(minus(x,x'))' minus(s(x),x') ->* no union *<- minus(x,p(x')) "Not joinable" The problem is not confluent.