0.00/0.01 YES 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 0.00/0.01 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 Confluence Problem: 0.00/0.01 (VAR vNonEmpty x) 0.00/0.01 (REPLACEMENT-MAP 0.00/0.01 (f 1) 0.00/0.01 (a) 0.00/0.01 (fSNonEmpty) 0.00/0.01 ) 0.00/0.01 (RULES 0.00/0.01 f(a) -> f(f(a)) 0.00/0.01 f(x) -> f(a) 0.00/0.01 ) 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 Not CS-TRS Procedure: 0.00/0.01 R is not a CS-TRS 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 Linearity Procedure: 0.00/0.01 Linear? 0.00/0.01 YES 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 Confluence Problem: 0.00/0.01 (VAR vNonEmpty x) 0.00/0.01 (REPLACEMENT-MAP 0.00/0.01 (f 1) 0.00/0.01 (a) 0.00/0.01 (fSNonEmpty) 0.00/0.01 ) 0.00/0.01 (RULES 0.00/0.01 f(a) -> f(f(a)) 0.00/0.01 f(x) -> f(a) 0.00/0.01 ) 0.00/0.01 Linear:YES 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 0.00/0.01 Huet Levy Procedure: 0.00/0.01 -> Rules: 0.00/0.01 f(a) -> f(f(a)) 0.00/0.01 f(x) -> f(a) 0.00/0.01 -> Vars: 0.00/0.01 x 0.00/0.01 0.00/0.01 -> Rlps: 0.00/0.01 (rule: f(a) -> f(f(a)), id: 1, possubterms: f(a)->[], a->[1]) 0.00/0.01 (rule: f(x) -> f(a), id: 2, possubterms: f(x)->[]) 0.00/0.01 0.00/0.01 -> Unifications: 0.00/0.01 (R2 unifies with R1 at p: [], l: f(x), lp: f(x), sig: {x -> a}, l': f(a), r: f(a), r': f(f(a))) 0.00/0.01 0.00/0.01 -> Critical pairs info: 0.00/0.01 => Not trivial, Overlay, Proper, NW0, N1 0.00/0.01 0.00/0.01 -> Problem conclusions: 0.00/0.01 Left linear, Right linear, Linear 0.00/0.01 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.00/0.01 Not Huet-Levy confluent, Not Newman confluent 0.00/0.01 R is a TRS 0.00/0.01 0.00/0.01 Problem 1.1: 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 Confluence Problem: 0.00/0.01 (VAR x) 0.00/0.01 (REPLACEMENT-MAP 0.00/0.01 (f 1) 0.00/0.01 (a) 0.00/0.01 (fSNonEmpty) 0.00/0.01 ) 0.00/0.01 (RULES 0.00/0.01 f(a) -> f(f(a)) 0.00/0.01 f(x) -> f(a) 0.00/0.01 ) 0.00/0.01 Critical Pairs: 0.00/0.01 => Not trivial, Overlay, Proper, NW0, N1 0.00/0.01 Linear:YES 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 0.00/0.01 Strong Confluence Procedure: 0.00/0.01 -> Rewritings: 0.00/0.01 s: f(f(a)) 0.00/0.01 Nodes: [0,1,2,3,4,5,6,7,8,9] 0.00/0.01 Edges: [(0,0),(0,1),(0,2),(1,0),(1,1),(1,2),(1,3),(2,0),(2,2),(3,0),(3,1),(3,2),(3,3),(3,4),(4,0),(4,1),(4,2),(4,3),(4,4),(4,5),(5,0),(5,1),(5,2),(5,3),(5,4),(5,5),(5,6),(6,0),(6,1),(6,2),(6,3),(6,4),(6,5),(6,6),(6,7),(7,0),(7,1),(7,2),(7,3),(7,4),(7,5),(7,6),(7,7),(7,8),(8,0),(8,1),(8,2),(8,3),(8,4),(8,5),(8,6),(8,7),(8,8),(8,9)] 0.00/0.01 ID: 0 => ('f(f(a))', D0) 0.00/0.01 ID: 1 => ('f(f(f(a)))', D1, R1, P[1], S{}), NR: 'f(f(a))' 0.00/0.01 ID: 2 => ('f(a)', D1, R2, P[], S{x2 -> f(a)}), NR: 'f(a)' 0.00/0.01 ID: 3 => ('f(f(f(f(a))))', D2, R1, P[1, 1], S{}), NR: 'f(f(a))' 0.00/0.01 ID: 4 => ('f(f(f(f(f(a)))))', D3, R1, P[1, 1, 1], S{}), NR: 'f(f(a))' 0.00/0.01 ID: 5 => ('f(f(f(f(f(f(a))))))', D4, R1, P[1, 1, 1, 1], S{}), NR: 'f(f(a))' 0.00/0.01 ID: 6 => ('f(f(f(f(f(f(f(a)))))))', D5, R1, P[1, 1, 1, 1, 1], S{}), NR: 'f(f(a))' 0.00/0.01 ID: 7 => ('f(f(f(f(f(f(f(f(a))))))))', D6, R1, P[1, 1, 1, 1, 1, 1], S{}), NR: 'f(f(a))' 0.00/0.01 ID: 8 => ('f(f(f(f(f(f(f(f(f(a)))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1], S{}), NR: 'f(f(a))' 0.00/0.01 ID: 9 => ('f(f(f(f(f(f(f(f(f(f(a))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{}), NR: 'f(f(a))' 0.00/0.01 t: f(a) 0.00/0.01 Nodes: [0,1,2,3,4,5,6,7,8] 0.00/0.01 Edges: [(0,0),(0,1),(1,0),(1,1),(1,2),(2,0),(2,1),(2,2),(2,3),(3,0),(3,1),(3,2),(3,3),(3,4),(4,0),(4,1),(4,2),(4,3),(4,4),(4,5),(5,0),(5,1),(5,2),(5,3),(5,4),(5,5),(5,6),(6,0),(6,1),(6,2),(6,3),(6,4),(6,5),(6,6),(6,7),(7,0),(7,1),(7,2),(7,3),(7,4),(7,5),(7,6),(7,7),(7,8)] 0.00/0.01 ID: 0 => ('f(a)', D0) 0.00/0.01 ID: 1 => ('f(f(a))', D1, R1, P[], S{}), NR: 'f(f(a))' 0.00/0.01 ID: 2 => ('f(f(f(a)))', D2, R1, P[1], S{}), NR: 'f(f(a))' 0.00/0.01 ID: 3 => ('f(f(f(f(a))))', D3, R1, P[1, 1], S{}), NR: 'f(f(a))' 0.00/0.01 ID: 4 => ('f(f(f(f(f(a)))))', D4, R1, P[1, 1, 1], S{}), NR: 'f(f(a))' 0.00/0.01 ID: 5 => ('f(f(f(f(f(f(a))))))', D5, R1, P[1, 1, 1, 1], S{}), NR: 'f(f(a))' 0.00/0.01 ID: 6 => ('f(f(f(f(f(f(f(a)))))))', D6, R1, P[1, 1, 1, 1, 1], S{}), NR: 'f(f(a))' 0.00/0.01 ID: 7 => ('f(f(f(f(f(f(f(f(a))))))))', D7, R1, P[1, 1, 1, 1, 1, 1], S{}), NR: 'f(f(a))' 0.00/0.01 ID: 8 => ('f(f(f(f(f(f(f(f(f(a)))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1], S{}), NR: 'f(f(a))' 0.00/0.01 SNodesPath1: f(f(a)) 0.00/0.01 TNodesPath1: f(a) -> f(f(a)) 0.00/0.01 SNodesPath2: f(f(a)) -> f(f(f(a))) -> f(a) 0.00/0.01 TNodesPath2: f(a) 0.00/0.01 f(f(a)) ->= f(f(a)) *<- f(a) 0.00/0.01 f(a) ->= f(a) *<- f(f(a)) 0.00/0.01 "Strongly closed critical pair" 0.00/0.01 0.00/0.01 The problem is confluent. 0.00/0.01 EOF