0.001/0.001 YES 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 0.001/0.001 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 Confluence Problem: 0.001/0.001 (VAR vNonEmpty:S w:S x:S y:S z:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (fib 1) 0.001/0.001 (plus 1 2) 0.001/0.001 (0) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (pair 1 2) 0.001/0.001 (s 1) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 fib(0) -> pair(0,s(0)) 0.001/0.001 fib(s(x:S)) -> pair(z:S,w:S) | fib(x:S) ->* pair(y:S,z:S), plus(y:S,z:S) ->* w:S 0.001/0.001 plus(0,y:S) -> y:S 0.001/0.001 plus(s(x:S),y:S) -> s(plus(x:S,y:S)) 0.001/0.001 ) 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 0.001/0.001 Inlining of Conditions Processor [STERN17]: 0.001/0.001 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 Confluence Problem: 0.001/0.001 (VAR vNonEmpty:S w:S x:S y:S z:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (fib 1) 0.001/0.001 (plus 1 2) 0.001/0.001 (0) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (pair 1 2) 0.001/0.001 (s 1) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 fib(0) -> pair(0,s(0)) 0.001/0.001 fib(s(x:S)) -> pair(z:S,plus(y:S,z:S)) | fib(x:S) ->* pair(y:S,z:S) 0.001/0.001 plus(0,y:S) -> y:S 0.001/0.001 plus(s(x:S),y:S) -> s(plus(x:S,y:S)) 0.001/0.001 ) 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 Confluence Problem: 0.001/0.001 (VAR vNonEmpty:S w:S x:S y:S z:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (fib 1) 0.001/0.001 (plus 1 2) 0.001/0.001 (0) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (pair 1 2) 0.001/0.001 (s 1) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 fib(0) -> pair(0,s(0)) 0.001/0.001 fib(s(x:S)) -> pair(z:S,plus(y:S,z:S)) | fib(x:S) ->* pair(y:S,z:S) 0.001/0.001 plus(0,y:S) -> y:S 0.001/0.001 plus(s(x:S),y:S) -> s(plus(x:S,y:S)) 0.001/0.001 ) 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 0.001/0.001 Critical Pairs Processor: 0.001/0.001 -> Rules: 0.001/0.001 fib(0) -> pair(0,s(0)) 0.001/0.001 fib(s(x:S)) -> pair(z:S,plus(y:S,z:S)) | fib(x:S) ->* pair(y:S,z:S) 0.001/0.001 plus(0,y:S) -> y:S 0.001/0.001 plus(s(x:S),y:S) -> s(plus(x:S,y:S)) 0.001/0.001 -> Vars: 0.001/0.001 "x", "y", "z", "y", "x", "y" 0.001/0.001 -> FVars: 0.001/0.001 "x5", "x6", "x7", "x8", "x9", "x10" 0.001/0.001 -> PVars: 0.001/0.001 "x": ["x5", "x9"], "y": ["x6", "x8", "x10"], "z": ["x7"] 0.001/0.001 0.001/0.001 -> Rlps: 0.001/0.001 crule: fib(0) -> pair(0,s(0)), id: 1, possubterms: fib(0)-> [], 0-> [1] 0.001/0.001 crule: fib(s(x5:S)) -> pair(x7:S,plus(x6:S,x7:S)) | fib(x5:S) ->* pair(x6:S,x7:S), id: 2, possubterms: fib(s(x5:S))-> [], s(x5:S)-> [1] 0.001/0.001 crule: plus(0,x8:S) -> x8:S, id: 3, possubterms: plus(0,x8:S)-> [], 0-> [1] 0.001/0.001 crule: plus(s(x9:S),x10:S) -> s(plus(x9:S,x10:S)), id: 4, possubterms: plus(s(x9:S),x10:S)-> [], s(x9:S)-> [1] 0.001/0.001 0.001/0.001 -> Unifications: 0.001/0.001 0.001/0.001 0.001/0.001 -> Critical pairs info: 0.001/0.001 0.001/0.001 0.001/0.001 -> Problem conclusions: 0.001/0.001 Left linear, Not right linear, Not linear 0.001/0.001 Weakly orthogonal, Almost orthogonal, Orthogonal 0.001/0.001 CTRS Type: 3 0.001/0.001 Deterministic, Strongly deterministic 0.001/0.001 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.001/0.001 Maybe right-stable CTRS, Overlay CTRS 0.001/0.001 Maybe normal CTRS, Maybe almost normal CTRS 0.001/0.001 Maybe terminating CTRS, Joinable CCPs 0.001/0.001 Maybe level confluent 0.001/0.001 Maybe confluent 0.001/0.001 0.001/0.001 Problem 1: 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 Confluence Problem: 0.001/0.001 (VAR vNonEmpty:S w:S x:S y:S z:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (fib 1) 0.001/0.001 (plus 1 2) 0.001/0.001 (0) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (pair 1 2) 0.001/0.001 (s 1) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 fib(0) -> pair(0,s(0)) 0.001/0.001 fib(s(x:S)) -> pair(z:S,plus(y:S,z:S)) | fib(x:S) ->* pair(y:S,z:S) 0.001/0.001 plus(0,y:S) -> y:S 0.001/0.001 plus(s(x:S),y:S) -> s(plus(x:S,y:S)) 0.001/0.001 ) 0.001/0.001 Critical Pairs: 0.001/0.001 0.001/0.001 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.001/0.001 0.001/0.001 Right Stable Processor: 0.001/0.001 Right-stable CTRS 0.001/0.001 Justification: 0.001/0.001 0.001/0.001 -> Term right-stability conditions: 0.001/0.001 Term: pair(c_y,c_z) 0.001/0.001 Right-stable term 0.001/0.001 Linear constructor form 0.001/0.001 Don't know if term is a ground normal form (not needed) 0.001/0.001 Right-stability condition achieved 0.001/0.001 A call to InfChecker wasn't needed 0.001/0.001 0.001/0.001 -> Problem conclusions: 0.001/0.001 Left linear, Not right linear, Not linear 0.001/0.001 Weakly orthogonal, Almost orthogonal, Orthogonal 0.001/0.001 CTRS Type: 3 0.001/0.001 Deterministic, Strongly deterministic 0.001/0.001 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.001/0.001 Right-stable CTRS, Overlay CTRS 0.001/0.001 Maybe normal CTRS, Almost normal CTRS 0.001/0.001 Maybe terminating CTRS, Joinable CCPs 0.001/0.001 Level confluent 0.001/0.001 Confluent 0.001/0.001 0.001/0.001 The problem is joinable. 0.001/0.001 0.00user 0.00system 0:00.01elapsed 58%CPU (0avgtext+0avgdata 8372maxresident)k 0.001/0.001 8inputs+0outputs (0major+664minor)pagefaults 0swaps