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