NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a) (c) (f 1) (h 1, 2) (b) (fSNonEmpty) ) (RULES a -> h(h(b,b),b) c -> a f(h(a,c)) -> h(f(b),h(c,h(c,h(f(h(b,b)),a)))) h(h(h(f(b),c),b),h(a,h(a,c))) -> h(f(b),h(c,b)) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a) (c) (f 1) (h 1, 2) (b) (fSNonEmpty) ) (RULES a -> h(h(b,b),b) c -> a f(h(a,c)) -> h(f(b),h(c,h(c,h(f(h(b,b)),a)))) h(h(h(f(b),c),b),h(a,h(a,c))) -> h(f(b),h(c,b)) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: a -> h(h(b,b),b) c -> a f(h(a,c)) -> h(f(b),h(c,h(c,h(f(h(b,b)),a)))) h(h(h(f(b),c),b),h(a,h(a,c))) -> h(f(b),h(c,b)) -> Vars: -> Rlps: (rule: a -> h(h(b,b),b), id: 1, possubterms: a->[]) (rule: c -> a, id: 2, possubterms: c->[]) (rule: f(h(a,c)) -> h(f(b),h(c,h(c,h(f(h(b,b)),a)))), id: 3, possubterms: f(h(a,c))->[], h(a,c)->[1], a->[1, 1], c->[1, 2]) (rule: h(h(h(f(b),c),b),h(a,h(a,c))) -> h(f(b),h(c,b)), id: 4, possubterms: h(h(h(f(b),c),b),h(a,h(a,c)))->[], h(h(f(b),c),b)->[1], h(f(b),c)->[1, 1], f(b)->[1, 1, 1], b->[1, 1, 1, 1], c->[1, 1, 2], b->[1, 2], h(a,h(a,c))->[2], a->[2, 1], h(a,c)->[2, 2], a->[2, 2, 1], c->[2, 2, 2]) -> Unifications: (R3 unifies with R1 at p: [1,1], l: f(h(a,c)), lp: a, sig: {}, l': a, r: h(f(b),h(c,h(c,h(f(h(b,b)),a)))), r': h(h(b,b),b)) (R3 unifies with R2 at p: [1,2], l: f(h(a,c)), lp: c, sig: {}, l': c, r: h(f(b),h(c,h(c,h(f(h(b,b)),a)))), r': a) (R4 unifies with R2 at p: [1,1,2], l: h(h(h(f(b),c),b),h(a,h(a,c))), lp: c, sig: {}, l': c, r: h(f(b),h(c,b)), r': a) (R4 unifies with R1 at p: [2,1], l: h(h(h(f(b),c),b),h(a,h(a,c))), lp: a, sig: {}, l': a, r: h(f(b),h(c,b)), r': h(h(b,b),b)) (R4 unifies with R1 at p: [2,2,1], l: h(h(h(f(b),c),b),h(a,h(a,c))), lp: a, sig: {}, l': a, r: h(f(b),h(c,b)), r': h(h(b,b),b)) (R4 unifies with R2 at p: [2,2,2], l: h(h(h(f(b),c),b),h(a,h(a,c))), lp: c, sig: {}, l': c, r: h(f(b),h(c,b)), r': a) -> Critical pairs info: => Not trivial, Not overlay, Proper, NW0, N1 => Not trivial, Not overlay, Proper, NW0, N2 => Not 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 -> 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(h(h(f(b),a),b),h(a,h(a,c))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23] Edges: [(0,1),(0,2),(0,3),(0,4),(1,5),(1,6),(1,7),(2,5),(2,8),(2,9),(3,6),(3,8),(3,10),(4,7),(4,9),(4,10),(4,11),(5,12),(5,13),(6,12),(6,14),(7,13),(7,14),(7,15),(8,12),(8,16),(9,13),(9,16),(9,17),(10,14),(10,16),(10,18),(11,15),(11,17),(11,18),(12,19),(13,19),(13,20),(14,19),(14,21),(15,20),(15,21),(16,19),(16,22),(17,20),(17,22),(18,21),(18,22),(19,23),(20,23),(21,23),(22,23)] ID: 0 => ('h(h(h(f(b),a),b),h(a,h(a,c)))', D0) ID: 1 => ('h(h(h(f(b),h(h(b,b),b)),b),h(a,h(a,c)))', D1, R1, P[1, 1, 2], S{}), NR: 'h(h(b,b),b)' ID: 2 => ('h(h(h(f(b),a),b),h(h(h(b,b),b),h(a,c)))', D1, R1, P[2, 1], S{}), NR: 'h(h(b,b),b)' ID: 3 => ('h(h(h(f(b),a),b),h(a,h(h(h(b,b),b),c)))', D1, R1, P[2, 2, 1], S{}), NR: 'h(h(b,b),b)' ID: 4 => ('h(h(h(f(b),a),b),h(a,h(a,a)))', D1, R2, P[2, 2, 2], S{}), NR: 'a' ID: 5 => ('h(h(h(f(b),h(h(b,b),b)),b),h(h(h(b,b),b),h(a,c)))', D2, R1, P[2, 1], S{}), NR: 'h(h(b,b),b)' ID: 6 => ('h(h(h(f(b),h(h(b,b),b)),b),h(a,h(h(h(b,b),b),c)))', D2, R1, P[2, 2, 1], S{}), NR: 'h(h(b,b),b)' ID: 7 => ('h(h(h(f(b),h(h(b,b),b)),b),h(a,h(a,a)))', D2, R2, P[2, 2, 2], S{}), NR: 'a' ID: 8 => ('h(h(h(f(b),a),b),h(h(h(b,b),b),h(h(h(b,b),b),c)))', D2, R1, P[2, 2, 1], S{}), NR: 'h(h(b,b),b)' ID: 9 => ('h(h(h(f(b),a),b),h(h(h(b,b),b),h(a,a)))', D2, R2, P[2, 2, 2], S{}), NR: 'a' ID: 10 => ('h(h(h(f(b),a),b),h(a,h(h(h(b,b),b),a)))', D2, R2, P[2, 2, 2], S{}), NR: 'a' ID: 11 => ('h(h(h(f(b),a),b),h(a,h(a,h(h(b,b),b))))', D2, R1, P[2, 2, 2], S{}), NR: 'h(h(b,b),b)' ID: 12 => ('h(h(h(f(b),h(h(b,b),b)),b),h(h(h(b,b),b),h(h(h(b,b),b),c)))', D3, R1, P[2, 2, 1], S{}), NR: 'h(h(b,b),b)' ID: 13 => ('h(h(h(f(b),h(h(b,b),b)),b),h(h(h(b,b),b),h(a,a)))', D3, R2, P[2, 2, 2], S{}), NR: 'a' ID: 14 => ('h(h(h(f(b),h(h(b,b),b)),b),h(a,h(h(h(b,b),b),a)))', D3, R2, P[2, 2, 2], S{}), NR: 'a' ID: 15 => ('h(h(h(f(b),h(h(b,b),b)),b),h(a,h(a,h(h(b,b),b))))', D3, R1, P[2, 2, 2], S{}), NR: 'h(h(b,b),b)' ID: 16 => ('h(h(h(f(b),a),b),h(h(h(b,b),b),h(h(h(b,b),b),a)))', D3, R2, P[2, 2, 2], S{}), NR: 'a' ID: 17 => ('h(h(h(f(b),a),b),h(h(h(b,b),b),h(a,h(h(b,b),b))))', D3, R1, P[2, 2, 2], S{}), NR: 'h(h(b,b),b)' ID: 18 => ('h(h(h(f(b),a),b),h(a,h(h(h(b,b),b),h(h(b,b),b))))', D3, R1, P[2, 2, 2], S{}), NR: 'h(h(b,b),b)' ID: 19 => ('h(h(h(f(b),h(h(b,b),b)),b),h(h(h(b,b),b),h(h(h(b,b),b),a)))', D4, R2, P[2, 2, 2], S{}), NR: 'a' ID: 20 => ('h(h(h(f(b),h(h(b,b),b)),b),h(h(h(b,b),b),h(a,h(h(b,b),b))))', D4, R1, P[2, 2, 2], S{}), NR: 'h(h(b,b),b)' ID: 21 => ('h(h(h(f(b),h(h(b,b),b)),b),h(a,h(h(h(b,b),b),h(h(b,b),b))))', D4, R1, P[2, 2, 2], S{}), NR: 'h(h(b,b),b)' ID: 22 => ('h(h(h(f(b),a),b),h(h(h(b,b),b),h(h(h(b,b),b),h(h(b,b),b))))', D4, R1, P[2, 2, 2], S{}), NR: 'h(h(b,b),b)' ID: 23 => ('h(h(h(f(b),h(h(b,b),b)),b),h(h(h(b,b),b),h(h(h(b,b),b),h(h(b,b),b))))', D5, R1, P[2, 2, 2], S{}), NR: 'h(h(b,b),b)' t: h(f(b),h(c,b)) Nodes: [0,1,2] Edges: [(0,1),(1,2)] ID: 0 => ('h(f(b),h(c,b))', D0) ID: 1 => ('h(f(b),h(a,b))', D1, R2, P[2, 1], S{}), NR: 'a' ID: 2 => ('h(f(b),h(h(h(b,b),b),b))', D2, R1, P[2, 1], S{}), NR: 'h(h(b,b),b)' h(h(h(f(b),a),b),h(a,h(a,c))) ->* no union *<- h(f(b),h(c,b)) "Not joinable" The problem is not confluent.