YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (f 1) (g 1) (h 1) (fSNonEmpty) ) (RULES f(x) -> g(x) f(x) -> h(f(x)) g(x) -> h(g(x)) h(f(x)) -> h(g(x)) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: Linearity Procedure: Linear? YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (f 1) (g 1) (h 1) (fSNonEmpty) ) (RULES f(x) -> g(x) f(x) -> h(f(x)) g(x) -> h(g(x)) h(f(x)) -> h(g(x)) ) Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: f(x) -> g(x) f(x) -> h(f(x)) g(x) -> h(g(x)) h(f(x)) -> h(g(x)) -> Vars: x, x, x, x -> Rlps: (rule: f(x) -> g(x), id: 1, possubterms: f(x)->[]) (rule: f(x) -> h(f(x)), id: 2, possubterms: f(x)->[]) (rule: g(x) -> h(g(x)), id: 3, possubterms: g(x)->[]) (rule: h(f(x)) -> h(g(x)), id: 4, possubterms: h(f(x))->[], f(x)->[1]) -> Unifications: (R2 unifies with R1 at p: [], l: f(x), lp: f(x), sig: {x -> x'}, l': f(x'), r: h(f(x)), r': g(x')) (R4 unifies with R1 at p: [1], l: h(f(x)), lp: f(x), sig: {x -> x'}, l': f(x'), r: h(g(x)), r': g(x')) (R4 unifies with R2 at p: [1], l: h(f(x)), lp: f(x), sig: {x -> x'}, l': f(x'), r: h(g(x)), r': h(f(x'))) -> Critical pairs info: => Not trivial, Overlay, Proper, NW0, N1 => Trivial, Not overlay, Proper, NW0, N2 => Not trivial, Not 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 The problem is decomposed in 2 subproblems. Problem 1.1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (f 1) (g 1) (h 1) (fSNonEmpty) ) (RULES f(x) -> g(x) f(x) -> h(f(x)) g(x) -> h(g(x)) h(f(x)) -> h(g(x)) ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N1 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: g(x') Nodes: [0,1,2,3,4,5,6,7,8] Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(5,6),(6,7),(7,8)] ID: 0 => ('g(x')', D0) ID: 1 => ('h(g(x'))', D1, R3, P[], S{x6 -> x'}), NR: 'h(g(x'))' ID: 2 => ('h(h(g(x')))', D2, R3, P[1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 3 => ('h(h(h(g(x'))))', D3, R3, P[1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 4 => ('h(h(h(h(g(x')))))', D4, R3, P[1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 5 => ('h(h(h(h(h(g(x'))))))', D5, R3, P[1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 6 => ('h(h(h(h(h(h(g(x')))))))', D6, R3, P[1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 7 => ('h(h(h(h(h(h(h(g(x'))))))))', D7, R3, P[1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 8 => ('h(h(h(h(h(h(h(h(g(x')))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' t: h(f(x')) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] Edges: [(0,1),(0,1),(0,2),(1,3),(2,3),(2,3),(2,4),(3,5),(4,5),(4,5),(4,6),(5,7),(6,7),(6,7),(6,8),(7,9),(8,9),(8,9),(8,10),(9,11),(10,11),(10,11),(10,12),(11,13),(12,13),(12,13),(12,14),(13,15),(14,15),(14,15),(14,16)] ID: 0 => ('h(f(x'))', D0) ID: 1 => ('h(g(x'))', D1, R1, P[1], S{x4 -> x'}), NR: 'g(x')' ID: 2 => ('h(h(f(x')))', D1, R2, P[1], S{x5 -> x'}), NR: 'h(f(x'))' ID: 3 => ('h(h(g(x')))', D2, R3, P[1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 4 => ('h(h(h(f(x'))))', D2, R2, P[1, 1], S{x5 -> x'}), NR: 'h(f(x'))' ID: 5 => ('h(h(h(g(x'))))', D3, R3, P[1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 6 => ('h(h(h(h(f(x')))))', D3, R2, P[1, 1, 1], S{x5 -> x'}), NR: 'h(f(x'))' ID: 7 => ('h(h(h(h(g(x')))))', D4, R3, P[1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 8 => ('h(h(h(h(h(f(x'))))))', D4, R2, P[1, 1, 1, 1], S{x5 -> x'}), NR: 'h(f(x'))' ID: 9 => ('h(h(h(h(h(g(x'))))))', D5, R3, P[1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 10 => ('h(h(h(h(h(h(f(x')))))))', D5, R2, P[1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'h(f(x'))' ID: 11 => ('h(h(h(h(h(h(g(x')))))))', D6, R3, P[1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 12 => ('h(h(h(h(h(h(h(f(x'))))))))', D6, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'h(f(x'))' ID: 13 => ('h(h(h(h(h(h(h(g(x'))))))))', D7, R3, P[1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 14 => ('h(h(h(h(h(h(h(h(f(x')))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'h(f(x'))' ID: 15 => ('h(h(h(h(h(h(h(h(g(x')))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 16 => ('h(h(h(h(h(h(h(h(h(f(x'))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'h(f(x'))' SNodesPath1: g(x') -> h(g(x')) TNodesPath1: h(f(x')) -> h(g(x')) SNodesPath2: g(x') -> h(g(x')) TNodesPath2: h(f(x')) -> h(g(x')) g(x') ->= h(g(x')) *<- h(f(x')) h(f(x')) ->= h(g(x')) *<- g(x') "Strongly closed critical pair" The problem is confluent. Problem 1.2: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (f 1) (g 1) (h 1) (fSNonEmpty) ) (RULES f(x) -> g(x) f(x) -> h(f(x)) g(x) -> h(g(x)) h(f(x)) -> h(g(x)) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N3 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: h(h(f(x'))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] Edges: [(0,1),(0,1),(0,2),(1,3),(2,3),(2,3),(2,4),(3,5),(4,5),(4,5),(4,6),(5,7),(6,7),(6,7),(6,8),(7,9),(8,9),(8,9),(8,10),(9,11),(10,11),(10,11),(10,12),(11,13),(12,13),(12,13),(12,14),(13,15),(14,15),(14,15),(14,16)] ID: 0 => ('h(h(f(x')))', D0) ID: 1 => ('h(h(g(x')))', D1, R1, P[1, 1], S{x4 -> x'}), NR: 'g(x')' ID: 2 => ('h(h(h(f(x'))))', D1, R2, P[1, 1], S{x5 -> x'}), NR: 'h(f(x'))' ID: 3 => ('h(h(h(g(x'))))', D2, R3, P[1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 4 => ('h(h(h(h(f(x')))))', D2, R2, P[1, 1, 1], S{x5 -> x'}), NR: 'h(f(x'))' ID: 5 => ('h(h(h(h(g(x')))))', D3, R3, P[1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 6 => ('h(h(h(h(h(f(x'))))))', D3, R2, P[1, 1, 1, 1], S{x5 -> x'}), NR: 'h(f(x'))' ID: 7 => ('h(h(h(h(h(g(x'))))))', D4, R3, P[1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 8 => ('h(h(h(h(h(h(f(x')))))))', D4, R2, P[1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'h(f(x'))' ID: 9 => ('h(h(h(h(h(h(g(x')))))))', D5, R3, P[1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 10 => ('h(h(h(h(h(h(h(f(x'))))))))', D5, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'h(f(x'))' ID: 11 => ('h(h(h(h(h(h(h(g(x'))))))))', D6, R3, P[1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 12 => ('h(h(h(h(h(h(h(h(f(x')))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'h(f(x'))' ID: 13 => ('h(h(h(h(h(h(h(h(g(x')))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 14 => ('h(h(h(h(h(h(h(h(h(f(x'))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'h(f(x'))' ID: 15 => ('h(h(h(h(h(h(h(h(h(g(x'))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 16 => ('h(h(h(h(h(h(h(h(h(h(f(x')))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'h(f(x'))' t: h(g(x')) Nodes: [0,1,2,3,4,5,6,7,8] Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(5,6),(6,7),(7,8)] ID: 0 => ('h(g(x'))', D0) ID: 1 => ('h(h(g(x')))', D1, R3, P[1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 2 => ('h(h(h(g(x'))))', D2, R3, P[1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 3 => ('h(h(h(h(g(x')))))', D3, R3, P[1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 4 => ('h(h(h(h(h(g(x'))))))', D4, R3, P[1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 5 => ('h(h(h(h(h(h(g(x')))))))', D5, R3, P[1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 6 => ('h(h(h(h(h(h(h(g(x'))))))))', D6, R3, P[1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 7 => ('h(h(h(h(h(h(h(h(g(x')))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' ID: 8 => ('h(h(h(h(h(h(h(h(h(g(x'))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'h(g(x'))' SNodesPath1: h(h(f(x'))) -> h(h(g(x'))) TNodesPath1: h(g(x')) -> h(h(g(x'))) SNodesPath2: h(h(f(x'))) -> h(h(g(x'))) TNodesPath2: h(g(x')) -> h(h(g(x'))) h(h(f(x'))) ->= h(h(g(x'))) *<- h(g(x')) h(g(x')) ->= h(h(g(x'))) *<- h(h(f(x'))) "Strongly closed critical pair" The problem is confluent.