NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x y z) (REPLACEMENT-MAP (+ 1, 2) (dbl 1) (0) (fSNonEmpty) (s 1) ) (RULES +(+(x,y),z) -> +(x,+(y,z)) +(0,y) -> y +(s(x),y) -> s(+(x,y)) +(x,0) -> x +(x,s(y)) -> s(+(x,y)) +(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 +(+(x,y),z) -> +(x,+(y,z)) +(0,y) -> y +(s(x),y) -> s(+(x,y)) +(x,0) -> x +(x,s(y)) -> s(+(x,y)) +(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: +(+(x,y),z) -> +(x,+(y,z)) +(0,y) -> y +(s(x),y) -> s(+(x,y)) +(x,0) -> x +(x,s(y)) -> s(+(x,y)) +(x,y) -> +(y,x) dbl(+(x,y)) -> +(dbl(x),dbl(y)) dbl(x) -> +(x,x) -> Vars: x, y, z, y, x, y, x, x, y, x, y, x, y, x -> Rlps: (rule: +(+(x,y),z) -> +(x,+(y,z)), id: 1, possubterms: +(+(x,y),z)->[], +(x,y)->[1]) (rule: +(0,y) -> y, id: 2, possubterms: +(0,y)->[], 0->[1]) (rule: +(s(x),y) -> s(+(x,y)), id: 3, possubterms: +(s(x),y)->[], s(x)->[1]) (rule: +(x,0) -> x, id: 4, possubterms: +(x,0)->[], 0->[2]) (rule: +(x,s(y)) -> s(+(x,y)), 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: (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 -> 0,y -> y'}, l': +(0,y'), r: +(x,+(y,z)), r': y') (R1 unifies with R3 at p: [1], l: +(+(x,y),z), lp: +(x,y), sig: {x -> s(x'),y -> y'}, l': +(s(x'),y'), r: +(x,+(y,z)), r': s(+(x',y'))) (R1 unifies with R4 at p: [1], l: +(+(x,y),z), lp: +(x,y), sig: {x -> x',y -> 0}, l': +(x',0), r: +(x,+(y,z)), r': x') (R1 unifies with R5 at p: [1], l: +(+(x,y),z), lp: +(x,y), sig: {x -> x',y -> s(y')}, l': +(x',s(y')), r: +(x,+(y,z)), r': s(+(x',y'))) (R1 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')) (R4 unifies with R1 at p: [], l: +(x,0), lp: +(x,0), sig: {x -> +(x',y),z -> 0}, l': +(+(x',y),z), r: x, r': +(x',+(y,z))) (R4 unifies with R2 at p: [], l: +(x,0), lp: +(x,0), sig: {x -> 0,y -> 0}, l': +(0,y), r: x, r': y) (R4 unifies with R3 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 -> +(x',y'),z -> s(y)}, l': +(+(x',y'),z), r: s(+(x,y)), r': +(x',+(y',z))) (R5 unifies with R2 at p: [], l: +(x,s(y)), lp: +(x,s(y)), sig: {x -> 0,y' -> s(y)}, l': +(0,y'), r: s(+(x,y)), r': y') (R5 unifies with R3 at p: [], l: +(x,s(y)), lp: +(x,s(y)), sig: {x -> s(x'),y' -> s(y)}, l': +(s(x'),y'), r: s(+(x,y)), r': s(+(x',y'))) (R6 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))) (R6 unifies with R2 at p: [], l: +(x,y), lp: +(x,y), sig: {x -> 0,y -> y'}, l': +(0,y'), r: +(y,x), r': y') (R6 unifies with R3 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 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(+(x',y'))) (R7 unifies with R1 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 R2 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 R3 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 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(+(x',y'))) (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, Not overlay, Proper, NW0, N5 => Not trivial, Not overlay, Proper, NW0, N6 => Not trivial, Overlay, Proper, NW0, N7 <+(x',+(y,0)),+(x',y)> => Not trivial, Overlay, Proper, NW0, N8 <+(y',z),+(0,+(y',z))> => Not trivial, Not overlay, Proper, NW0, N9 <+(x',z),+(x',+(0,z))> => Not trivial, Not overlay, Proper, NW0, N10 <+(dbl(x'),dbl(y)),+(+(x',y),+(x',y))> => Not trivial, Overlay, Proper, NW0, N11 => Not trivial, Not overlay, Proper, NW0, N12 <+(x',+(y',z)),+(z,+(x',y'))> => Not trivial, Overlay, Proper, NW0, N13 => Not trivial, Overlay, Proper, NW0, N14 => Not trivial, Overlay, Proper, NW0, N15 <+(+(y',x'),z),+(x',+(y',z))> => Not trivial, Not overlay, Proper, NW0, N16 => Not trivial, Overlay, Proper, NW0, N17 <+(x',+(y',s(y))),s(+(+(x',y'),y))> => Not trivial, Overlay, Proper, NW0, N18 => Not trivial, Not overlay, Proper, NW0, N19 => Not trivial, Not overlay, Proper, NW0, N20 <+(s(+(x',y')),z),+(s(x'),+(y',z))> => Not trivial, Not overlay, Proper, NW0, N21 <+(s(+(x',y')),z),+(x',+(s(y'),z))> => Not trivial, Not overlay, Proper, NW0, N22 => Not trivial, Not overlay, Proper, NW0, N23 <+(+(x',+(y',z')),z),+(+(x',y'),+(z',z))> => 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 +(+(x,y),z) -> +(x,+(y,z)) +(0,y) -> y +(s(x),y) -> s(+(x,y)) +(x,0) -> x +(x,s(y)) -> s(+(x,y)) +(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 +(+(x,y),z) -> +(x,+(y,z)) +(0,y) -> y +(s(x),y) -> s(+(x,y)) +(x,0) -> x +(x,s(y)) -> s(+(x,y)) +(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(c_x1),dbl(s(c_y1))) ->* z0 Problem 1: Obtaining a model using AGES: -> Theory (Usable Rules): +(+(x,y),z) -> +(x,+(y,z)) +(0,y) -> y +(s(x),y) -> s(+(x,y)) +(x,0) -> x +(x,s(y)) -> s(+(x,y)) +(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.