0.009/0.009 YES 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 Confluence Problem: 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 (fSNonEmpty) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> c | b ->* c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ) 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 Inlining of Conditions Processor [STERN17]: 0.009/0.009 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 Confluence Problem: 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 (fSNonEmpty) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> c | b ->* c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ) 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 Confluence Problem: 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 (fSNonEmpty) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> c | b ->* c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ) 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 0.009/0.009 Critical Pairs Processor: 0.009/0.009 -> Rules: 0.009/0.009 a -> c | b ->* c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 -> Vars: 0.009/0.009 0.009/0.009 -> FVars: 0.009/0.009 0.009/0.009 -> PVars: 0.009/0.009 0.009/0.009 0.009/0.009 -> Rlps: 0.009/0.009 crule: a -> c | b ->* c, id: 1, possubterms: a-> [] 0.009/0.009 crule: b -> c, id: 2, possubterms: b-> [] 0.009/0.009 crule: f(b) -> f(a), id: 3, possubterms: f(b)-> [], b-> [1] 0.009/0.009 0.009/0.009 -> Unifications: 0.009/0.009 R3 unifies with R2 at p: [1], l: f(b), lp: b, conds: {}, sig: {}, l': b, r: f(a), r': c 0.009/0.009 0.009/0.009 -> Critical pairs info: 0.009/0.009 => Not trivial, Not overlay, N1 0.009/0.009 0.009/0.009 -> Problem conclusions: 0.009/0.009 Left linear, Right linear, Linear 0.009/0.009 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.009/0.009 CTRS Type: 1 0.009/0.009 Deterministic, Strongly deterministic 0.009/0.009 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.009/0.009 Maybe right-stable CTRS, Not overlay CTRS 0.009/0.009 Maybe normal CTRS, Maybe almost normal CTRS 0.009/0.009 Maybe terminating CTRS, Maybe joinable CCPs 0.009/0.009 Maybe level confluent 0.009/0.009 Maybe confluent 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 Underlying TRS Termination Processor: 0.009/0.009 0.009/0.009 Resulting Underlying TRS: 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ) 0.009/0.009 Underlying TRS terminating? 0.009/0.009 YES 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 (VAR vu95NonEmpty:S vNonEmptyu58S:S) 0.009/0.009 (RULES 0.009/0.009 a -> c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ) 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 Dependency Pairs Processor: 0.009/0.009 -> Pairs: 0.009/0.009 F(b) -> A 0.009/0.009 F(b) -> F(a) 0.009/0.009 -> Rules: 0.009/0.009 a -> c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 SCC Processor: 0.009/0.009 -> Pairs: 0.009/0.009 F(b) -> A 0.009/0.009 F(b) -> F(a) 0.009/0.009 -> Rules: 0.009/0.009 a -> c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ->Strongly Connected Components: 0.009/0.009 ->->Cycle: 0.009/0.009 ->->-> Pairs: 0.009/0.009 F(b) -> F(a) 0.009/0.009 ->->-> Rules: 0.009/0.009 a -> c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 Reduction Pair Processor: 0.009/0.009 -> Pairs: 0.009/0.009 F(b) -> F(a) 0.009/0.009 -> Rules: 0.009/0.009 a -> c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 -> Usable rules: 0.009/0.009 a -> c 0.009/0.009 ->Interpretation type: 0.009/0.009 Linear 0.009/0.009 ->Coefficients: 0.009/0.009 Natural Numbers 0.009/0.009 ->Dimension: 0.009/0.009 1 0.009/0.009 ->Bound: 0.009/0.009 2 0.009/0.009 ->Interpretation: 0.009/0.009 0.009/0.009 [a] = 1 0.009/0.009 [b] = 2 0.009/0.009 [f](X) = 0 0.009/0.009 [c] = 1 0.009/0.009 [fSNonEmpty] = 0 0.009/0.009 [A] = 0 0.009/0.009 [F](X) = 2.X 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 SCC Processor: 0.009/0.009 -> Pairs: 0.009/0.009 Empty 0.009/0.009 -> Rules: 0.009/0.009 a -> c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ->Strongly Connected Components: 0.009/0.009 There is no strongly connected component 0.009/0.009 0.009/0.009 The problem is finite. 0.009/0.009 0.009/0.009 0.009/0.009 -> Problem conclusions: 0.009/0.009 Left linear, Right linear, Linear 0.009/0.009 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.009/0.009 CTRS Type: 1 0.009/0.009 Deterministic, Strongly deterministic 0.009/0.009 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.009/0.009 Maybe right-stable CTRS, Not overlay CTRS 0.009/0.009 Maybe normal CTRS, Maybe almost normal CTRS 0.009/0.009 Terminating CTRS, Maybe joinable CCPs 0.009/0.009 Maybe level confluent 0.009/0.009 Maybe confluent 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 Transform CTRS Processor: 0.009/0.009 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 Confluence Problem: 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 (fSNonEmpty) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> c | b ->* c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ) 0.009/0.009 Critical Pairs: 0.009/0.009 => Not trivial, Not overlay, N1 0.009/0.009 Terminating:YES 0.009/0.009 0.009/0.009 -> Problem conclusions: 0.009/0.009 Left linear, Right linear, Linear 0.009/0.009 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.009/0.009 CTRS Type: 1 0.009/0.009 Deterministic, Strongly deterministic 0.009/0.009 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.009/0.009 Maybe right-stable CTRS, Not overlay CTRS 0.009/0.009 Maybe normal CTRS, Maybe almost normal CTRS 0.009/0.009 Terminating CTRS, Maybe joinable CCPs 0.009/0.009 Maybe level confluent 0.009/0.009 Maybe confluent 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 Resulting U(R): 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 (fSNonEmpty) 0.009/0.009 (U6_1 1) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> U6_1(b) 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 U6_1(c) -> c 0.009/0.009 ) 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 Confluence Problem: 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 (fSNonEmpty) 0.009/0.009 (U6_1 1) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> U6_1(b) 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 U6_1(c) -> c 0.009/0.009 ) 0.009/0.009 Terminating:"YES" 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 0.009/0.009 Huet Levy Processor: 0.009/0.009 -> Rules: 0.009/0.009 a -> U6_1(b) 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 U6_1(c) -> c 0.009/0.009 -> Vars: 0.009/0.009 0.009/0.009 -> FVars: 0.009/0.009 0.009/0.009 -> PVars: 0.009/0.009 0.009/0.009 0.009/0.009 -> Rlps: 0.009/0.009 (rule: a -> U6_1(b), id: 1, possubterms: a->[]) 0.009/0.009 (rule: b -> c, id: 2, possubterms: b->[]) 0.009/0.009 (rule: f(b) -> f(a), id: 3, possubterms: f(b)->[], b->[1]) 0.009/0.009 (rule: U6_1(c) -> c, id: 4, possubterms: U6_1(c)->[], c->[1]) 0.009/0.009 0.009/0.009 -> Unifications: 0.009/0.009 (R3 unifies with R2 at p: [1], l: f(b), lp: b, sig: {}, l': b, r: f(a), r': c) 0.009/0.009 0.009/0.009 -> Critical pairs info: 0.009/0.009 => Not trivial, Not overlay, N1 0.009/0.009 0.009/0.009 -> Problem conclusions: 0.009/0.009 Left linear, Right linear, Linear 0.009/0.009 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.009/0.009 Not Huet-Levy confluent, Not Newman confluent 0.009/0.009 R is a TRS 0.009/0.009 0.009/0.009 Problem 1.1: 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 Confluence Problem: 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 (fSNonEmpty) 0.009/0.009 (U6_1 1) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> U6_1(b) 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 U6_1(c) -> c 0.009/0.009 ) 0.009/0.009 Critical Pairs: 0.009/0.009 => Not trivial, Not overlay, N1 0.009/0.009 Terminating:"YES" 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 0.009/0.009 Huet Brute Force Joinability Processor: 0.009/0.009 -> Rewritings: 0.009/0.009 s: f(c) 0.009/0.009 Nodes: [0] 0.009/0.009 Edges: [] 0.009/0.009 ID: 0 => ('f(c)', D0) 0.009/0.009 t: f(a) 0.009/0.009 Nodes: [0,1,2,3] 0.009/0.009 Edges: [(0,1),(1,2),(2,3)] 0.009/0.009 ID: 0 => ('f(a)', D0) 0.009/0.009 ID: 1 => ('f(U6_1(b))', D1, R1, P[1], S{}), NR: 'U6_1(b)' 0.009/0.009 ID: 2 => ('f(U6_1(c))', D2, R2, P[1, 1], S{}), NR: 'c' 0.009/0.009 ID: 3 => ('f(c)', D3, R4, P[1], S{}), NR: 'c' 0.009/0.009 f(c) ->* f(c) *<- f(a) 0.009/0.009 "Joinable" 0.009/0.009 0.009/0.009 The problem is joinable. 0.009/0.009 0.07user 0.01system 0:00.09elapsed 94%CPU (0avgtext+0avgdata 14492maxresident)k 0.009/0.009 0inputs+0outputs (0major+6020minor)pagefaults 0swaps