NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x y) (REPLACEMENT-MAP (m 1) (plus 1, 2) (times 1, 2) (0) (1) (fSNonEmpty) ) (RULES m(m(x)) -> x m(0) -> 0 plus(m(plus(x,1)),1) -> m(x) plus(m(1),1) -> 0 plus(0,1) -> 1 plus(x,m(y)) -> m(plus(m(x),y)) plus(x,plus(y,1)) -> plus(plus(x,y),1) plus(x,0) -> x times(x,m(y)) -> m(times(x,y)) times(x,plus(y,1)) -> plus(times(x,y),x) times(x,0) -> 0 times(x,1) -> x ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x y) (REPLACEMENT-MAP (m 1) (plus 1, 2) (times 1, 2) (0) (1) (fSNonEmpty) ) (RULES m(m(x)) -> x m(0) -> 0 plus(m(plus(x,1)),1) -> m(x) plus(m(1),1) -> 0 plus(0,1) -> 1 plus(x,m(y)) -> m(plus(m(x),y)) plus(x,plus(y,1)) -> plus(plus(x,y),1) plus(x,0) -> x times(x,m(y)) -> m(times(x,y)) times(x,plus(y,1)) -> plus(times(x,y),x) times(x,0) -> 0 times(x,1) -> x ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: m(m(x)) -> x m(0) -> 0 plus(m(plus(x,1)),1) -> m(x) plus(m(1),1) -> 0 plus(0,1) -> 1 plus(x,m(y)) -> m(plus(m(x),y)) plus(x,plus(y,1)) -> plus(plus(x,y),1) plus(x,0) -> x times(x,m(y)) -> m(times(x,y)) times(x,plus(y,1)) -> plus(times(x,y),x) times(x,0) -> 0 times(x,1) -> x -> Vars: x, x, x, y, x, y, x, x, y, x, y, x, x -> Rlps: (rule: m(m(x)) -> x, id: 1, possubterms: m(m(x))->[], m(x)->[1]) (rule: m(0) -> 0, id: 2, possubterms: m(0)->[], 0->[1]) (rule: plus(m(plus(x,1)),1) -> m(x), id: 3, possubterms: plus(m(plus(x,1)),1)->[], m(plus(x,1))->[1], plus(x,1)->[1, 1], 1->[1, 1, 2], 1->[2]) (rule: plus(m(1),1) -> 0, id: 4, possubterms: plus(m(1),1)->[], m(1)->[1], 1->[1, 1], 1->[2]) (rule: plus(0,1) -> 1, id: 5, possubterms: plus(0,1)->[], 0->[1], 1->[2]) (rule: plus(x,m(y)) -> m(plus(m(x),y)), id: 6, possubterms: plus(x,m(y))->[], m(y)->[2]) (rule: plus(x,plus(y,1)) -> plus(plus(x,y),1), id: 7, possubterms: plus(x,plus(y,1))->[], plus(y,1)->[2], 1->[2, 2]) (rule: plus(x,0) -> x, id: 8, possubterms: plus(x,0)->[], 0->[2]) (rule: times(x,m(y)) -> m(times(x,y)), id: 9, possubterms: times(x,m(y))->[], m(y)->[2]) (rule: times(x,plus(y,1)) -> plus(times(x,y),x), id: 10, possubterms: times(x,plus(y,1))->[], plus(y,1)->[2], 1->[2, 2]) (rule: times(x,0) -> 0, id: 11, possubterms: times(x,0)->[], 0->[2]) (rule: times(x,1) -> x, id: 12, possubterms: times(x,1)->[], 1->[2]) -> Unifications: (R1 unifies with R1 at p: [1], l: m(m(x)), lp: m(x), sig: {x -> m(x')}, l': m(m(x')), r: x, r': x') (R1 unifies with R2 at p: [1], l: m(m(x)), lp: m(x), sig: {x -> 0}, l': m(0), r: x, r': 0) (R3 unifies with R3 at p: [1,1], l: plus(m(plus(x,1)),1), lp: plus(x,1), sig: {x -> m(plus(x',1))}, l': plus(m(plus(x',1)),1), r: m(x), r': m(x')) (R3 unifies with R4 at p: [1,1], l: plus(m(plus(x,1)),1), lp: plus(x,1), sig: {x -> m(1)}, l': plus(m(1),1), r: m(x), r': 0) (R3 unifies with R5 at p: [1,1], l: plus(m(plus(x,1)),1), lp: plus(x,1), sig: {x -> 0}, l': plus(0,1), r: m(x), r': 1) (R6 unifies with R1 at p: [2], l: plus(x,m(y)), lp: m(y), sig: {y -> m(x')}, l': m(m(x')), r: m(plus(m(x),y)), r': x') (R6 unifies with R2 at p: [2], l: plus(x,m(y)), lp: m(y), sig: {y -> 0}, l': m(0), r: m(plus(m(x),y)), r': 0) (R7 unifies with R3 at p: [2], l: plus(x,plus(y,1)), lp: plus(y,1), sig: {y -> m(plus(x',1))}, l': plus(m(plus(x',1)),1), r: plus(plus(x,y),1), r': m(x')) (R7 unifies with R4 at p: [2], l: plus(x,plus(y,1)), lp: plus(y,1), sig: {y -> m(1)}, l': plus(m(1),1), r: plus(plus(x,y),1), r': 0) (R7 unifies with R5 at p: [2], l: plus(x,plus(y,1)), lp: plus(y,1), sig: {y -> 0}, l': plus(0,1), r: plus(plus(x,y),1), r': 1) (R9 unifies with R1 at p: [2], l: times(x,m(y)), lp: m(y), sig: {y -> m(x')}, l': m(m(x')), r: m(times(x,y)), r': x') (R9 unifies with R2 at p: [2], l: times(x,m(y)), lp: m(y), sig: {y -> 0}, l': m(0), r: m(times(x,y)), r': 0) (R10 unifies with R3 at p: [2], l: times(x,plus(y,1)), lp: plus(y,1), sig: {y -> m(plus(x',1))}, l': plus(m(plus(x',1)),1), r: plus(times(x,y),x), r': m(x')) (R10 unifies with R4 at p: [2], l: times(x,plus(y,1)), lp: plus(y,1), sig: {y -> m(1)}, l': plus(m(1),1), r: plus(times(x,y),x), r': 0) (R10 unifies with R5 at p: [2], l: times(x,plus(y,1)), lp: plus(y,1), sig: {y -> 0}, l': plus(0,1), r: plus(times(x,y),x), r': 1) -> Critical pairs info: => Not trivial, Not overlay, Proper, NW0, N1 => Not trivial, Not overlay, Proper, NW0, N2 => Trivial, Not overlay, Proper, NW0, N3 => Not trivial, Not overlay, Proper, NW0, N4 => Not trivial, Not overlay, Proper, NW0, N5 => Not trivial, Not overlay, Proper, NW0, N6 => Not trivial, Not overlay, Proper, NW0, N7 => Not trivial, Not overlay, Proper, NW0, N8 => Not trivial, Not overlay, Proper, NW0, N9 => Not trivial, Not overlay, Proper, NW0, N10 => Not trivial, Not overlay, Proper, NW0, N11 => Not trivial, Not overlay, Proper, NW0, N12 => Not trivial, Not overlay, Proper, NW0, N13 => Not trivial, Not overlay, Proper, NW0, N14 => Not trivial, Not overlay, Proper, NW0, N15 -> 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: No Convergence Brute Force Procedure: -> Rewritings: s: times(x,1) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('times(x,1)', D0) ID: 1 => ('x', D1, R12, P[], S{x17 -> x}), NR: 'x' t: plus(times(x,0),x) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('plus(times(x,0),x)', D0) ID: 1 => ('plus(0,x)', D1, R11, P[1], S{x16 -> x}), NR: '0' times(x,1) ->* no union *<- plus(times(x,0),x) "Not joinable" The problem is not confluent.