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 x:S y:S z1:S z2:S z3: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(s(0),0) 0.001/0.001 fib(s(x:S)) -> pair(z3:S,z1:S) | fib(x:S) ->* pair(z1:S,z2:S), plus(z1:S,z2:S) ->* z3: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 x:S y:S z1:S z2:S z3: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(s(0),0) 0.001/0.001 fib(s(x:S)) -> pair(plus(z1:S,z2:S),z1:S) | fib(x:S) ->* pair(z1:S,z2: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 x:S y:S z1:S z2:S z3: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(s(0),0) 0.001/0.001 fib(s(x:S)) -> pair(plus(z1:S,z2:S),z1:S) | fib(x:S) ->* pair(z1:S,z2: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(s(0),0) 0.001/0.001 fib(s(x:S)) -> pair(plus(z1:S,z2:S),z1:S) | fib(x:S) ->* pair(z1:S,z2: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", "z1", "z2", "y", "x", "y" 0.001/0.001 -> FVars: 0.001/0.001 "x6", "x7", "x8", "x9", "x10", "x11" 0.001/0.001 -> PVars: 0.001/0.001 "x": ["x6", "x10"], "z1": ["x7"], "z2": ["x8"], "y": ["x9", "x11"] 0.001/0.001 0.001/0.001 -> Rlps: 0.001/0.001 crule: fib(0) -> pair(s(0),0), id: 1, possubterms: fib(0)-> [], 0-> [1] 0.001/0.001 crule: fib(s(x6:S)) -> pair(plus(x7:S,x8:S),x7:S) | fib(x6:S) ->* pair(x7:S,x8:S), id: 2, possubterms: fib(s(x6:S))-> [], s(x6:S)-> [1] 0.001/0.001 crule: plus(0,x9:S) -> x9:S, id: 3, possubterms: plus(0,x9:S)-> [], 0-> [1] 0.001/0.001 crule: plus(s(x10:S),x11:S) -> s(plus(x10:S,x11:S)), id: 4, possubterms: plus(s(x10:S),x11:S)-> [], s(x10: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 x:S y:S z1:S z2:S z3: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(s(0),0) 0.001/0.001 fib(s(x:S)) -> pair(plus(z1:S,z2:S),z1:S) | fib(x:S) ->* pair(z1:S,z2: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_z1,c_z2) 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 50%CPU (0avgtext+0avgdata 8208maxresident)k 0.001/0.001 8inputs+0outputs (0major+658minor)pagefaults 0swaps