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