YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(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 (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) -> Vars: x, x, x, x, x -> Rlps: (rule: b(a(b(b(x)))) -> b(b(x)), id: 1, possubterms: b(a(b(b(x))))->[], a(b(b(x)))->[1], b(b(x))->[1, 1], b(x)->[1, 1, 1]) (rule: b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))), id: 2, possubterms: b(a(b(a(a(a(a(b(x))))))))->[], a(b(a(a(a(a(b(x)))))))->[1], b(a(a(a(a(b(x))))))->[1, 1], a(a(a(a(b(x)))))->[1, 1, 1], a(a(a(b(x))))->[1, 1, 1, 1], a(a(b(x)))->[1, 1, 1, 1, 1], a(b(x))->[1, 1, 1, 1, 1, 1], b(x)->[1, 1, 1, 1, 1, 1, 1]) (rule: b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))), id: 3, possubterms: b(a(a(b(b(x)))))->[], a(a(b(b(x))))->[1], a(b(b(x)))->[1, 1], b(b(x))->[1, 1, 1], b(x)->[1, 1, 1, 1]) (rule: b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))), id: 4, possubterms: b(a(a(b(a(a(a(a(b(x)))))))))->[], a(a(b(a(a(a(a(b(x))))))))->[1], a(b(a(a(a(a(b(x)))))))->[1, 1], b(a(a(a(a(b(x))))))->[1, 1, 1], a(a(a(a(b(x)))))->[1, 1, 1, 1], a(a(a(b(x))))->[1, 1, 1, 1, 1], a(a(b(x)))->[1, 1, 1, 1, 1, 1], a(b(x))->[1, 1, 1, 1, 1, 1, 1], b(x)->[1, 1, 1, 1, 1, 1, 1, 1]) (rule: b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x), id: 5, possubterms: b(a(a(a(b(a(a(a(a(b(x))))))))))->[], a(a(a(b(a(a(a(a(b(x)))))))))->[1], a(a(b(a(a(a(a(b(x))))))))->[1, 1], a(b(a(a(a(a(b(x)))))))->[1, 1, 1], b(a(a(a(a(b(x))))))->[1, 1, 1, 1], a(a(a(a(b(x)))))->[1, 1, 1, 1, 1], a(a(a(b(x))))->[1, 1, 1, 1, 1, 1], a(a(b(x)))->[1, 1, 1, 1, 1, 1, 1], a(b(x))->[1, 1, 1, 1, 1, 1, 1, 1], b(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1]) -> Unifications: (R1 unifies with R1 at p: [1,1,1], l: b(a(b(b(x)))), lp: b(x), sig: {x -> a(b(b(x')))}, l': b(a(b(b(x')))), r: b(b(x)), r': b(b(x'))) (R1 unifies with R2 at p: [1,1,1], l: b(a(b(b(x)))), lp: b(x), sig: {x -> a(b(a(a(a(a(b(x')))))))}, l': b(a(b(a(a(a(a(b(x')))))))), r: b(b(x)), r': b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) (R1 unifies with R3 at p: [1,1,1], l: b(a(b(b(x)))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(b(x)), r': b(a(a(a(a(b(b(x')))))))) (R1 unifies with R4 at p: [1,1,1], l: b(a(b(b(x)))), lp: b(x), sig: {x -> a(a(b(a(a(a(a(b(x'))))))))}, l': b(a(a(b(a(a(a(a(b(x'))))))))), r: b(b(x)), r': b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) (R1 unifies with R5 at p: [1,1,1], l: b(a(b(b(x)))), lp: b(x), sig: {x -> a(a(a(b(a(a(a(a(b(x')))))))))}, l': b(a(a(a(b(a(a(a(a(b(x')))))))))), r: b(b(x)), r': b(x')) (R2 unifies with R1 at p: [1,1,1,1,1,1,1], l: b(a(b(a(a(a(a(b(x)))))))), lp: b(x), sig: {x -> a(b(b(x')))}, l': b(a(b(b(x')))), r: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))), r': b(b(x'))) (R2 unifies with R2 at p: [1,1,1,1,1,1,1], l: b(a(b(a(a(a(a(b(x)))))))), lp: b(x), sig: {x -> a(b(a(a(a(a(b(x')))))))}, l': b(a(b(a(a(a(a(b(x')))))))), r: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))), r': b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) (R2 unifies with R3 at p: [1,1,1,1,1,1,1], l: b(a(b(a(a(a(a(b(x)))))))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))), r': b(a(a(a(a(b(b(x')))))))) (R2 unifies with R4 at p: [1,1,1,1,1,1,1], l: b(a(b(a(a(a(a(b(x)))))))), lp: b(x), sig: {x -> a(a(b(a(a(a(a(b(x'))))))))}, l': b(a(a(b(a(a(a(a(b(x'))))))))), r: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))), r': b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) (R2 unifies with R5 at p: [1,1,1,1,1,1,1], l: b(a(b(a(a(a(a(b(x)))))))), lp: b(x), sig: {x -> a(a(a(b(a(a(a(a(b(x')))))))))}, l': b(a(a(a(b(a(a(a(a(b(x')))))))))), r: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))), r': b(x')) (R3 unifies with R1 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> a(b(b(x')))}, l': b(a(b(b(x')))), r: b(a(a(a(a(b(b(x))))))), r': b(b(x'))) (R3 unifies with R2 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> a(b(a(a(a(a(b(x')))))))}, l': b(a(b(a(a(a(a(b(x')))))))), r: b(a(a(a(a(b(b(x))))))), r': b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) (R3 unifies with R3 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(a(a(a(a(b(b(x))))))), r': b(a(a(a(a(b(b(x')))))))) (R3 unifies with R4 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> a(a(b(a(a(a(a(b(x'))))))))}, l': b(a(a(b(a(a(a(a(b(x'))))))))), r: b(a(a(a(a(b(b(x))))))), r': b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) (R3 unifies with R5 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> a(a(a(b(a(a(a(a(b(x')))))))))}, l': b(a(a(a(b(a(a(a(a(b(x')))))))))), r: b(a(a(a(a(b(b(x))))))), r': b(x')) (R4 unifies with R1 at p: [1,1,1,1,1,1,1,1], l: b(a(a(b(a(a(a(a(b(x))))))))), lp: b(x), sig: {x -> a(b(b(x')))}, l': b(a(b(b(x')))), r: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))), r': b(b(x'))) (R4 unifies with R2 at p: [1,1,1,1,1,1,1,1], l: b(a(a(b(a(a(a(a(b(x))))))))), lp: b(x), sig: {x -> a(b(a(a(a(a(b(x')))))))}, l': b(a(b(a(a(a(a(b(x')))))))), r: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))), r': b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) (R4 unifies with R3 at p: [1,1,1,1,1,1,1,1], l: b(a(a(b(a(a(a(a(b(x))))))))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))), r': b(a(a(a(a(b(b(x')))))))) (R4 unifies with R4 at p: [1,1,1,1,1,1,1,1], l: b(a(a(b(a(a(a(a(b(x))))))))), lp: b(x), sig: {x -> a(a(b(a(a(a(a(b(x'))))))))}, l': b(a(a(b(a(a(a(a(b(x'))))))))), r: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))), r': b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) (R4 unifies with R5 at p: [1,1,1,1,1,1,1,1], l: b(a(a(b(a(a(a(a(b(x))))))))), lp: b(x), sig: {x -> a(a(a(b(a(a(a(a(b(x')))))))))}, l': b(a(a(a(b(a(a(a(a(b(x')))))))))), r: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))), r': b(x')) (R5 unifies with R1 at p: [1,1,1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(a(a(b(x)))))))))), lp: b(x), sig: {x -> a(b(b(x')))}, l': b(a(b(b(x')))), r: b(x), r': b(b(x'))) (R5 unifies with R2 at p: [1,1,1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(a(a(b(x)))))))))), lp: b(x), sig: {x -> a(b(a(a(a(a(b(x')))))))}, l': b(a(b(a(a(a(a(b(x')))))))), r: b(x), r': b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) (R5 unifies with R3 at p: [1,1,1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(a(a(b(x)))))))))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(x), r': b(a(a(a(a(b(b(x')))))))) (R5 unifies with R4 at p: [1,1,1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(a(a(b(x)))))))))), lp: b(x), sig: {x -> a(a(b(a(a(a(a(b(x'))))))))}, l': b(a(a(b(a(a(a(a(b(x'))))))))), r: b(x), r': b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) (R5 unifies with R5 at p: [1,1,1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(a(a(b(x)))))))))), lp: b(x), sig: {x -> a(a(a(b(a(a(a(a(b(x')))))))))}, l': b(a(a(a(b(a(a(a(a(b(x')))))))))), r: b(x), r': b(x')) -> 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 => Not trivial, Not overlay, Proper, NW0, N7 => Not trivial, Not overlay, Proper, NW0, N8 => Not trivial, Not overlay, Proper, NW0, N9 => Not trivial, Not overlay, Proper, NW0, N10 => Not trivial, Not overlay, Proper, NW0, N11 => Not trivial, Not overlay, Proper, NW0, N12 => Not trivial, Not overlay, Proper, NW0, N13 => Not trivial, Not overlay, Proper, NW0, N14 => Not trivial, Not overlay, Proper, NW0, N15 => Not trivial, Not overlay, Proper, NW0, N16 => Trivial, Not overlay, Proper, NW0, N17 => Not trivial, Not overlay, Proper, NW0, N18 => Not trivial, Not overlay, Proper, NW0, N19 => Not trivial, Not overlay, Proper, NW0, N20 => Not trivial, Not overlay, Proper, NW0, N21 => Not trivial, Not overlay, Proper, NW0, N22 => Not trivial, Not overlay, Proper, NW0, N23 => Not trivial, Not overlay, Proper, NW0, N24 => Not trivial, Not overlay, Proper, NW0, N25 -> 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 24 subproblems. Problem 1.1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N1 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) Nodes: [0,1,2,3,4,5] Edges: [(0,1),(0,2),(1,3),(1,4),(2,4),(3,5),(4,5)] ID: 0 => ('b(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))', D1, R2, P[], S{x5 -> a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))' ID: 2 => ('b(a(b(a(a(a(a(b(a(b(a(a(b(x')))))))))))))', D1, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 3 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))' ID: 4 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 5 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(b(a(a(b(x'))))))))))))))))))', D3, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' t: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))) Nodes: [0,1,2,3,4,5] Edges: [(0,1),(0,2),(1,3),(1,4),(2,3),(3,5),(4,5)] ID: 0 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))', D1, R4, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x7 -> x'}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))' ID: 2 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(a(b(x')))))))))))))))))))))', D1, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(a(b(a(a(a(a(b(x'))))))))}), NR: 'b(a(a(b(a(a(a(a(b(x')))))))))' ID: 3 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))' ID: 4 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 5 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(b(a(a(b(x'))))))))))))))))))', D3, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' SNodesPath1: b(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))) TNodesPath1: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))) SNodesPath2: b(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))) TNodesPath2: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))) b(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) ->= b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))) *<- b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))) b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))) ->= b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))) *<- b(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.2: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N2 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13] Edges: [(0,1),(0,2),(1,3),(1,4),(2,4),(3,5),(3,6),(4,6),(5,7),(5,8),(6,8),(7,9),(7,10),(8,10),(9,11),(9,12),(10,12),(11,13),(12,13)] ID: 0 => ('b(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))', D0) ID: 1 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))', D1, R4, P[], S{x7 -> a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))' ID: 2 => ('b(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))))))))))', D1, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 3 => ('b(a(b(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1], S{x8 -> a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))' ID: 4 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 5 => ('b(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))', D3, R4, P[1, 1], S{x7 -> a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))' ID: 6 => ('b(a(b(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(x'))))))))))))))))))', D3, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 7 => ('b(a(b(a(b(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))', D4, R5, P[1, 1, 1, 1, 1, 1, 1], S{x8 -> a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))}), NR: 'b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))' ID: 8 => ('b(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(x'))))))))))))))))))))))))', D4, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 9 => ('b(a(b(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))', D5, R4, P[1, 1, 1, 1], S{x7 -> a(b(a(a(a(b(a(a(a(a(b(x')))))))))))}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))' ID: 10 => ('b(a(b(a(b(a(a(b(a(a(a(a(b(a(b(x')))))))))))))))', D5, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 11 => ('b(a(b(a(b(a(b(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))', D6, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(b(a(a(a(b(a(a(a(a(b(x')))))))))))}), NR: 'b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))' ID: 12 => ('b(a(b(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))))))))))', D6, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 13 => ('b(a(b(a(b(a(b(a(a(b(a(b(x'))))))))))))', D7, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' t: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(x')))))))))))))))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13] Edges: [(0,1),(0,2),(1,3),(1,4),(2,3),(3,5),(3,6),(4,6),(5,7),(5,8),(6,8),(7,9),(7,10),(8,10),(9,11),(9,12),(10,12),(11,13),(12,13)] ID: 0 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(x'))))))))))))))))))))))', D0) ID: 1 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))', D1, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))' ID: 2 => ('b(a(b(a(a(b(a(b(a(a(a(a(b(x')))))))))))))', D1, R5, P[1, 1, 1, 1, 1], S{x8 -> a(b(a(a(a(a(b(x')))))))}), NR: 'b(a(b(a(a(a(a(b(x'))))))))' ID: 3 => ('b(a(b(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1], S{x8 -> a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))' ID: 4 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 5 => ('b(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))', D3, R4, P[1, 1], S{x7 -> a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))' ID: 6 => ('b(a(b(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(x'))))))))))))))))))', D3, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 7 => ('b(a(b(a(b(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))', D4, R5, P[1, 1, 1, 1, 1, 1, 1], S{x8 -> a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))}), NR: 'b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))' ID: 8 => ('b(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(x'))))))))))))))))))))))))', D4, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 9 => ('b(a(b(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))', D5, R4, P[1, 1, 1, 1], S{x7 -> a(b(a(a(a(b(a(a(a(a(b(x')))))))))))}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))' ID: 10 => ('b(a(b(a(b(a(a(b(a(a(a(a(b(a(b(x')))))))))))))))', D5, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 11 => ('b(a(b(a(b(a(b(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))', D6, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(b(a(a(a(b(a(a(a(a(b(x')))))))))))}), NR: 'b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))' ID: 12 => ('b(a(b(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))))))))))', D6, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 13 => ('b(a(b(a(b(a(b(a(a(b(a(b(x'))))))))))))', D7, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' SNodesPath1: b(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))) TNodesPath1: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(x')))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))) SNodesPath2: b(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))) TNodesPath2: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(x')))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))) b(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))) ->= b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))) *<- b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(x')))))))))))))))))))))) b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(x')))))))))))))))))))))) ->= b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))) *<- b(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.3: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N3 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))) Nodes: [0,1,2,3,4,5] Edges: [(0,1),(1,2),(2,3),(3,4),(4,5)] ID: 0 => ('b(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))))))))))', D1, R2, P[], S{x5 -> a(a(a(a(b(b(x'))))))}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))))))))))' ID: 2 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(b(x')))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(a(a(a(b(b(x'))))))}), NR: 'b(a(a(a(a(b(b(x')))))))' ID: 3 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))))))))))))', D3, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> b(x')}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))' ID: 4 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))))))))))))', D4, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> b(x')}), NR: 'b(b(x'))' ID: 5 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))))', D5, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'b(b(x'))' t: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(x')))))))))))))))))))))))))) Nodes: [0,1,2,3,4,5,6] Edges: [(0,1),(0,2),(1,3),(2,3),(3,4),(4,5),(5,6)] ID: 0 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(x'))))))))))))))))))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))))))))))', D1, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'b(a(a(a(a(b(b(x')))))))' ID: 2 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(b(b(x')))))))))))))))))', D1, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(a(b(b(x'))))}), NR: 'b(a(a(b(b(x')))))' ID: 3 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(b(x')))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(a(a(a(b(b(x'))))))}), NR: 'b(a(a(a(a(b(b(x')))))))' ID: 4 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))))))))))))', D3, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> b(x')}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))' ID: 5 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))))))))))))', D4, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> b(x')}), NR: 'b(b(x'))' ID: 6 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))))', D5, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'b(b(x'))' SNodesPath1: b(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))))))) TNodesPath1: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(x')))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))))))) SNodesPath2: b(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))))))) TNodesPath2: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(x')))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))))))) b(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))) ->= b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))))))) *<- b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(x')))))))))))))))))))))))))) b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(x')))))))))))))))))))))))))) ->= b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))))))) *<- b(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.4: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N4 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(b(b(b(x')))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(a(a(b(b(b(x'))))))', D0) ID: 1 => ('b(a(a(a(a(b(b(b(x'))))))))', D1, R3, P[], S{x6 -> b(x')}), NR: 'b(a(a(a(a(b(b(b(x'))))))))' t: b(a(a(a(a(b(b(a(b(b(x')))))))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(a(a(a(a(b(b(a(b(b(x'))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(b(b(x'))))))))', D1, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'b(b(x'))' SNodesPath1: b(a(a(b(b(b(x')))))) -> b(a(a(a(a(b(b(b(x')))))))) TNodesPath1: b(a(a(a(a(b(b(a(b(b(x')))))))))) -> b(a(a(a(a(b(b(b(x')))))))) SNodesPath2: b(a(a(b(b(b(x')))))) -> b(a(a(a(a(b(b(b(x')))))))) TNodesPath2: b(a(a(a(a(b(b(a(b(b(x')))))))))) -> b(a(a(a(a(b(b(b(x')))))))) b(a(a(b(b(b(x')))))) ->= b(a(a(a(a(b(b(b(x')))))))) *<- b(a(a(a(a(b(b(a(b(b(x')))))))))) b(a(a(a(a(b(b(a(b(b(x')))))))))) ->= b(a(a(a(a(b(b(b(x')))))))) *<- b(a(a(b(b(b(x')))))) "Strongly closed critical pair" The problem is confluent. Problem 1.5: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N5 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(b(x')))))))', D1, R5, P[], S{x8 -> a(a(a(a(b(b(x'))))))}), NR: 'b(a(a(a(a(b(b(x')))))))' t: b(a(a(b(b(x'))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(a(a(b(b(x')))))', D0) ID: 1 => ('b(a(a(a(a(b(b(x')))))))', D1, R3, P[], S{x6 -> x'}), NR: 'b(a(a(a(a(b(b(x')))))))' SNodesPath1: b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))) -> b(a(a(a(a(b(b(x'))))))) TNodesPath1: b(a(a(b(b(x'))))) -> b(a(a(a(a(b(b(x'))))))) SNodesPath2: b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))) -> b(a(a(a(a(b(b(x'))))))) TNodesPath2: b(a(a(b(b(x'))))) -> b(a(a(a(a(b(b(x'))))))) b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))) ->= b(a(a(a(a(b(b(x'))))))) *<- b(a(a(b(b(x'))))) b(a(a(b(b(x'))))) ->= b(a(a(a(a(b(b(x'))))))) *<- b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.6: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N6 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13] Edges: [(0,1),(0,2),(1,3),(1,4),(2,4),(3,5),(3,6),(4,6),(5,7),(5,8),(6,8),(7,9),(7,10),(8,10),(9,11),(9,12),(10,12),(11,13),(12,13)] ID: 0 => ('b(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))))))))))', D1, R2, P[], S{x5 -> a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))))))))))' ID: 2 => ('b(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(x'))))))))))))))))))))', D1, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 3 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))' ID: 4 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(x'))))))))))))))))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 5 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))))))))))))))', D3, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))))' ID: 6 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))))))))))))))', D3, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 7 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))))))', D4, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))}), NR: 'b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))' ID: 8 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))))))))))))))))))))))))))))', D4, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 9 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(a(b(a(a(a(a(b(x')))))))))))}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))' ID: 10 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(a(b(x'))))))))))))))))))))))))))))))', D5, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 11 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))))))))))', D6, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(b(a(a(a(b(a(a(a(a(b(x')))))))))))}), NR: 'b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))' ID: 12 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(x'))))))))))))))))))))))))))))))))))))))))))))', D6, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 13 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(b(x')))))))))))))))))))))))))))))))))))', D7, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' t: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13] Edges: [(0,1),(0,2),(1,3),(1,4),(2,3),(3,5),(3,6),(4,6),(5,7),(5,8),(6,8),(7,9),(7,10),(8,10),(9,11),(9,12),(10,12),(11,13),(12,13)] ID: 0 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))))))))))', D1, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))' ID: 2 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(b(a(a(a(a(b(x'))))))))))))))))))))', D1, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(b(a(a(a(a(b(x')))))))}), NR: 'b(a(b(a(a(a(a(b(x'))))))))' ID: 3 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))' ID: 4 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(x'))))))))))))))))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 5 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))))))))))))))', D3, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))))' ID: 6 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))))))))))))))', D3, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 7 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))))))', D4, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))}), NR: 'b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))' ID: 8 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))))))))))))))))))))))))))))', D4, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 9 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))))))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(a(b(a(a(a(a(b(x')))))))))))}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))))' ID: 10 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(a(b(x'))))))))))))))))))))))))))))))', D5, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 11 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))))))))))', D6, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(b(a(a(a(b(a(a(a(a(b(x')))))))))))}), NR: 'b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))' ID: 12 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(x'))))))))))))))))))))))))))))))))))))))))))))', D6, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 13 => ('b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(b(x')))))))))))))))))))))))))))))))))))', D7, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' SNodesPath1: b(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))))))))) TNodesPath1: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))))))))) SNodesPath2: b(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))))))))) TNodesPath2: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))))))))) b(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) ->= b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))))))))) *<- b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) ->= b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))))))))))))))) *<- b(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.7: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N7 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(b(b(a(a(a(a(b(b(x')))))))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(a(b(b(a(a(a(a(b(b(x'))))))))))', D0) ID: 1 => ('b(b(a(a(a(a(b(b(x'))))))))', D1, R1, P[], S{x4 -> a(a(a(a(b(b(x'))))))}), NR: 'b(b(a(a(a(a(b(b(x'))))))))' t: b(b(a(a(b(b(x')))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(b(a(a(b(b(x'))))))', D0) ID: 1 => ('b(b(a(a(a(a(b(b(x'))))))))', D1, R3, P[1], S{x6 -> x'}), NR: 'b(a(a(a(a(b(b(x')))))))' SNodesPath1: b(a(b(b(a(a(a(a(b(b(x')))))))))) -> b(b(a(a(a(a(b(b(x')))))))) TNodesPath1: b(b(a(a(b(b(x')))))) -> b(b(a(a(a(a(b(b(x')))))))) SNodesPath2: b(a(b(b(a(a(a(a(b(b(x')))))))))) -> b(b(a(a(a(a(b(b(x')))))))) TNodesPath2: b(b(a(a(b(b(x')))))) -> b(b(a(a(a(a(b(b(x')))))))) b(a(b(b(a(a(a(a(b(b(x')))))))))) ->= b(b(a(a(a(a(b(b(x')))))))) *<- b(b(a(a(b(b(x')))))) b(b(a(a(b(b(x')))))) ->= b(b(a(a(a(a(b(b(x')))))))) *<- b(a(b(b(a(a(a(a(b(b(x')))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.8: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N8 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))) Nodes: [0,1,2,3] Edges: [(0,1),(0,2),(1,3),(2,3)] ID: 0 => ('b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))', D0) ID: 1 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))', D1, R5, P[], S{x8 -> a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))' ID: 2 => ('b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(x')))))))))))))))', D1, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 3 => ('b(a(b(a(a(b(x'))))))', D2, R5, P[1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' t: b(a(a(b(a(a(a(a(b(x'))))))))) Nodes: [0,1,2] Edges: [(0,1),(1,2)] ID: 0 => ('b(a(a(b(a(a(a(a(b(x')))))))))', D0) ID: 1 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))', D1, R4, P[], S{x7 -> x'}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))' ID: 2 => ('b(a(b(a(a(b(x'))))))', D2, R5, P[1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' SNodesPath1: b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))) TNodesPath1: b(a(a(b(a(a(a(a(b(x'))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))) SNodesPath2: b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))) TNodesPath2: b(a(a(b(a(a(a(a(b(x'))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))) b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))) ->= b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))) *<- b(a(a(b(a(a(a(a(b(x'))))))))) b(a(a(b(a(a(a(a(b(x'))))))))) ->= b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))) *<- b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.9: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N9 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))) Nodes: [0,1,2,3] Edges: [(0,1),(0,2),(1,3),(2,3)] ID: 0 => ('b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))', D1, R5, P[], S{x8 -> a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))' ID: 2 => ('b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(x'))))))))))))))))))))))', D1, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 3 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' t: b(a(b(a(a(a(a(b(x')))))))) Nodes: [0,1,2] Edges: [(0,1),(1,2)] ID: 0 => ('b(a(b(a(a(a(a(b(x'))))))))', D0) ID: 1 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))', D1, R2, P[], S{x5 -> x'}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))' ID: 2 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' SNodesPath1: b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) TNodesPath1: b(a(b(a(a(a(a(b(x')))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) SNodesPath2: b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) TNodesPath2: b(a(b(a(a(a(a(b(x')))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))) ->= b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) *<- b(a(b(a(a(a(a(b(x')))))))) b(a(b(a(a(a(a(b(x')))))))) ->= b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) *<- b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.10: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N10 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))) Nodes: [0,1,2,3] Edges: [(0,1),(0,2),(1,3),(2,3)] ID: 0 => ('b(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))', D1, R3, P[], S{x6 -> a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))}), NR: 'b(a(a(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))' ID: 2 => ('b(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))))))', D1, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 3 => ('b(a(a(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' t: b(a(a(a(a(b(b(a(b(a(a(a(a(b(x')))))))))))))) Nodes: [0,1,2] Edges: [(0,1),(1,2)] ID: 0 => ('b(a(a(a(a(b(b(a(b(a(a(a(a(b(x'))))))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))', D1, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))' ID: 2 => ('b(a(a(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' SNodesPath1: b(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))) -> b(a(a(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))) TNodesPath1: b(a(a(a(a(b(b(a(b(a(a(a(a(b(x')))))))))))))) -> b(a(a(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))) SNodesPath2: b(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))) -> b(a(a(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))) TNodesPath2: b(a(a(a(a(b(b(a(b(a(a(a(a(b(x')))))))))))))) -> b(a(a(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))) b(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))) ->= b(a(a(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))) *<- b(a(a(a(a(b(b(a(b(a(a(a(a(b(x')))))))))))))) b(a(a(a(a(b(b(a(b(a(a(a(a(b(x')))))))))))))) ->= b(a(a(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))) *<- b(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.11: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N11 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) Nodes: [0,1,2,3,4,5] Edges: [(0,1),(0,2),(1,3),(1,4),(2,4),(3,5),(4,5)] ID: 0 => ('b(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))', D0) ID: 1 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))', D1, R4, P[], S{x7 -> a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))' ID: 2 => ('b(a(a(b(a(a(a(a(b(a(b(a(a(b(x'))))))))))))))', D1, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 3 => ('b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1], S{x8 -> a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))' ID: 4 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 5 => ('b(a(b(a(a(b(a(b(a(a(b(x')))))))))))', D3, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' t: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) Nodes: [0,1,2,3,4,5] Edges: [(0,1),(0,2),(1,3),(1,4),(2,3),(3,5),(4,5)] ID: 0 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))', D0) ID: 1 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))', D1, R4, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x7 -> x'}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))' ID: 2 => ('b(a(b(a(a(b(a(a(b(a(a(a(a(b(x'))))))))))))))', D1, R5, P[1, 1, 1, 1, 1], S{x8 -> a(a(b(a(a(a(a(b(x'))))))))}), NR: 'b(a(a(b(a(a(a(a(b(x')))))))))' ID: 3 => ('b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1], S{x8 -> a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))' ID: 4 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 5 => ('b(a(b(a(a(b(a(b(a(a(b(x')))))))))))', D3, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' SNodesPath1: b(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) TNodesPath1: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) SNodesPath2: b(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) TNodesPath2: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) b(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) ->= b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) *<- b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) ->= b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))) *<- b(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.12: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N12 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))) Nodes: [0,1,2,3] Edges: [(0,1),(0,2),(1,3),(2,3)] ID: 0 => ('b(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))', D0) ID: 1 => ('b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))', D1, R1, P[], S{x4 -> a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))}), NR: 'b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))' ID: 2 => ('b(a(b(b(a(b(a(a(b(x')))))))))', D1, R5, P[1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 3 => ('b(b(a(b(a(a(b(x')))))))', D2, R5, P[1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' t: b(b(a(a(b(a(a(a(a(b(x')))))))))) Nodes: [0,1,2] Edges: [(0,1),(1,2)] ID: 0 => ('b(b(a(a(b(a(a(a(a(b(x'))))))))))', D0) ID: 1 => ('b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))', D1, R4, P[1], S{x7 -> x'}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))' ID: 2 => ('b(b(a(b(a(a(b(x')))))))', D2, R5, P[1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' SNodesPath1: b(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))) -> b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) TNodesPath1: b(b(a(a(b(a(a(a(a(b(x')))))))))) -> b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) SNodesPath2: b(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))) -> b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) TNodesPath2: b(b(a(a(b(a(a(a(a(b(x')))))))))) -> b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) b(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))) ->= b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) *<- b(b(a(a(b(a(a(a(a(b(x')))))))))) b(b(a(a(b(a(a(a(a(b(x')))))))))) ->= b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) *<- b(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.13: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N13 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(b(b(b(x'))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(a(b(b(b(x')))))', D0) ID: 1 => ('b(b(b(x')))', D1, R1, P[], S{x4 -> b(x')}), NR: 'b(b(b(x')))' t: b(b(a(b(b(x'))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(b(a(b(b(x')))))', D0) ID: 1 => ('b(b(b(x')))', D1, R1, P[1], S{x4 -> x'}), NR: 'b(b(x'))' SNodesPath1: b(a(b(b(b(x'))))) -> b(b(b(x'))) TNodesPath1: b(b(a(b(b(x'))))) -> b(b(b(x'))) SNodesPath2: b(a(b(b(b(x'))))) -> b(b(b(x'))) TNodesPath2: b(b(a(b(b(x'))))) -> b(b(b(x'))) b(a(b(b(b(x'))))) ->= b(b(b(x'))) *<- b(b(a(b(b(x'))))) b(b(a(b(b(x'))))) ->= b(b(b(x'))) *<- b(a(b(b(b(x'))))) "Strongly closed critical pair" The problem is confluent. Problem 1.14: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N14 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11] Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(5,6),(6,7),(6,8),(7,9),(7,10),(8,10),(8,11)] ID: 0 => ('b(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))', D0) ID: 1 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))', D1, R4, P[], S{x7 -> a(a(a(a(b(b(x'))))))}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))' ID: 2 => ('b(a(b(a(a(b(a(a(a(a(b(b(x'))))))))))))', D2, R5, P[1, 1, 1, 1, 1], S{x8 -> a(a(a(a(b(b(x'))))))}), NR: 'b(a(a(a(a(b(b(x')))))))' ID: 3 => ('b(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))', D3, R4, P[1, 1], S{x7 -> b(x')}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))' ID: 4 => ('b(a(b(a(b(a(a(b(b(x')))))))))', D4, R5, P[1, 1, 1, 1, 1, 1, 1], S{x8 -> b(x')}), NR: 'b(b(x'))' ID: 5 => ('b(a(b(a(b(a(a(a(a(b(b(x')))))))))))', D5, R3, P[1, 1, 1, 1], S{x6 -> x'}), NR: 'b(a(a(a(a(b(b(x')))))))' ID: 6 => ('b(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))))', D6, R2, P[1, 1], S{x5 -> b(x')}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))' ID: 7 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))))))))))))))))))', D7, R2, P[], S{x5 -> a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))))))))))))))))))' ID: 8 => ('b(a(b(a(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))))', D7, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> b(x')}), NR: 'b(b(x'))' ID: 9 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))))))))))))', D8, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))}), NR: 'b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))' ID: 10 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))))))))))))))))))', D8, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> b(x')}), NR: 'b(b(x'))' ID: 11 => ('b(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'b(b(x'))' t: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(x'))))))))))))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12] Edges: [(0,1),(0,2),(1,3),(2,3),(3,4),(4,5),(5,6),(6,7),(7,8),(7,9),(8,10),(8,11),(9,11),(9,12)] ID: 0 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(x')))))))))))))))))))', D0) ID: 1 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))', D1, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'b(a(a(a(a(b(b(x')))))))' ID: 2 => ('b(a(b(a(a(b(a(a(b(b(x'))))))))))', D1, R5, P[1, 1, 1, 1, 1], S{x8 -> a(a(b(b(x'))))}), NR: 'b(a(a(b(b(x')))))' ID: 3 => ('b(a(b(a(a(b(a(a(a(a(b(b(x'))))))))))))', D2, R5, P[1, 1, 1, 1, 1], S{x8 -> a(a(a(a(b(b(x'))))))}), NR: 'b(a(a(a(a(b(b(x')))))))' ID: 4 => ('b(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))', D3, R4, P[1, 1], S{x7 -> b(x')}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))' ID: 5 => ('b(a(b(a(b(a(a(b(b(x')))))))))', D4, R5, P[1, 1, 1, 1, 1, 1, 1], S{x8 -> b(x')}), NR: 'b(b(x'))' ID: 6 => ('b(a(b(a(b(a(a(a(a(b(b(x')))))))))))', D5, R3, P[1, 1, 1, 1], S{x6 -> x'}), NR: 'b(a(a(a(a(b(b(x')))))))' ID: 7 => ('b(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))))', D6, R2, P[1, 1], S{x5 -> b(x')}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))' ID: 8 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))))))))))))))))))', D7, R2, P[], S{x5 -> a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))))))))))))))))))' ID: 9 => ('b(a(b(a(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))))', D7, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> b(x')}), NR: 'b(b(x'))' ID: 10 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))))))))))))', D8, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))}), NR: 'b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))' ID: 11 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))))))))))))))))))', D8, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> b(x')}), NR: 'b(b(x'))' ID: 12 => ('b(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'b(b(x'))' SNodesPath1: b(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))) TNodesPath1: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(x'))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))) SNodesPath2: b(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))) TNodesPath2: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(x'))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))) b(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))) ->= b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))) *<- b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(x'))))))))))))))))))) b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(x'))))))))))))))))))) ->= b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))) *<- b(a(a(b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.15: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N15 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(b(b(x')))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(a(b(b(x'))))', D0) ID: 1 => ('b(b(x'))', D1, R1, P[], S{x4 -> x'}), NR: 'b(b(x'))' t: b(b(a(a(a(b(a(a(a(a(b(x'))))))))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(b(a(a(a(b(a(a(a(a(b(x')))))))))))', D0) ID: 1 => ('b(b(x'))', D1, R5, P[1], S{x8 -> x'}), NR: 'b(x')' SNodesPath1: b(a(b(b(x')))) -> b(b(x')) TNodesPath1: b(b(a(a(a(b(a(a(a(a(b(x'))))))))))) -> b(b(x')) SNodesPath2: b(a(b(b(x')))) -> b(b(x')) TNodesPath2: b(b(a(a(a(b(a(a(a(a(b(x'))))))))))) -> b(b(x')) b(a(b(b(x')))) ->= b(b(x')) *<- b(b(a(a(a(b(a(a(a(a(b(x'))))))))))) b(b(a(a(a(b(a(a(a(a(b(x'))))))))))) ->= b(b(x')) *<- b(a(b(b(x')))) "Strongly closed critical pair" The problem is confluent. Problem 1.16: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N16 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))) Nodes: [0,1,2,3] Edges: [(0,1),(0,2),(1,3),(2,3)] ID: 0 => ('b(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))', D0) ID: 1 => ('b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))', D1, R1, P[], S{x4 -> a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))}), NR: 'b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))' ID: 2 => ('b(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(x'))))))))))))))))', D1, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 3 => ('b(b(a(a(a(a(b(a(a(a(a(b(a(b(x'))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' t: b(b(a(b(a(a(a(a(b(x'))))))))) Nodes: [0,1,2] Edges: [(0,1),(1,2)] ID: 0 => ('b(b(a(b(a(a(a(a(b(x')))))))))', D0) ID: 1 => ('b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))', D1, R2, P[1], S{x5 -> x'}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))' ID: 2 => ('b(b(a(a(a(a(b(a(a(a(a(b(a(b(x'))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' SNodesPath1: b(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))) -> b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) TNodesPath1: b(b(a(b(a(a(a(a(b(x'))))))))) -> b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) SNodesPath2: b(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))) -> b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) TNodesPath2: b(b(a(b(a(a(a(a(b(x'))))))))) -> b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) b(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))) ->= b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) *<- b(b(a(b(a(a(a(a(b(x'))))))))) b(b(a(b(a(a(a(a(b(x'))))))))) ->= b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))) *<- b(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.17: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N18 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(b(a(a(a(a(b(b(x'))))))))) Nodes: [0,1,2,3] Edges: [(0,1),(1,2),(2,3)] ID: 0 => ('b(a(b(a(a(a(a(b(b(x')))))))))', D0) ID: 1 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))', D1, R2, P[], S{x5 -> b(x')}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))' ID: 2 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> b(x')}), NR: 'b(b(x'))' ID: 3 => ('b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))', D3, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'b(b(x'))' t: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))))))))))))) Nodes: [0,1,2,3,4] Edges: [(0,1),(0,2),(1,3),(2,3),(3,4)] ID: 0 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(b(x')))))))))))))))))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))', D1, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'b(b(x'))' ID: 2 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(b(b(x'))))))))))))))))', D1, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(b(b(x')))}), NR: 'b(a(b(b(x'))))' ID: 3 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> b(x')}), NR: 'b(b(x'))' ID: 4 => ('b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))', D3, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'b(b(x'))' SNodesPath1: b(a(b(a(a(a(a(b(b(x'))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))))) TNodesPath1: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))))) SNodesPath2: b(a(b(a(a(a(a(b(b(x'))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))))) TNodesPath2: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))))) b(a(b(a(a(a(a(b(b(x'))))))))) ->= b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))))) *<- b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))))))))))))) b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))))))))))))) ->= b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))))))))) *<- b(a(b(a(a(a(a(b(b(x'))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.18: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N19 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(b(a(a(a(a(b(x'))))))))) Nodes: [0,1,2] Edges: [(0,1),(1,2)] ID: 0 => ('b(a(a(b(a(a(a(a(b(x')))))))))', D0) ID: 1 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))', D1, R4, P[], S{x7 -> x'}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))' ID: 2 => ('b(a(b(a(a(b(x'))))))', D2, R5, P[1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' t: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))) Nodes: [0,1,2] Edges: [(0,1),(0,1),(1,2)] ID: 0 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))', D0) ID: 1 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))', D1, R5, P[1, 1, 1, 1, 1], S{x8 -> a(a(a(b(a(a(a(a(b(x')))))))))}), NR: 'b(a(a(a(b(a(a(a(a(b(x'))))))))))' ID: 2 => ('b(a(b(a(a(b(x'))))))', D2, R5, P[1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' SNodesPath1: b(a(a(b(a(a(a(a(b(x'))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))) TNodesPath1: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))) SNodesPath2: b(a(a(b(a(a(a(a(b(x'))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))) TNodesPath2: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))) b(a(a(b(a(a(a(a(b(x'))))))))) ->= b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))) *<- b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))) b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))) ->= b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))) *<- b(a(a(b(a(a(a(a(b(x'))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.19: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N20 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(b(b(x'))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(a(a(b(b(x')))))', D0) ID: 1 => ('b(a(a(a(a(b(b(x')))))))', D1, R3, P[], S{x6 -> x'}), NR: 'b(a(a(a(a(b(b(x')))))))' t: b(a(a(a(a(b(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(a(a(a(a(b(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(b(x')))))))', D1, R5, P[1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' SNodesPath1: b(a(a(b(b(x'))))) -> b(a(a(a(a(b(b(x'))))))) TNodesPath1: b(a(a(a(a(b(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) -> b(a(a(a(a(b(b(x'))))))) SNodesPath2: b(a(a(b(b(x'))))) -> b(a(a(a(a(b(b(x'))))))) TNodesPath2: b(a(a(a(a(b(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) -> b(a(a(a(a(b(b(x'))))))) b(a(a(b(b(x'))))) ->= b(a(a(a(a(b(b(x'))))))) *<- b(a(a(a(a(b(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) b(a(a(a(a(b(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))) ->= b(a(a(a(a(b(b(x'))))))) *<- b(a(a(b(b(x'))))) "Strongly closed critical pair" The problem is confluent. Problem 1.20: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N21 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(b(b(a(a(a(a(b(b(x'))))))))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(a(a(b(b(a(a(a(a(b(b(x')))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(b(a(a(a(a(b(b(x')))))))))))))', D1, R3, P[], S{x6 -> a(a(a(a(b(b(x'))))))}), NR: 'b(a(a(a(a(b(b(a(a(a(a(b(b(x')))))))))))))' t: b(a(a(a(a(b(b(a(a(b(b(x'))))))))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(a(a(a(a(b(b(a(a(b(b(x')))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(b(a(a(a(a(b(b(x')))))))))))))', D1, R3, P[1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'b(a(a(a(a(b(b(x')))))))' SNodesPath1: b(a(a(b(b(a(a(a(a(b(b(x'))))))))))) -> b(a(a(a(a(b(b(a(a(a(a(b(b(x'))))))))))))) TNodesPath1: b(a(a(a(a(b(b(a(a(b(b(x'))))))))))) -> b(a(a(a(a(b(b(a(a(a(a(b(b(x'))))))))))))) SNodesPath2: b(a(a(b(b(a(a(a(a(b(b(x'))))))))))) -> b(a(a(a(a(b(b(a(a(a(a(b(b(x'))))))))))))) TNodesPath2: b(a(a(a(a(b(b(a(a(b(b(x'))))))))))) -> b(a(a(a(a(b(b(a(a(a(a(b(b(x'))))))))))))) b(a(a(b(b(a(a(a(a(b(b(x'))))))))))) ->= b(a(a(a(a(b(b(a(a(a(a(b(b(x'))))))))))))) *<- b(a(a(a(a(b(b(a(a(b(b(x'))))))))))) b(a(a(a(a(b(b(a(a(b(b(x'))))))))))) ->= b(a(a(a(a(b(b(a(a(a(a(b(b(x'))))))))))))) *<- b(a(a(b(b(a(a(a(a(b(b(x'))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.21: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N22 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(b(a(a(a(a(b(b(x')))))))))) Nodes: [0,1,2,3,4,5,6] Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(5,6)] ID: 0 => ('b(a(a(b(a(a(a(a(b(b(x'))))))))))', D0) ID: 1 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))', D1, R4, P[], S{x7 -> b(x')}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))' ID: 2 => ('b(a(b(a(a(b(b(x')))))))', D2, R5, P[1, 1, 1, 1, 1], S{x8 -> b(x')}), NR: 'b(b(x'))' ID: 3 => ('b(a(b(a(a(a(a(b(b(x')))))))))', D3, R3, P[1, 1], S{x6 -> x'}), NR: 'b(a(a(a(a(b(b(x')))))))' ID: 4 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))', D4, R2, P[], S{x5 -> b(x')}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))' ID: 5 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))', D5, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> b(x')}), NR: 'b(b(x'))' ID: 6 => ('b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'b(b(x'))' t: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(b(x')))))))))))))))))) Nodes: [0,1,2,3,4,5,6,7] Edges: [(0,1),(0,2),(1,3),(2,3),(3,4),(4,5),(5,6),(6,7)] ID: 0 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))))))', D0) ID: 1 => ('b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(b(x'))))))))))))))))', D1, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'b(b(x'))' ID: 2 => ('b(a(b(a(a(b(a(b(b(x')))))))))', D1, R5, P[1, 1, 1, 1, 1], S{x8 -> a(b(b(x')))}), NR: 'b(a(b(b(x'))))' ID: 3 => ('b(a(b(a(a(b(b(x')))))))', D2, R5, P[1, 1, 1, 1, 1], S{x8 -> b(x')}), NR: 'b(b(x'))' ID: 4 => ('b(a(b(a(a(a(a(b(b(x')))))))))', D3, R3, P[1, 1], S{x6 -> x'}), NR: 'b(a(a(a(a(b(b(x')))))))' ID: 5 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))', D4, R2, P[], S{x5 -> b(x')}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))))))))))' ID: 6 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(b(x'))))))))))))))', D5, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> b(x')}), NR: 'b(b(x'))' ID: 7 => ('b(a(a(a(a(b(a(a(a(a(b(b(x'))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'b(b(x'))' SNodesPath1: b(a(a(b(a(a(a(a(b(b(x')))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))) TNodesPath1: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(b(x')))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))) SNodesPath2: b(a(a(b(a(a(a(a(b(b(x')))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))) TNodesPath2: b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(b(x')))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))) b(a(a(b(a(a(a(a(b(b(x')))))))))) ->= b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))) *<- b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(b(x')))))))))))))))))) b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(b(x')))))))))))))))))) ->= b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(b(x')))))))))))))))) *<- b(a(a(b(a(a(a(a(b(b(x')))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.22: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N23 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))) Nodes: [0,1,2,3] Edges: [(0,1),(0,2),(1,3),(2,3)] ID: 0 => ('b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))', D1, R3, P[], S{x6 -> a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))}), NR: 'b(a(a(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))' ID: 2 => ('b(a(a(b(b(a(b(a(a(b(x'))))))))))', D1, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' ID: 3 => ('b(a(a(a(a(b(b(a(b(a(a(b(x'))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' t: b(a(a(a(a(b(b(a(a(b(a(a(a(a(b(x'))))))))))))))) Nodes: [0,1,2] Edges: [(0,1),(1,2)] ID: 0 => ('b(a(a(a(a(b(b(a(a(b(a(a(a(a(b(x')))))))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))', D1, R4, P[1, 1, 1, 1, 1, 1], S{x7 -> x'}), NR: 'b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))' ID: 2 => ('b(a(a(a(a(b(b(a(b(a(a(b(x'))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' SNodesPath1: b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))) -> b(a(a(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))) TNodesPath1: b(a(a(a(a(b(b(a(a(b(a(a(a(a(b(x'))))))))))))))) -> b(a(a(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))) SNodesPath2: b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))) -> b(a(a(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))) TNodesPath2: b(a(a(a(a(b(b(a(a(b(a(a(a(a(b(x'))))))))))))))) -> b(a(a(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))) b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))) ->= b(a(a(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))) *<- b(a(a(a(a(b(b(a(a(b(a(a(a(a(b(x'))))))))))))))) b(a(a(a(a(b(b(a(a(b(a(a(a(a(b(x'))))))))))))))) ->= b(a(a(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))) *<- b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.23: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N24 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(b(a(a(a(a(b(x')))))))) Nodes: [0,1,2] Edges: [(0,1),(1,2)] ID: 0 => ('b(a(b(a(a(a(a(b(x'))))))))', D0) ID: 1 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))', D1, R2, P[], S{x5 -> x'}), NR: 'b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))' ID: 2 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' t: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))) Nodes: [0,1,2] Edges: [(0,1),(0,1),(1,2)] ID: 0 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))))))))))))', D0) ID: 1 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))', D1, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> a(a(a(b(a(a(a(a(b(x')))))))))}), NR: 'b(a(a(a(b(a(a(a(a(b(x'))))))))))' ID: 2 => ('b(a(a(a(a(b(a(a(a(a(b(a(b(x')))))))))))))', D2, R5, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x8 -> x'}), NR: 'b(x')' SNodesPath1: b(a(b(a(a(a(a(b(x')))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) TNodesPath1: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) SNodesPath2: b(a(b(a(a(a(a(b(x')))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) TNodesPath2: b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) b(a(b(a(a(a(a(b(x')))))))) ->= b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) *<- b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))) b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(x'))))))))))))))))))))))))))))))) ->= b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x')))))))))))))))))))))) *<- b(a(b(a(a(a(a(b(x')))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.24: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N25 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(a(b(a(a(a(a(b(b(x'))))))))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(a(a(a(b(a(a(a(a(b(b(x')))))))))))', D0) ID: 1 => ('b(b(x'))', D1, R5, P[], S{x8 -> b(x')}), NR: 'b(b(x'))' t: b(a(b(b(x')))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('b(a(b(b(x'))))', D0) ID: 1 => ('b(b(x'))', D1, R1, P[], S{x4 -> x'}), NR: 'b(b(x'))' SNodesPath1: b(a(a(a(b(a(a(a(a(b(b(x'))))))))))) -> b(b(x')) TNodesPath1: b(a(b(b(x')))) -> b(b(x')) SNodesPath2: b(a(a(a(b(a(a(a(a(b(b(x'))))))))))) -> b(b(x')) TNodesPath2: b(a(b(b(x')))) -> b(b(x')) b(a(a(a(b(a(a(a(a(b(b(x'))))))))))) ->= b(b(x')) *<- b(a(b(b(x')))) b(a(b(b(x')))) ->= b(b(x')) *<- b(a(a(a(b(a(a(a(a(b(b(x'))))))))))) "Strongly closed critical pair" The problem is confluent.