YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (b 1) (w 1) (fSNonEmpty) ) (RULES b(b(x)) -> w(w(w(w(x)))) b(w(x)) -> w(w(w(b(x)))) w(b(x)) -> b(x) w(w(x)) -> w(x) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: Termination Procedure: Terminating? YES Problem 1: (VAR vu95NonEmpty vNonEmpty x) (RULES b(b(x)) -> w(w(w(w(x)))) b(w(x)) -> w(w(w(b(x)))) w(b(x)) -> b(x) w(w(x)) -> w(x) ) Problem 1: Dependency Pairs Processor: -> Pairs: B(b(x)) -> W(w(w(w(x)))) B(b(x)) -> W(w(w(x))) B(b(x)) -> W(w(x)) B(b(x)) -> W(x) B(w(x)) -> B(x) B(w(x)) -> W(b(x)) B(w(x)) -> W(w(b(x))) B(w(x)) -> W(w(w(b(x)))) -> Rules: b(b(x)) -> w(w(w(w(x)))) b(w(x)) -> w(w(w(b(x)))) w(b(x)) -> b(x) w(w(x)) -> w(x) Problem 1: SCC Processor: -> Pairs: B(b(x)) -> W(w(w(w(x)))) B(b(x)) -> W(w(w(x))) B(b(x)) -> W(w(x)) B(b(x)) -> W(x) B(w(x)) -> B(x) B(w(x)) -> W(b(x)) B(w(x)) -> W(w(b(x))) B(w(x)) -> W(w(w(b(x)))) -> Rules: b(b(x)) -> w(w(w(w(x)))) b(w(x)) -> w(w(w(b(x)))) w(b(x)) -> b(x) w(w(x)) -> w(x) ->Strongly Connected Components: ->->Cycle: ->->-> Pairs: B(w(x)) -> B(x) ->->-> Rules: b(b(x)) -> w(w(w(w(x)))) b(w(x)) -> w(w(w(b(x)))) w(b(x)) -> b(x) w(w(x)) -> w(x) Problem 1: Subterm Processor: -> Pairs: B(w(x)) -> B(x) -> Rules: b(b(x)) -> w(w(w(w(x)))) b(w(x)) -> w(w(w(b(x)))) w(b(x)) -> b(x) w(w(x)) -> w(x) ->Projection: pi(B) = 1 Problem 1: SCC Processor: -> Pairs: Empty -> Rules: b(b(x)) -> w(w(w(w(x)))) b(w(x)) -> w(w(w(b(x)))) w(b(x)) -> b(x) w(w(x)) -> w(x) ->Strongly Connected Components: There is no strongly connected component The problem is finite. Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (b 1) (w 1) (fSNonEmpty) ) (RULES b(b(x)) -> w(w(w(w(x)))) b(w(x)) -> w(w(w(b(x)))) w(b(x)) -> b(x) w(w(x)) -> w(x) ) Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy NW Procedure: -> Rules: b(b(x)) -> w(w(w(w(x)))) b(w(x)) -> w(w(w(b(x)))) w(b(x)) -> b(x) w(w(x)) -> w(x) -> Vars: x, x, x, x -> Rlps: (rule: b(b(x)) -> w(w(w(w(x)))), id: 1, possubterms: b(b(x))->[], b(x)->[1]) (rule: b(w(x)) -> w(w(w(b(x)))), id: 2, possubterms: b(w(x))->[], w(x)->[1]) (rule: w(b(x)) -> b(x), id: 3, possubterms: w(b(x))->[], b(x)->[1]) (rule: w(w(x)) -> w(x), id: 4, possubterms: w(w(x))->[], w(x)->[1]) -> Unifications: (R1 unifies with R1 at p: [1], l: b(b(x)), lp: b(x), sig: {x -> b(x')}, l': b(b(x')), r: w(w(w(w(x)))), r': w(w(w(w(x'))))) (R1 unifies with R2 at p: [1], l: b(b(x)), lp: b(x), sig: {x -> w(x')}, l': b(w(x')), r: w(w(w(w(x)))), r': w(w(w(b(x'))))) (R2 unifies with R3 at p: [1], l: b(w(x)), lp: w(x), sig: {x -> b(x')}, l': w(b(x')), r: w(w(w(b(x)))), r': b(x')) (R2 unifies with R4 at p: [1], l: b(w(x)), lp: w(x), sig: {x -> w(x')}, l': w(w(x')), r: w(w(w(b(x)))), r': w(x')) (R3 unifies with R1 at p: [1], l: w(b(x)), lp: b(x), sig: {x -> b(x')}, l': b(b(x')), r: b(x), r': w(w(w(w(x'))))) (R3 unifies with R2 at p: [1], l: w(b(x)), lp: b(x), sig: {x -> w(x')}, l': b(w(x')), r: b(x), r': w(w(w(b(x'))))) (R4 unifies with R3 at p: [1], l: w(w(x)), lp: w(x), sig: {x -> b(x')}, l': w(b(x')), r: w(x), r': b(x')) (R4 unifies with R4 at p: [1], l: w(w(x)), lp: w(x), sig: {x -> w(x')}, l': w(w(x')), r: w(x), r': w(x')) -> Critical pairs info: => Not trivial, Not overlay, Proper, NW0, N1 => Not trivial, Not overlay, Proper, NW0, N2 => Trivial, Not overlay, Proper, NW0, N3 => Not trivial, Not overlay, Proper, NW0, N4 => 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 -> 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 6 subproblems. Problem 1.1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (w 1) (fSNonEmpty) ) (RULES b(b(x)) -> w(w(w(w(x)))) b(w(x)) -> w(w(w(b(x)))) w(b(x)) -> b(x) w(w(x)) -> w(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N1 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: w(w(w(w(b(x'))))) Nodes: [0,1,2,3,4] Edges: [(0,1),(0,1),(0,1),(0,1),(1,2),(1,2),(1,2),(2,3),(2,3),(3,4)] ID: 0 => ('w(w(w(w(b(x')))))', D0) ID: 1 => ('w(w(w(b(x'))))', D1, R3, P[1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 2 => ('w(w(b(x')))', D2, R3, P[1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 3 => ('w(b(x'))', D3, R3, P[1], S{x6 -> x'}), NR: 'b(x')' ID: 4 => ('b(x')', D4, R3, P[], S{x6 -> x'}), NR: 'b(x')' t: b(w(x')) Nodes: [0,1,2,3,4] Edges: [(0,1),(1,2),(1,2),(1,2),(2,3),(2,3),(3,4)] ID: 0 => ('b(w(x'))', D0) ID: 1 => ('w(w(w(b(x'))))', D1, R2, P[], S{x5 -> x'}), NR: 'w(w(w(b(x'))))' ID: 2 => ('w(w(b(x')))', D2, R3, P[1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 3 => ('w(b(x'))', D3, R3, P[1], S{x6 -> x'}), NR: 'b(x')' ID: 4 => ('b(x')', D4, R3, P[], S{x6 -> x'}), NR: 'b(x')' SNodesPath: w(w(w(w(b(x'))))) -> w(w(w(b(x')))) TNodesPath: b(w(x')) -> w(w(w(b(x')))) w(w(w(w(b(x'))))) ->* w(w(w(b(x')))) *<- b(w(x')) "Joinable" The problem is confluent. Problem 1.2: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (w 1) (fSNonEmpty) ) (RULES b(b(x)) -> w(w(w(w(x)))) b(w(x)) -> w(w(w(b(x)))) w(b(x)) -> b(x) w(w(x)) -> w(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N2 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b(w(w(w(w(x'))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34] Edges: [(0,1),(0,2),(0,2),(0,2),(1,3),(1,4),(1,4),(1,4),(1,5),(1,5),(2,5),(2,6),(2,6),(3,7),(3,8),(3,8),(3,8),(3,8),(3,8),(3,8),(3,9),(4,8),(4,10),(4,10),(4,11),(4,11),(5,9),(5,11),(5,11),(5,11),(5,12),(6,12),(6,13),(7,14),(7,15),(7,15),(7,15),(7,15),(7,15),(7,15),(7,15),(7,15),(7,15),(8,15),(8,16),(8,16),(8,16),(8,16),(8,16),(8,17),(9,17),(9,17),(9,17),(9,17),(9,17),(9,17),(9,18),(10,2),(10,16),(10,19),(10,19),(11,17),(11,19),(11,19),(11,20),(12,20),(12,20),(12,20),(12,21),(13,22),(14,23),(14,23),(14,23),(14,23),(14,23),(14,23),(14,23),(14,23),(14,23),(14,23),(14,23),(14,23),(15,23),(15,24),(15,24),(15,24),(15,24),(15,24),(15,24),(15,24),(15,24),(16,5),(16,5),(16,5),(16,5),(16,24),(16,25),(17,25),(17,25),(17,25),(17,25),(17,25),(17,26),(18,26),(18,26),(18,26),(18,26),(18,26),(18,26),(18,26),(18,26),(18,26),(19,6),(19,25),(19,27),(20,27),(20,27),(20,28),(21,28),(21,28),(21,28),(21,28),(21,28),(21,28),(22,29),(22,29),(22,29),(23,30),(23,30),(23,30),(23,30),(23,30),(23,30),(23,30),(23,30),(23,30),(23,30),(23,30),(24,9),(24,9),(24,9),(24,9),(24,9),(24,9),(24,9),(24,30),(25,12),(25,12),(25,12),(25,12),(25,31),(26,31),(26,31),(26,31),(26,31),(26,31),(26,31),(26,31),(26,31),(27,13),(27,32),(28,32),(28,32),(28,32),(28,32),(28,32),(29,33),(29,33),(30,18),(30,18),(30,18),(30,18),(30,18),(30,18),(30,18),(30,18),(30,18),(30,18),(31,21),(31,21),(31,21),(31,21),(31,21),(31,21),(31,21),(32,22),(32,22),(32,22),(32,22),(33,34)] ID: 0 => ('b(w(w(w(w(x')))))', D0) ID: 1 => ('w(w(w(b(w(w(w(x')))))))', D1, R2, P[], S{x5 -> w(w(w(x')))}), NR: 'w(w(w(b(w(w(w(x')))))))' ID: 2 => ('b(w(w(w(x'))))', D1, R4, P[1], S{x7 -> w(w(x'))}), NR: 'w(w(w(x')))' ID: 3 => ('w(w(w(w(w(w(b(w(w(x')))))))))', D2, R2, P[1, 1, 1], S{x5 -> w(w(x'))}), NR: 'w(w(w(b(w(w(x'))))))' ID: 4 => ('w(w(b(w(w(w(x'))))))', D2, R3, P[1, 1], S{x6 -> w(w(w(x')))}), NR: 'b(w(w(w(x'))))' ID: 5 => ('w(w(w(b(w(w(x'))))))', D2, R4, P[1, 1, 1, 1], S{x7 -> w(x')}), NR: 'w(w(x'))' ID: 6 => ('b(w(w(x')))', D2, R4, P[1], S{x7 -> w(x')}), NR: 'w(w(x'))' ID: 7 => ('w(w(w(w(w(w(w(w(w(b(w(x')))))))))))', D3, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> w(x')}), NR: 'w(w(w(b(w(x')))))' ID: 8 => ('w(w(w(w(w(b(w(w(x'))))))))', D3, R3, P[1, 1, 1, 1, 1], S{x6 -> w(w(x'))}), NR: 'b(w(w(x')))' ID: 9 => ('w(w(w(w(w(w(b(w(x'))))))))', D3, R4, P[1, 1, 1, 1, 1, 1, 1], S{x7 -> x'}), NR: 'w(x')' ID: 10 => ('w(b(w(w(w(x')))))', D3, R3, P[1], S{x6 -> w(w(w(x')))}), NR: 'b(w(w(w(x'))))' ID: 11 => ('w(w(b(w(w(x')))))', D3, R4, P[1, 1, 1], S{x7 -> w(x')}), NR: 'w(w(x'))' ID: 12 => ('w(w(w(b(w(x')))))', D3, R4, P[1, 1, 1, 1], S{x7 -> x'}), NR: 'w(x')' ID: 13 => ('b(w(x'))', D3, R4, P[1], S{x7 -> x'}), NR: 'w(x')' ID: 14 => ('w(w(w(w(w(w(w(w(w(w(w(w(b(x')))))))))))))', D4, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'w(w(w(b(x'))))' ID: 15 => ('w(w(w(w(w(w(w(w(b(w(x'))))))))))', D4, R3, P[1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> w(x')}), NR: 'b(w(x'))' ID: 16 => ('w(w(w(w(b(w(w(x')))))))', D4, R3, P[1, 1, 1, 1], S{x6 -> w(w(x'))}), NR: 'b(w(w(x')))' ID: 17 => ('w(w(w(w(w(b(w(x')))))))', D4, R4, P[1, 1, 1, 1, 1, 1], S{x7 -> x'}), NR: 'w(x')' ID: 18 => ('w(w(w(w(w(w(w(w(w(b(x'))))))))))', D4, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'w(w(w(b(x'))))' ID: 19 => ('w(b(w(w(x'))))', D4, R4, P[1, 1], S{x7 -> w(x')}), NR: 'w(w(x'))' ID: 20 => ('w(w(b(w(x'))))', D4, R4, P[1, 1, 1], S{x7 -> x'}), NR: 'w(x')' ID: 21 => ('w(w(w(w(w(w(b(x')))))))', D4, R2, P[1, 1, 1], S{x5 -> x'}), NR: 'w(w(w(b(x'))))' ID: 22 => ('w(w(w(b(x'))))', D4, R2, P[], S{x5 -> x'}), NR: 'w(w(w(b(x'))))' ID: 23 => ('w(w(w(w(w(w(w(w(w(w(w(b(x'))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 24 => ('w(w(w(w(w(w(w(b(w(x')))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1], S{x6 -> w(x')}), NR: 'b(w(x'))' ID: 25 => ('w(w(w(w(b(w(x'))))))', D5, R4, P[1, 1, 1, 1, 1], S{x7 -> x'}), NR: 'w(x')' ID: 26 => ('w(w(w(w(w(w(w(w(b(x')))))))))', D5, R2, P[1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'w(w(w(b(x'))))' ID: 27 => ('w(b(w(x')))', D5, R4, P[1, 1], S{x7 -> x'}), NR: 'w(x')' ID: 28 => ('w(w(w(w(w(b(x'))))))', D5, R2, P[1, 1], S{x5 -> x'}), NR: 'w(w(w(b(x'))))' ID: 29 => ('w(w(b(x')))', D5, R3, P[1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 30 => ('w(w(w(w(w(w(w(w(w(w(b(x')))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 31 => ('w(w(w(w(w(w(w(b(x'))))))))', D6, R2, P[1, 1, 1, 1], S{x5 -> x'}), NR: 'w(w(w(b(x'))))' ID: 32 => ('w(w(w(w(b(x')))))', D6, R2, P[1], S{x5 -> x'}), NR: 'w(w(w(b(x'))))' ID: 33 => ('w(b(x'))', D6, R3, P[1], S{x6 -> x'}), NR: 'b(x')' ID: 34 => ('b(x')', D7, R3, P[], S{x6 -> x'}), NR: 'b(x')' t: w(w(w(w(b(x'))))) Nodes: [0,1,2,3,4] Edges: [(0,1),(0,1),(0,1),(0,1),(1,2),(1,2),(1,2),(2,3),(2,3),(3,4)] ID: 0 => ('w(w(w(w(b(x')))))', D0) ID: 1 => ('w(w(w(b(x'))))', D1, R3, P[1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 2 => ('w(w(b(x')))', D2, R3, P[1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 3 => ('w(b(x'))', D3, R3, P[1], S{x6 -> x'}), NR: 'b(x')' ID: 4 => ('b(x')', D4, R3, P[], S{x6 -> x'}), NR: 'b(x')' SNodesPath: b(w(w(w(w(x'))))) -> w(w(w(b(w(w(w(x'))))))) -> w(w(w(w(w(w(b(w(w(x'))))))))) -> w(w(w(w(w(w(w(w(w(b(w(x'))))))))))) -> w(w(w(w(w(w(w(w(w(w(w(w(b(x'))))))))))))) -> w(w(w(w(w(w(w(w(w(w(w(b(x')))))))))))) -> w(w(w(w(w(w(w(w(w(w(b(x'))))))))))) -> w(w(w(w(w(w(w(w(w(b(x')))))))))) -> w(w(w(w(w(w(w(w(b(x'))))))))) -> w(w(w(w(w(w(w(b(x')))))))) -> w(w(w(w(w(w(b(x'))))))) -> w(w(w(w(w(b(x')))))) -> w(w(w(w(b(x'))))) -> w(w(w(b(x')))) TNodesPath: w(w(w(w(b(x'))))) -> w(w(w(b(x')))) b(w(w(w(w(x'))))) ->* w(w(w(b(x')))) *<- w(w(w(w(b(x'))))) "Joinable" The problem is confluent. Problem 1.3: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (w 1) (fSNonEmpty) ) (RULES b(b(x)) -> w(w(w(w(x)))) b(w(x)) -> w(w(w(b(x)))) w(b(x)) -> b(x) w(w(x)) -> w(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N4 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b(w(x')) Nodes: [0,1,2,3,4] Edges: [(0,1),(1,2),(1,2),(1,2),(2,3),(2,3),(3,4)] ID: 0 => ('b(w(x'))', D0) ID: 1 => ('w(w(w(b(x'))))', D1, R2, P[], S{x5 -> x'}), NR: 'w(w(w(b(x'))))' ID: 2 => ('w(w(b(x')))', D2, R3, P[1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 3 => ('w(b(x'))', D3, R3, P[1], S{x6 -> x'}), NR: 'b(x')' ID: 4 => ('b(x')', D4, R3, P[], S{x6 -> x'}), NR: 'b(x')' t: w(w(w(b(w(x'))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10] Edges: [(0,1),(0,2),(0,2),(0,2),(1,3),(1,3),(1,3),(1,3),(1,3),(1,3),(2,3),(2,4),(2,4),(3,5),(3,5),(3,5),(3,5),(3,5),(4,5),(4,6),(5,7),(5,7),(5,7),(5,7),(6,7),(7,8),(7,8),(7,8),(8,9),(8,9),(9,10)] ID: 0 => ('w(w(w(b(w(x')))))', D0) ID: 1 => ('w(w(w(w(w(w(b(x')))))))', D1, R2, P[1, 1, 1], S{x5 -> x'}), NR: 'w(w(w(b(x'))))' ID: 2 => ('w(w(b(w(x'))))', D1, R3, P[1, 1], S{x6 -> w(x')}), NR: 'b(w(x'))' ID: 3 => ('w(w(w(w(w(b(x'))))))', D2, R3, P[1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 4 => ('w(b(w(x')))', D2, R3, P[1], S{x6 -> w(x')}), NR: 'b(w(x'))' ID: 5 => ('w(w(w(w(b(x')))))', D3, R3, P[1, 1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 6 => ('b(w(x'))', D3, R3, P[], S{x6 -> w(x')}), NR: 'b(w(x'))' ID: 7 => ('w(w(w(b(x'))))', D4, R3, P[1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 8 => ('w(w(b(x')))', D5, R3, P[1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 9 => ('w(b(x'))', D6, R3, P[1], S{x6 -> x'}), NR: 'b(x')' ID: 10 => ('b(x')', D7, R3, P[], S{x6 -> x'}), NR: 'b(x')' SNodesPath: b(w(x')) TNodesPath: b(w(x')) ->* b(w(x')) *<- w(w(w(b(w(x'))))) "Joinable" The problem is confluent. Problem 1.4: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (w 1) (fSNonEmpty) ) (RULES b(b(x)) -> w(w(w(w(x)))) b(w(x)) -> w(w(w(b(x)))) w(b(x)) -> b(x) w(w(x)) -> w(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N6 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b(w(w(w(b(x'))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34] Edges: [(0,1),(0,2),(0,2),(0,2),(1,3),(1,4),(1,4),(1,4),(1,5),(1,5),(2,5),(2,6),(2,6),(3,7),(3,8),(3,8),(3,8),(3,8),(3,8),(3,8),(3,9),(4,8),(4,10),(4,10),(4,11),(4,11),(5,9),(5,11),(5,11),(5,11),(5,12),(6,12),(6,13),(7,14),(7,15),(7,15),(7,15),(7,15),(7,15),(7,15),(7,15),(7,15),(7,15),(8,15),(8,16),(8,16),(8,16),(8,16),(8,16),(8,17),(9,17),(9,17),(9,17),(9,17),(9,17),(9,17),(9,18),(10,2),(10,16),(10,19),(10,19),(11,17),(11,19),(11,19),(11,20),(12,20),(12,20),(12,20),(12,21),(13,22),(14,23),(14,23),(14,23),(14,23),(14,23),(14,23),(14,23),(14,23),(14,23),(14,23),(14,23),(14,23),(15,23),(15,24),(15,24),(15,24),(15,24),(15,24),(15,24),(15,24),(15,24),(16,5),(16,5),(16,5),(16,5),(16,24),(16,25),(17,25),(17,25),(17,25),(17,25),(17,25),(17,26),(18,26),(18,26),(18,26),(18,26),(18,26),(18,26),(18,26),(18,26),(18,26),(19,6),(19,25),(19,27),(20,27),(20,27),(20,28),(21,28),(21,28),(21,28),(21,28),(21,28),(21,28),(22,29),(22,29),(22,29),(23,30),(23,30),(23,30),(23,30),(23,30),(23,30),(23,30),(23,30),(23,30),(23,30),(23,30),(24,9),(24,9),(24,9),(24,9),(24,9),(24,9),(24,9),(24,30),(25,12),(25,12),(25,12),(25,12),(25,31),(26,31),(26,31),(26,31),(26,31),(26,31),(26,31),(26,31),(26,31),(27,13),(27,32),(28,32),(28,32),(28,32),(28,32),(28,32),(29,33),(29,33),(30,18),(30,18),(30,18),(30,18),(30,18),(30,18),(30,18),(30,18),(30,18),(30,18),(31,21),(31,21),(31,21),(31,21),(31,21),(31,21),(31,21),(32,22),(32,22),(32,22),(32,22),(33,34)] ID: 0 => ('b(w(w(w(b(x')))))', D0) ID: 1 => ('w(w(w(b(w(w(b(x')))))))', D1, R2, P[], S{x5 -> w(w(b(x')))}), NR: 'w(w(w(b(w(w(b(x')))))))' ID: 2 => ('b(w(w(b(x'))))', D1, R3, P[1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 3 => ('w(w(w(w(w(w(b(w(b(x')))))))))', D2, R2, P[1, 1, 1], S{x5 -> w(b(x'))}), NR: 'w(w(w(b(w(b(x'))))))' ID: 4 => ('w(w(b(w(w(b(x'))))))', D2, R3, P[1, 1], S{x6 -> w(w(b(x')))}), NR: 'b(w(w(b(x'))))' ID: 5 => ('w(w(w(b(w(b(x'))))))', D2, R3, P[1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 6 => ('b(w(b(x')))', D2, R3, P[1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 7 => ('w(w(w(w(w(w(w(w(w(b(b(x')))))))))))', D3, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> b(x')}), NR: 'w(w(w(b(b(x')))))' ID: 8 => ('w(w(w(w(w(b(w(b(x'))))))))', D3, R3, P[1, 1, 1, 1, 1], S{x6 -> w(b(x'))}), NR: 'b(w(b(x')))' ID: 9 => ('w(w(w(w(w(w(b(b(x'))))))))', D3, R3, P[1, 1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 10 => ('w(b(w(w(b(x')))))', D3, R3, P[1], S{x6 -> w(w(b(x')))}), NR: 'b(w(w(b(x'))))' ID: 11 => ('w(w(b(w(b(x')))))', D3, R3, P[1, 1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 12 => ('w(w(w(b(b(x')))))', D3, R3, P[1, 1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 13 => ('b(b(x'))', D3, R3, P[1], S{x6 -> x'}), NR: 'b(x')' ID: 14 => ('w(w(w(w(w(w(w(w(w(w(w(w(w(x')))))))))))))', D4, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'w(w(w(w(x'))))' ID: 15 => ('w(w(w(w(w(w(w(w(b(b(x'))))))))))', D4, R3, P[1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> b(x')}), NR: 'b(b(x'))' ID: 16 => ('w(w(w(w(b(w(b(x')))))))', D4, R3, P[1, 1, 1, 1], S{x6 -> w(b(x'))}), NR: 'b(w(b(x')))' ID: 17 => ('w(w(w(w(w(b(b(x')))))))', D4, R3, P[1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 18 => ('w(w(w(w(w(w(w(w(w(w(x'))))))))))', D4, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'w(w(w(w(x'))))' ID: 19 => ('w(b(w(b(x'))))', D4, R3, P[1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 20 => ('w(w(b(b(x'))))', D4, R3, P[1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 21 => ('w(w(w(w(w(w(w(x')))))))', D4, R1, P[1, 1, 1], S{x4 -> x'}), NR: 'w(w(w(w(x'))))' ID: 22 => ('w(w(w(w(x'))))', D4, R1, P[], S{x4 -> x'}), NR: 'w(w(w(w(x'))))' ID: 23 => ('w(w(w(w(w(w(w(w(w(w(w(w(x'))))))))))))', D5, R4, P[], S{x7 -> w(w(w(w(w(w(w(w(w(w(w(x')))))))))))}), NR: 'w(w(w(w(w(w(w(w(w(w(w(w(x'))))))))))))' ID: 24 => ('w(w(w(w(w(w(w(b(b(x')))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1], S{x6 -> b(x')}), NR: 'b(b(x'))' ID: 25 => ('w(w(w(w(b(b(x'))))))', D5, R3, P[1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 26 => ('w(w(w(w(w(w(w(w(w(x')))))))))', D5, R1, P[1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'w(w(w(w(x'))))' ID: 27 => ('w(b(b(x')))', D5, R3, P[1, 1], S{x6 -> x'}), NR: 'b(x')' ID: 28 => ('w(w(w(w(w(w(x'))))))', D5, R1, P[1, 1], S{x4 -> x'}), NR: 'w(w(w(w(x'))))' ID: 29 => ('w(w(w(x')))', D5, R4, P[], S{x7 -> w(w(x'))}), NR: 'w(w(w(x')))' ID: 30 => ('w(w(w(w(w(w(w(w(w(w(w(x')))))))))))', D6, R4, P[], S{x7 -> w(w(w(w(w(w(w(w(w(w(x'))))))))))}), NR: 'w(w(w(w(w(w(w(w(w(w(w(x')))))))))))' ID: 31 => ('w(w(w(w(w(w(w(w(x'))))))))', D6, R1, P[1, 1, 1, 1], S{x4 -> x'}), NR: 'w(w(w(w(x'))))' ID: 32 => ('w(w(w(w(w(x')))))', D6, R1, P[1], S{x4 -> x'}), NR: 'w(w(w(w(x'))))' ID: 33 => ('w(w(x'))', D6, R4, P[], S{x7 -> w(x')}), NR: 'w(w(x'))' ID: 34 => ('w(x')', D7, R4, P[], S{x7 -> x'}), NR: 'w(x')' t: w(w(w(w(w(x'))))) Nodes: [0,1,2,3,4] Edges: [(0,1),(0,1),(0,1),(0,1),(1,2),(1,2),(1,2),(2,3),(2,3),(3,4)] ID: 0 => ('w(w(w(w(w(x')))))', D0) ID: 1 => ('w(w(w(w(x'))))', D1, R4, P[], S{x7 -> w(w(w(x')))}), NR: 'w(w(w(w(x'))))' ID: 2 => ('w(w(w(x')))', D2, R4, P[], S{x7 -> w(w(x'))}), NR: 'w(w(w(x')))' ID: 3 => ('w(w(x'))', D3, R4, P[], S{x7 -> w(x')}), NR: 'w(w(x'))' ID: 4 => ('w(x')', D4, R4, P[], S{x7 -> x'}), NR: 'w(x')' SNodesPath: b(w(w(w(b(x'))))) -> w(w(w(b(w(w(b(x'))))))) -> w(w(w(w(w(w(b(w(b(x'))))))))) -> w(w(w(w(w(w(w(w(w(b(b(x'))))))))))) -> w(w(w(w(w(w(w(w(w(w(w(w(w(x'))))))))))))) -> w(w(w(w(w(w(w(w(w(w(w(w(x')))))))))))) -> w(w(w(w(w(w(w(w(w(w(w(x'))))))))))) -> w(w(w(w(w(w(w(w(w(w(x')))))))))) -> w(w(w(w(w(w(w(w(w(x'))))))))) -> w(w(w(w(w(w(w(w(x')))))))) -> w(w(w(w(w(w(w(x'))))))) -> w(w(w(w(w(w(x')))))) -> w(w(w(w(w(x'))))) -> w(w(w(w(x')))) TNodesPath: w(w(w(w(w(x'))))) -> w(w(w(w(x')))) b(w(w(w(b(x'))))) ->* w(w(w(w(x')))) *<- w(w(w(w(w(x'))))) "Joinable" The problem is confluent. Problem 1.5: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (w 1) (fSNonEmpty) ) (RULES b(b(x)) -> w(w(w(w(x)))) b(w(x)) -> w(w(w(b(x)))) w(b(x)) -> b(x) w(w(x)) -> w(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N7 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: w(w(w(w(w(x'))))) Nodes: [0,1,2,3,4] Edges: [(0,1),(0,1),(0,1),(0,1),(1,2),(1,2),(1,2),(2,3),(2,3),(3,4)] ID: 0 => ('w(w(w(w(w(x')))))', D0) ID: 1 => ('w(w(w(w(x'))))', D1, R4, P[], S{x7 -> w(w(w(x')))}), NR: 'w(w(w(w(x'))))' ID: 2 => ('w(w(w(x')))', D2, R4, P[], S{x7 -> w(w(x'))}), NR: 'w(w(w(x')))' ID: 3 => ('w(w(x'))', D3, R4, P[], S{x7 -> w(x')}), NR: 'w(w(x'))' ID: 4 => ('w(x')', D4, R4, P[], S{x7 -> x'}), NR: 'w(x')' t: b(b(x')) Nodes: [0,1,2,3,4] Edges: [(0,1),(1,2),(1,2),(1,2),(2,3),(2,3),(3,4)] ID: 0 => ('b(b(x'))', D0) ID: 1 => ('w(w(w(w(x'))))', D1, R1, P[], S{x4 -> x'}), NR: 'w(w(w(w(x'))))' ID: 2 => ('w(w(w(x')))', D2, R4, P[], S{x7 -> w(w(x'))}), NR: 'w(w(w(x')))' ID: 3 => ('w(w(x'))', D3, R4, P[], S{x7 -> w(x')}), NR: 'w(w(x'))' ID: 4 => ('w(x')', D4, R4, P[], S{x7 -> x'}), NR: 'w(x')' SNodesPath: w(w(w(w(w(x'))))) -> w(w(w(w(x')))) TNodesPath: b(b(x')) -> w(w(w(w(x')))) w(w(w(w(w(x'))))) ->* w(w(w(w(x')))) *<- b(b(x')) "Joinable" The problem is confluent. Problem 1.6: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (w 1) (fSNonEmpty) ) (RULES b(b(x)) -> w(w(w(w(x)))) b(w(x)) -> w(w(w(b(x)))) w(b(x)) -> b(x) w(w(x)) -> w(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N8 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b(b(x')) Nodes: [0,1,2,3,4] Edges: [(0,1),(1,2),(1,2),(1,2),(2,3),(2,3),(3,4)] ID: 0 => ('b(b(x'))', D0) ID: 1 => ('w(w(w(w(x'))))', D1, R1, P[], S{x4 -> x'}), NR: 'w(w(w(w(x'))))' ID: 2 => ('w(w(w(x')))', D2, R4, P[], S{x7 -> w(w(x'))}), NR: 'w(w(w(x')))' ID: 3 => ('w(w(x'))', D3, R4, P[], S{x7 -> w(x')}), NR: 'w(w(x'))' ID: 4 => ('w(x')', D4, R4, P[], S{x7 -> x'}), NR: 'w(x')' t: w(w(w(b(b(x'))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10] Edges: [(0,1),(0,2),(0,2),(0,2),(1,3),(1,3),(1,3),(1,3),(1,3),(1,3),(2,3),(2,4),(2,4),(3,5),(3,5),(3,5),(3,5),(3,5),(4,5),(4,6),(5,7),(5,7),(5,7),(5,7),(6,7),(7,8),(7,8),(7,8),(8,9),(8,9),(9,10)] ID: 0 => ('w(w(w(b(b(x')))))', D0) ID: 1 => ('w(w(w(w(w(w(w(x')))))))', D1, R1, P[1, 1, 1], S{x4 -> x'}), NR: 'w(w(w(w(x'))))' ID: 2 => ('w(w(b(b(x'))))', D1, R3, P[1, 1], S{x6 -> b(x')}), NR: 'b(b(x'))' ID: 3 => ('w(w(w(w(w(w(x'))))))', D2, R4, P[], S{x7 -> w(w(w(w(w(x')))))}), NR: 'w(w(w(w(w(w(x'))))))' ID: 4 => ('w(b(b(x')))', D2, R3, P[1], S{x6 -> b(x')}), NR: 'b(b(x'))' ID: 5 => ('w(w(w(w(w(x')))))', D3, R4, P[], S{x7 -> w(w(w(w(x'))))}), NR: 'w(w(w(w(w(x')))))' ID: 6 => ('b(b(x'))', D3, R3, P[], S{x6 -> b(x')}), NR: 'b(b(x'))' ID: 7 => ('w(w(w(w(x'))))', D4, R4, P[], S{x7 -> w(w(w(x')))}), NR: 'w(w(w(w(x'))))' ID: 8 => ('w(w(w(x')))', D5, R4, P[], S{x7 -> w(w(x'))}), NR: 'w(w(w(x')))' ID: 9 => ('w(w(x'))', D6, R4, P[], S{x7 -> w(x')}), NR: 'w(w(x'))' ID: 10 => ('w(x')', D7, R4, P[], S{x7 -> x'}), NR: 'w(x')' SNodesPath: b(b(x')) TNodesPath: b(b(x')) ->* b(b(x')) *<- w(w(w(b(b(x'))))) "Joinable" The problem is confluent.