YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (a) (b) (c) (d) (g 1) (h 1) (e) (fSNonEmpty) ) (RULES a -> b a -> c a -> e b -> d c -> a d -> a d -> e g(x) -> h(a) h(x) -> e ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: CSR Converter From Canonical u-Replacement Map Procedure [CSUR20]: Original Replacement Map: (a) (b) (c) (d) (g 1) (h 1) (e) (fSNonEmpty) New Replacement Map: (a) (b) (c) (d) (g) (h) (e) (fSNonEmpty) New problem: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (a) (b) (c) (d) (g) (h) (e) (fSNonEmpty) ) (RULES a -> b a -> c a -> e b -> d c -> a d -> a d -> e g(x) -> h(a) h(x) -> e ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Weak Normalization FORT Procedure: (VAR vNonEmpty x) (RULES a -> b a -> c a -> e b -> d c -> a d -> a d -> e g(x) -> h(a) h(x) -> e ) Normalizating? YES ; certificate: (0 (rr2-rel (stepsnf (0)) 1 0) (rr2-rel (stepsnf (0)) 1 0) (size 2 14 0)) (1 (exists 0) (exists (rr2-rel (stepsnf (0)) 1 0)) (size 2 14 0)) (2 (not 1) (not (exists (rr2-rel (stepsnf (0)) 1 0))) (size 0 0 0)) (3 (exists 2) (exists (not (exists (rr2-rel (stepsnf (0)) 1 0))))) (4 (not 3) (not (exists (not (exists (rr2-rel (stepsnf (0)) 1 0)))))) (5 (nnf+ 4) (forall (exists (rr2-rel (stepsnf (0)) 1 0)))) (nonempty 5) Problem 1.1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (a) (b) (c) (d) (g) (h) (e) (fSNonEmpty) ) (RULES a -> b a -> c a -> e b -> d c -> a d -> a d -> e g(x) -> h(a) h(x) -> e ) Normalizating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy NW Procedure: -> Rules: a -> b a -> c a -> e b -> d c -> a d -> a d -> e g(x) -> h(a) h(x) -> e -> Vars: x, x -> UVars: (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) (UV-RuleId: 3, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) (UV-RuleId: 4, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) (UV-RuleId: 5, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) (UV-RuleId: 8, UV-LActive: [x], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) (UV-RuleId: 9, UV-LActive: [x], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) -> Rlps: (rule: a -> b, id: 1, possubterms: a->[]) (rule: a -> c, id: 2, possubterms: a->[]) (rule: a -> e, id: 3, possubterms: a->[]) (rule: b -> d, id: 4, possubterms: b->[]) (rule: c -> a, id: 5, possubterms: c->[]) (rule: d -> a, id: 6, possubterms: d->[]) (rule: d -> e, id: 7, possubterms: d->[]) (rule: g(x) -> h(a), id: 8, possubterms: g(x)->[]) (rule: h(x) -> e, id: 9, possubterms: h(x)->[]) -> Unifications: (R2 unifies with R1 at p: [], l: a, lp: a, sig: {}, l': a, r: c, r': b) (R3 unifies with R1 at p: [], l: a, lp: a, sig: {}, l': a, r: e, r': b) (R3 unifies with R2 at p: [], l: a, lp: a, sig: {}, l': a, r: e, r': c) (R7 unifies with R6 at p: [], l: d, lp: d, sig: {}, l': d, r: e, r': a) -> Critical pairs info: => Not trivial, Overlay, Proper, NW1, N1 => Not trivial, Overlay, Proper, NW1, N2 => Not trivial, Overlay, Proper, NW1, N3 => Not trivial, Overlay, Proper, NW0, N4 -> 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 CS-TRS, Left-homogeneous u-replacing variables The problem is decomposed in 4 subproblems. Problem 1.1.1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x) (REPLACEMENT-MAP (a) (b) (c) (d) (g) (h) (e) (fSNonEmpty) ) (RULES a -> b a -> c a -> e b -> d c -> a d -> a d -> e g(x) -> h(a) h(x) -> e ) Critical Pairs: => Not trivial, Overlay, Proper, NW1, N1 Normalizating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: c Nodes: [0,1,2,3,4] Edges: [(0,1),(1,0),(1,2),(1,3),(2,4),(4,1),(4,3)] ID: 0 => ('c', D0) ID: 1 => ('a', D1, R5, P[], S{}), NR: 'a' ID: 2 => ('b', D2, R1, P[], S{}), NR: 'b' ID: 3 => ('e', D2, R3, P[], S{}), NR: 'e' ID: 4 => ('d', D3, R4, P[], S{}), NR: 'd' t: e Nodes: [0] Edges: [] ID: 0 => ('e', D0) SNodesPath: c -> a -> b -> d -> e TNodesPath: e c ->* e *<- e "Joinable" The problem is confluent. Problem 1.1.2: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x) (REPLACEMENT-MAP (a) (b) (c) (d) (g) (h) (e) (fSNonEmpty) ) (RULES a -> b a -> c a -> e b -> d c -> a d -> a d -> e g(x) -> h(a) h(x) -> e ) Critical Pairs: => Not trivial, Overlay, Proper, NW1, N2 Normalizating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: a Nodes: [0,1,2,3,4] Edges: [(0,1),(0,2),(0,3),(1,4),(2,0),(4,0),(4,3)] ID: 0 => ('a', D0) ID: 1 => ('b', D1, R1, P[], S{}), NR: 'b' ID: 2 => ('c', D1, R2, P[], S{}), NR: 'c' ID: 3 => ('e', D1, R3, P[], S{}), NR: 'e' ID: 4 => ('d', D2, R4, P[], S{}), NR: 'd' t: e Nodes: [0] Edges: [] ID: 0 => ('e', D0) SNodesPath: a -> b -> d -> e TNodesPath: e a ->* e *<- e "Joinable" The problem is confluent. Problem 1.1.3: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x) (REPLACEMENT-MAP (a) (b) (c) (d) (g) (h) (e) (fSNonEmpty) ) (RULES a -> b a -> c a -> e b -> d c -> a d -> a d -> e g(x) -> h(a) h(x) -> e ) Critical Pairs: => Not trivial, Overlay, Proper, NW1, N3 Normalizating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b Nodes: [0,1,2,3,4] Edges: [(0,1),(1,2),(1,3),(2,0),(2,3),(2,4),(4,2)] ID: 0 => ('b', D0) ID: 1 => ('d', D1, R4, P[], S{}), NR: 'd' ID: 2 => ('a', D2, R6, P[], S{}), NR: 'a' ID: 3 => ('e', D2, R7, P[], S{}), NR: 'e' ID: 4 => ('c', D3, R2, P[], S{}), NR: 'c' t: e Nodes: [0] Edges: [] ID: 0 => ('e', D0) SNodesPath: b -> d -> a -> e TNodesPath: e b ->* e *<- e "Joinable" The problem is confluent. Problem 1.1.4: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x) (REPLACEMENT-MAP (a) (b) (c) (d) (g) (h) (e) (fSNonEmpty) ) (RULES a -> b a -> c a -> e b -> d c -> a d -> a d -> e g(x) -> h(a) h(x) -> e ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N4 Normalizating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b Nodes: [0,1,2,3,4] Edges: [(0,1),(1,2),(1,3),(2,0),(2,3),(2,4),(4,2)] ID: 0 => ('b', D0) ID: 1 => ('d', D1, R4, P[], S{}), NR: 'd' ID: 2 => ('a', D2, R6, P[], S{}), NR: 'a' ID: 3 => ('e', D2, R7, P[], S{}), NR: 'e' ID: 4 => ('c', D3, R2, P[], S{}), NR: 'c' t: c Nodes: [0,1,2,3,4] Edges: [(0,1),(1,0),(1,2),(1,3),(2,4),(4,1),(4,3)] ID: 0 => ('c', D0) ID: 1 => ('a', D1, R5, P[], S{}), NR: 'a' ID: 2 => ('b', D2, R1, P[], S{}), NR: 'b' ID: 3 => ('e', D2, R3, P[], S{}), NR: 'e' ID: 4 => ('d', D3, R4, P[], S{}), NR: 'd' SNodesPath: b TNodesPath: c -> a -> b b ->* b *<- c "Joinable" The problem is confluent.