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