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