NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a) (b) (h 1, 2) (c) (f 1) (fSNonEmpty) ) (RULES a -> f(b) b -> f(b) b -> f(c) h(b,f(c)) -> c h(c,c) -> c ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a) (b) (h 1, 2) (c) (f 1) (fSNonEmpty) ) (RULES a -> f(b) b -> f(b) b -> f(c) h(b,f(c)) -> c h(c,c) -> c ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: a -> f(b) b -> f(b) b -> f(c) h(b,f(c)) -> c h(c,c) -> c -> Vars: -> Rlps: (rule: a -> f(b), id: 1, possubterms: a->[]) (rule: b -> f(b), id: 2, possubterms: b->[]) (rule: b -> f(c), id: 3, possubterms: b->[]) (rule: h(b,f(c)) -> c, id: 4, possubterms: h(b,f(c))->[], b->[1], f(c)->[2], c->[2, 1]) (rule: h(c,c) -> c, id: 5, possubterms: h(c,c)->[], c->[1], c->[2]) -> Unifications: (R3 unifies with R2 at p: [], l: b, lp: b, sig: {}, l': b, r: f(c), r': f(b)) (R4 unifies with R2 at p: [1], l: h(b,f(c)), lp: b, sig: {}, l': b, r: c, r': f(b)) (R4 unifies with R3 at p: [1], l: h(b,f(c)), lp: b, sig: {}, l': b, r: c, r': f(c)) -> Critical pairs info: => Not trivial, Not overlay, Proper, NW0, N1 => Not trivial, Not overlay, Proper, NW0, N2 => Not trivial, Overlay, Proper, NW0, N3 -> 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 Problem 1: No Convergence Brute Force Procedure: -> Rewritings: s: h(f(c),f(c)) Nodes: [0] Edges: [] ID: 0 => ('h(f(c),f(c))', D0) t: c Nodes: [0] Edges: [] ID: 0 => ('c', D0) h(f(c),f(c)) ->* no union *<- c "Not joinable" The problem is not confluent.