NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x y z) (REPLACEMENT-MAP (* 1, 2) (+ 1, 2) (fSNonEmpty) ) (RULES *(*(x,y),z) -> *(x,*(y,z)) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(x,y) -> *(y,x) +(+(x,y),z) -> +(x,+(y,z)) +(x,y) -> +(y,x) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x y z) (REPLACEMENT-MAP (* 1, 2) (+ 1, 2) (fSNonEmpty) ) (RULES *(*(x,y),z) -> *(x,*(y,z)) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(x,y) -> *(y,x) +(+(x,y),z) -> +(x,+(y,z)) +(x,y) -> +(y,x) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Ordered by Num of Vars and Symbs Procedure: -> Rules: *(*(x,y),z) -> *(x,*(y,z)) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(x,y) -> *(y,x) +(+(x,y),z) -> +(x,+(y,z)) +(x,y) -> +(y,x) -> Vars: x, y, z, x, y, z, x, y, z, x, y, x, y, z, x, y -> Rlps: (rule: *(*(x,y),z) -> *(x,*(y,z)), id: 1, possubterms: *(*(x,y),z)->[], *(x,y)->[1]) (rule: *(+(x,y),z) -> +(*(x,z),*(y,z)), id: 2, possubterms: *(+(x,y),z)->[], +(x,y)->[1]) (rule: *(x,+(y,z)) -> +(*(x,y),*(x,z)), id: 3, possubterms: *(x,+(y,z))->[], +(y,z)->[2]) (rule: *(x,y) -> *(y,x), id: 4, possubterms: *(x,y)->[]) (rule: +(+(x,y),z) -> +(x,+(y,z)), id: 5, possubterms: +(+(x,y),z)->[], +(x,y)->[1]) (rule: +(x,y) -> +(y,x), id: 6, possubterms: +(x,y)->[]) -> 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',z'),*(y',z'))) (R1 unifies with R3 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'),*(x',z'))) (R1 unifies with R4 at p: [1], l: *(*(x,y),z), lp: *(x,y), sig: {x -> x',y -> y'}, l': *(x',y'), r: *(x,*(y,z)), r': *(y',x')) (R2 unifies with R5 at p: [1], l: *(+(x,y),z), lp: +(x,y), sig: {x -> +(x',y'),y -> z'}, l': +(+(x',y'),z'), r: +(*(x,z),*(y,z)), r': +(x',+(y',z'))) (R2 unifies with R6 at p: [1], l: *(+(x,y),z), lp: +(x,y), sig: {x -> x',y -> y'}, l': +(x',y'), r: +(*(x,z),*(y,z)), r': +(y',x')) (R3 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),*(x,z)), r': *(x',*(y',z'))) (R3 unifies with R2 at p: [], l: *(x,+(y,z)), lp: *(x,+(y,z)), sig: {x -> +(x',y'),z' -> +(y,z)}, l': *(+(x',y'),z'), r: +(*(x,y),*(x,z)), r': +(*(x',z'),*(y',z'))) (R3 unifies with R5 at p: [2], l: *(x,+(y,z)), lp: +(y,z), sig: {y -> +(x',y'),z -> z'}, l': +(+(x',y'),z'), r: +(*(x,y),*(x,z)), r': +(x',+(y',z'))) (R3 unifies with R6 at p: [2], l: *(x,+(y,z)), lp: +(y,z), sig: {y -> x',z -> y'}, l': +(x',y'), r: +(*(x,y),*(x,z)), r': +(y',x')) (R4 unifies with R1 at p: [], l: *(x,y), lp: *(x,y), sig: {x -> *(x',y'),y -> z}, l': *(*(x',y'),z), r: *(y,x), r': *(x',*(y',z))) (R4 unifies with R2 at p: [], l: *(x,y), lp: *(x,y), sig: {x -> +(x',y'),y -> z}, l': *(+(x',y'),z), r: *(y,x), r': +(*(x',z),*(y',z))) (R4 unifies with R3 at p: [], l: *(x,y), lp: *(x,y), sig: {x -> x',y -> +(y',z)}, l': *(x',+(y',z)), r: *(y,x), r': +(*(x',y'),*(x',z))) (R5 unifies with R5 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'))) (R5 unifies with R6 at p: [1], l: +(+(x,y),z), lp: +(x,y), sig: {x -> x',y -> y'}, l': +(x',y'), r: +(x,+(y,z)), r': +(y',x')) (R6 unifies with R5 at p: [], l: +(x,y), lp: +(x,y), sig: {x -> +(x',y'),y -> z}, l': +(+(x',y'),z), r: +(y,x), r': +(x',+(y',z))) -> Critical pairs info: <*(x',*(y',z)),*(z,*(x',y'))> => Not trivial, Overlay, Proper, NW0, N1 <+(+(y',x'),z),+(x',+(y',z))> => Not trivial, Not overlay, Proper, NW0, N2 <*(*(y',x'),z),*(x',*(y',z))> => Not trivial, Not overlay, Proper, NW0, N3 <+(x',+(y',z)),+(z,+(x',y'))> => Not trivial, Overlay, Proper, NW0, N4 <+(*(x',z),*(y',z)),*(z,+(x',y'))> => Not trivial, Overlay, Proper, NW0, N5 <+(*(x',y'),*(x',z)),*(+(y',z),x')> => Not trivial, Overlay, Proper, NW0, N6 <+(+(x',+(y',z')),z),+(+(x',y'),+(z',z))> => Not trivial, Not overlay, Proper, NW0, N7 <*(+(y',x'),z),+(*(x',z),*(y',z))> => Not trivial, Not overlay, Proper, NW0, N8 <*(x,+(y',x')),+(*(x,x'),*(x,y'))> => Not trivial, Not overlay, Proper, NW0, N9 <*(*(x',*(y',z')),z),*(*(x',y'),*(z',z))> => Not trivial, Not overlay, Proper, NW0, N10 <*(x,+(x',+(y',z'))),+(*(x,+(x',y')),*(x,z'))> => Not trivial, Not overlay, Proper, NW0, N11 <*(+(*(x',y'),*(x',z')),z),*(x',*(+(y',z'),z))> => Not trivial, Not overlay, Proper, NW0, N12 <*(+(x',+(y',z')),z),+(*(+(x',y'),z),*(z',z))> => Not trivial, Not overlay, Proper, NW0, N13 <+(*(x',+(y,z)),*(y',+(y,z))),+(*(+(x',y'),y),*(+(x',y'),z))> => Not trivial, Overlay, Proper, NW0, N14 <*(x',*(y',+(y,z))),+(*(*(x',y'),y),*(*(x',y'),z))> => Not trivial, Overlay, Proper, NW0, N15 <*(+(*(x',z'),*(y',z')),z),*(+(x',y'),*(z',z))> => Not trivial, Not overlay, Proper, NW0, N16 -> Problem conclusions: Left linear, Not right linear, Not linear Not weakly orthogonal, Not almost orthogonal, Not orthogonal Not Huet-Levy confluent, Not Newman confluent R is a TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x y z x' y' z) (REPLACEMENT-MAP (* 1, 2) (+ 1, 2) (fSNonEmpty) ) (RULES *(*(x,y),z) -> *(x,*(y,z)) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(x,y) -> *(y,x) +(+(x,y),z) -> +(x,+(y,z)) +(x,y) -> +(y,x) ) Critical Pairs: <+(*(x',+(y,z)),*(y',+(y,z))),+(*(+(x',y'),y),*(+(x',y'),z))> => Not trivial, Overlay, Proper, NW0, N14 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: No Convergence InfChecker Procedure: Infeasible convergence? YES Problem 1: Infeasibility Problem: [(VAR vNonEmpty x y z x1 y1 vNonEmpty z0) (STRATEGY CONTEXTSENSITIVE (+ 1 2) (* 1 2) (c_x1) (c_y) (c_y1) (c_z) (fSNonEmpty) ) (RULES +(+(x,y),z) -> +(x,+(y,z)) +(x,y) -> +(y,x) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(*(x,y),z) -> *(x,*(y,z)) *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(x,y) -> *(y,x) )] Infeasibility Conditions: +(*(c_x1,+(c_y,c_z)),*(c_y1,+(c_y,c_z))) ->* z0, +(*(+(c_x1,c_y1),c_y),*(+(c_x1,c_y1),c_z)) ->* z0 Problem 1: Obtaining a model using AGES: -> Theory (Usable Rules): +(+(x,y),z) -> +(x,+(y,z)) +(x,y) -> +(y,x) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(*(x,y),z) -> *(x,*(y,z)) *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(x,y) -> *(y,x) -> AGES Output: The problem is infeasible. The problem is not confluent.