YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x y) (REPLACEMENT-MAP (+ 1, 2) (- 1) (fSNonEmpty) ) (RULES +(-(x),-(y)) -> -(+(x,y)) -(+(x,y)) -> +(-(x),-(y)) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: Linearity Procedure: Linear? YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x y) (REPLACEMENT-MAP (+ 1, 2) (- 1) (fSNonEmpty) ) (RULES +(-(x),-(y)) -> -(+(x,y)) -(+(x,y)) -> +(-(x),-(y)) ) Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: +(-(x),-(y)) -> -(+(x,y)) -(+(x,y)) -> +(-(x),-(y)) -> Vars: x, y, x, y -> Rlps: (rule: +(-(x),-(y)) -> -(+(x,y)), id: 1, possubterms: +(-(x),-(y))->[], -(x)->[1], -(y)->[2]) (rule: -(+(x,y)) -> +(-(x),-(y)), id: 2, possubterms: -(+(x,y))->[], +(x,y)->[1]) -> Unifications: (R1 unifies with R2 at p: [1], l: +(-(x),-(y)), lp: -(x), sig: {x -> +(x',y')}, l': -(+(x',y')), r: -(+(x,y)), r': +(-(x'),-(y'))) (R1 unifies with R2 at p: [2], l: +(-(x),-(y)), lp: -(y), sig: {y -> +(x',y')}, l': -(+(x',y')), r: -(+(x,y)), r': +(-(x'),-(y'))) (R2 unifies with R1 at p: [1], l: -(+(x,y)), lp: +(x,y), sig: {x -> -(x'),y -> -(y')}, l': +(-(x'),-(y')), r: +(-(x),-(y)), r': -(+(x',y'))) -> Critical pairs info: <+(-(x),+(-(x'),-(y'))),-(+(x,+(x',y')))> => Not trivial, Not overlay, Proper, NW0, N1 <-(-(+(x',y'))),+(-(-(x')),-(-(y')))> => Not trivial, Not overlay, Proper, NW0, N2 <+(+(-(x'),-(y')),-(y)),-(+(+(x',y'),y))> => Not trivial, Not overlay, Proper, NW0, N3 -> 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 The problem is decomposed in 3 subproblems. Problem 1.1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x y x' y') (REPLACEMENT-MAP (+ 1, 2) (- 1) (fSNonEmpty) ) (RULES +(-(x),-(y)) -> -(+(x,y)) -(+(x,y)) -> +(-(x),-(y)) ) Critical Pairs: <+(-(x),+(-(x'),-(y'))),-(+(x,+(x',y')))> => Not trivial, Not overlay, Proper, NW0, N1 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: +(-(x),+(-(x'),-(y'))) Nodes: [0,1,2] Edges: [(0,1),(1,0),(1,2),(2,1)] ID: 0 => ('+(-(x),+(-(x'),-(y')))', D0) ID: 1 => ('+(-(x),-(+(x',y')))', D1, R1, P[2], S{x6 -> x', x7 -> y'}), NR: '-(+(x',y'))' ID: 2 => ('-(+(x,+(x',y')))', D2, R1, P[], S{x6 -> x, x7 -> +(x',y')}), NR: '-(+(x,+(x',y')))' t: -(+(x,+(x',y'))) Nodes: [0,1,2] Edges: [(0,1),(1,0),(1,2),(2,1)] ID: 0 => ('-(+(x,+(x',y')))', D0) ID: 1 => ('+(-(x),-(+(x',y')))', D1, R2, P[], S{x8 -> x, x9 -> +(x',y')}), NR: '+(-(x),-(+(x',y')))' ID: 2 => ('+(-(x),+(-(x'),-(y')))', D2, R2, P[2], S{x8 -> x', x9 -> y'}), NR: '+(-(x'),-(y'))' SNodesPath1: +(-(x),+(-(x'),-(y'))) TNodesPath1: -(+(x,+(x',y'))) -> +(-(x),-(+(x',y'))) -> +(-(x),+(-(x'),-(y'))) SNodesPath2: +(-(x),+(-(x'),-(y'))) -> +(-(x),-(+(x',y'))) -> -(+(x,+(x',y'))) TNodesPath2: -(+(x,+(x',y'))) +(-(x),+(-(x'),-(y'))) ->= +(-(x),+(-(x'),-(y'))) *<- -(+(x,+(x',y'))) -(+(x,+(x',y'))) ->= -(+(x,+(x',y'))) *<- +(-(x),+(-(x'),-(y'))) "Strongly closed critical pair" The problem is confluent. Problem 1.2: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x y x' y') (REPLACEMENT-MAP (+ 1, 2) (- 1) (fSNonEmpty) ) (RULES +(-(x),-(y)) -> -(+(x,y)) -(+(x,y)) -> +(-(x),-(y)) ) Critical Pairs: <-(-(+(x',y'))),+(-(-(x')),-(-(y')))> => Not trivial, Not overlay, Proper, NW0, N2 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: -(-(+(x',y'))) Nodes: [0,1,2] Edges: [(0,1),(1,0),(1,2),(2,1)] ID: 0 => ('-(-(+(x',y')))', D0) ID: 1 => ('-(+(-(x'),-(y')))', D1, R2, P[1], S{x8 -> x', x9 -> y'}), NR: '+(-(x'),-(y'))' ID: 2 => ('+(-(-(x')),-(-(y')))', D2, R2, P[], S{x8 -> -(x'), x9 -> -(y')}), NR: '+(-(-(x')),-(-(y')))' t: +(-(-(x')),-(-(y'))) Nodes: [0,1,2] Edges: [(0,1),(1,0),(1,2),(2,1)] ID: 0 => ('+(-(-(x')),-(-(y')))', D0) ID: 1 => ('-(+(-(x'),-(y')))', D1, R1, P[], S{x6 -> -(x'), x7 -> -(y')}), NR: '-(+(-(x'),-(y')))' ID: 2 => ('-(-(+(x',y')))', D2, R1, P[1], S{x6 -> x', x7 -> y'}), NR: '-(+(x',y'))' SNodesPath1: -(-(+(x',y'))) TNodesPath1: +(-(-(x')),-(-(y'))) -> -(+(-(x'),-(y'))) -> -(-(+(x',y'))) SNodesPath2: -(-(+(x',y'))) -> -(+(-(x'),-(y'))) -> +(-(-(x')),-(-(y'))) TNodesPath2: +(-(-(x')),-(-(y'))) -(-(+(x',y'))) ->= -(-(+(x',y'))) *<- +(-(-(x')),-(-(y'))) +(-(-(x')),-(-(y'))) ->= +(-(-(x')),-(-(y'))) *<- -(-(+(x',y'))) "Strongly closed critical pair" The problem is confluent. Problem 1.3: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x y x' y') (REPLACEMENT-MAP (+ 1, 2) (- 1) (fSNonEmpty) ) (RULES +(-(x),-(y)) -> -(+(x,y)) -(+(x,y)) -> +(-(x),-(y)) ) Critical Pairs: <+(+(-(x'),-(y')),-(y)),-(+(+(x',y'),y))> => Not trivial, Not overlay, Proper, NW0, N3 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: +(+(-(x'),-(y')),-(y)) Nodes: [0,1,2] Edges: [(0,1),(1,0),(1,2),(2,1)] ID: 0 => ('+(+(-(x'),-(y')),-(y))', D0) ID: 1 => ('+(-(+(x',y')),-(y))', D1, R1, P[1], S{x6 -> x', x7 -> y'}), NR: '-(+(x',y'))' ID: 2 => ('-(+(+(x',y'),y))', D2, R1, P[], S{x6 -> +(x',y'), x7 -> y}), NR: '-(+(+(x',y'),y))' t: -(+(+(x',y'),y)) Nodes: [0,1,2] Edges: [(0,1),(1,0),(1,2),(2,1)] ID: 0 => ('-(+(+(x',y'),y))', D0) ID: 1 => ('+(-(+(x',y')),-(y))', D1, R2, P[], S{x8 -> +(x',y'), x9 -> y}), NR: '+(-(+(x',y')),-(y))' ID: 2 => ('+(+(-(x'),-(y')),-(y))', D2, R2, P[1], S{x8 -> x', x9 -> y'}), NR: '+(-(x'),-(y'))' SNodesPath1: +(+(-(x'),-(y')),-(y)) TNodesPath1: -(+(+(x',y'),y)) -> +(-(+(x',y')),-(y)) -> +(+(-(x'),-(y')),-(y)) SNodesPath2: +(+(-(x'),-(y')),-(y)) -> +(-(+(x',y')),-(y)) -> -(+(+(x',y'),y)) TNodesPath2: -(+(+(x',y'),y)) +(+(-(x'),-(y')),-(y)) ->= +(+(-(x'),-(y')),-(y)) *<- -(+(+(x',y'),y)) -(+(+(x',y'),y)) ->= -(+(+(x',y'),y)) *<- +(+(-(x'),-(y')),-(y)) "Strongly closed critical pair" The problem is confluent.