NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (0 1) (1 1) (2 1) (fSNonEmpty) ) (RULES 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))))))))))) 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))))))))) 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))))) 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))) 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x))))))))))))) 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(x)))))))))) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (0 1) (1 1) (2 1) (fSNonEmpty) ) (RULES 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))))))))))) 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))))))))) 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))))) 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))) 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x))))))))))))) 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(x)))))))))) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))))))))))) 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))))))))) 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))))) 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))) 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x))))))))))))) 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(x)))))))))) -> Vars: x, x, x, x, x, x -> Rlps: (rule: 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))))))))))), id: 1, possubterms: 0(1(2(1(x))))->[], 1(2(1(x)))->[1], 2(1(x))->[1, 1], 1(x)->[1, 1, 1]) (rule: 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))))))))), id: 2, possubterms: 0(1(2(1(x))))->[], 1(2(1(x)))->[1], 2(1(x))->[1, 1], 1(x)->[1, 1, 1]) (rule: 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))))), id: 3, possubterms: 0(1(2(1(x))))->[], 1(2(1(x)))->[1], 2(1(x))->[1, 1], 1(x)->[1, 1, 1]) (rule: 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))), id: 4, possubterms: 0(1(2(1(x))))->[], 1(2(1(x)))->[1], 2(1(x))->[1, 1], 1(x)->[1, 1, 1]) (rule: 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x))))))))))))), id: 5, possubterms: 0(1(2(1(x))))->[], 1(2(1(x)))->[1], 2(1(x))->[1, 1], 1(x)->[1, 1, 1]) (rule: 0(1(2(1(x)))) -> 1(2(1(1(0(1(2(0(1(2(x)))))))))), id: 6, possubterms: 0(1(2(1(x))))->[], 1(2(1(x)))->[1], 2(1(x))->[1, 1], 1(x)->[1, 1, 1]) -> Unifications: (R2 unifies with R1 at p: [], l: 0(1(2(1(x)))), lp: 0(1(2(1(x)))), sig: {x -> x'}, l': 0(1(2(1(x')))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))))))))))))) (R3 unifies with R1 at p: [], l: 0(1(2(1(x)))), lp: 0(1(2(1(x)))), sig: {x -> x'}, l': 0(1(2(1(x')))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))))))))))))) (R3 unifies with R2 at p: [], l: 0(1(2(1(x)))), lp: 0(1(2(1(x)))), sig: {x -> x'}, l': 0(1(2(1(x')))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))))))))) (R4 unifies with R1 at p: [], l: 0(1(2(1(x)))), lp: 0(1(2(1(x)))), sig: {x -> x'}, l': 0(1(2(1(x')))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))))))))))))) (R4 unifies with R2 at p: [], l: 0(1(2(1(x)))), lp: 0(1(2(1(x)))), sig: {x -> x'}, l': 0(1(2(1(x')))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))))))))) (R4 unifies with R3 at p: [], l: 0(1(2(1(x)))), lp: 0(1(2(1(x)))), sig: {x -> x'}, l': 0(1(2(1(x')))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))))))) (R5 unifies with R1 at p: [], l: 0(1(2(1(x)))), lp: 0(1(2(1(x)))), sig: {x -> x'}, l': 0(1(2(1(x')))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(x))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))))))))))))) (R5 unifies with R2 at p: [], l: 0(1(2(1(x)))), lp: 0(1(2(1(x)))), sig: {x -> x'}, l': 0(1(2(1(x')))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(x))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))))))))) (R5 unifies with R3 at p: [], l: 0(1(2(1(x)))), lp: 0(1(2(1(x)))), sig: {x -> x'}, l': 0(1(2(1(x')))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(x))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))))))) (R5 unifies with R4 at p: [], l: 0(1(2(1(x)))), lp: 0(1(2(1(x)))), sig: {x -> x'}, l': 0(1(2(1(x')))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(x))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))) (R6 unifies with R1 at p: [], l: 0(1(2(1(x)))), lp: 0(1(2(1(x)))), sig: {x -> x'}, l': 0(1(2(1(x')))), r: 1(2(1(1(0(1(2(0(1(2(x)))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))))))))))))) (R6 unifies with R2 at p: [], l: 0(1(2(1(x)))), lp: 0(1(2(1(x)))), sig: {x -> x'}, l': 0(1(2(1(x')))), r: 1(2(1(1(0(1(2(0(1(2(x)))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))))))))) (R6 unifies with R3 at p: [], l: 0(1(2(1(x)))), lp: 0(1(2(1(x)))), sig: {x -> x'}, l': 0(1(2(1(x')))), r: 1(2(1(1(0(1(2(0(1(2(x)))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))))))) (R6 unifies with R4 at p: [], l: 0(1(2(1(x)))), lp: 0(1(2(1(x)))), sig: {x -> x'}, l': 0(1(2(1(x')))), r: 1(2(1(1(0(1(2(0(1(2(x)))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))) (R6 unifies with R5 at p: [], l: 0(1(2(1(x)))), lp: 0(1(2(1(x)))), sig: {x -> x'}, l': 0(1(2(1(x')))), r: 1(2(1(1(0(1(2(0(1(2(x)))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(x')))))))))))))) -> Critical pairs info: <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(x')))))))))))))> => Not trivial, Overlay, Proper, NW0, N1 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(x')))))))))))))> => Not trivial, Overlay, Proper, NW0, N2 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))))))> => Not trivial, Overlay, Proper, NW0, N3 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))))))))> => Not trivial, Overlay, Proper, NW0, N4 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(x')))))))))))))> => Not trivial, Overlay, Proper, NW0, N5 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))),1(2(1(1(0(1(2(0(1(2(x'))))))))))> => Not trivial, Overlay, Proper, NW0, N6 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(x'))))))))))> => Not trivial, Overlay, Proper, NW0, N7 <1(2(1(1(0(1(2(0(1(2(0(1(2(x'))))))))))))),1(2(1(1(0(1(2(0(1(2(x'))))))))))> => Not trivial, Overlay, Proper, NW0, N8 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))> => Not trivial, Overlay, Proper, NW0, N9 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))> => Not trivial, Overlay, Proper, NW0, N10 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))))))> => Not trivial, Overlay, Proper, NW0, N11 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(x'))))))))))> => Not trivial, Overlay, Proper, NW0, N12 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(x')))))))))))))> => Not trivial, Overlay, Proper, NW0, N13 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(x'))))))))))> => Not trivial, Overlay, Proper, NW0, N14 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))> => Not trivial, Overlay, Proper, NW0, N15 -> 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: 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))))))))))) Nodes: [0] Edges: [] ID: 0 => ('1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x')))))))))))))))))))))))))', D0) t: 1(2(1(1(0(1(2(0(1(2(0(1(2(x'))))))))))))) Nodes: [0] Edges: [] ID: 0 => ('1(2(1(1(0(1(2(0(1(2(0(1(2(x')))))))))))))', D0) 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x'))))))))))))))))))))))))) ->* no union *<- 1(2(1(1(0(1(2(0(1(2(0(1(2(x'))))))))))))) "Not joinable" The problem is not confluent.