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 x1:S y:S y1:S ys:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (cons 1 2) 0.001/0.001 (lt 1 2) 0.001/0.001 (nat 1) 0.001/0.001 (0) 0.001/0.001 (arr 1 2 3) 0.001/0.001 (empty) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (false) 0.001/0.001 (s 1) 0.001/0.001 (true) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 cons(s(x:S),cons(s(y:S),arr(ys:S,empty,empty))) -> arr(x1:S,y1:S,ys:S) | lt(x1:S,y1:S) ->* true, s(x:S) ->* x1:S, s(y:S) ->* y1:S 0.001/0.001 cons(x:S,cons(y:S,arr(ys:S,empty,empty))) -> arr(x:S,y:S,ys:S) | lt(x:S,y:S) ->* true 0.001/0.001 lt(0,s(y:S)) -> true | nat(s(y:S)) ->* true 0.001/0.001 lt(s(x:S),s(y:S)) -> lt(x:S,y:S) 0.001/0.001 lt(x:S,0) -> false | nat(x:S) ->* true 0.001/0.001 nat(x:S) -> lt(0,x: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 x1:S y:S y1:S ys:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (cons 1 2) 0.001/0.001 (lt 1 2) 0.001/0.001 (nat 1) 0.001/0.001 (0) 0.001/0.001 (arr 1 2 3) 0.001/0.001 (empty) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (false) 0.001/0.001 (s 1) 0.001/0.001 (true) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 cons(s(x:S),cons(s(y:S),arr(ys:S,empty,empty))) -> arr(s(x:S),s(y:S),ys:S) | lt(s(x:S),s(y:S)) ->* true 0.001/0.001 cons(x:S,cons(y:S,arr(ys:S,empty,empty))) -> arr(x:S,y:S,ys:S) | lt(x:S,y:S) ->* true 0.001/0.001 lt(0,s(y:S)) -> true | nat(s(y:S)) ->* true 0.001/0.001 lt(s(x:S),s(y:S)) -> lt(x:S,y:S) 0.001/0.001 lt(x:S,0) -> false | nat(x:S) ->* true 0.001/0.001 nat(x:S) -> lt(0,x: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 x1:S y:S y1:S ys:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (cons 1 2) 0.001/0.001 (lt 1 2) 0.001/0.001 (nat 1) 0.001/0.001 (0) 0.001/0.001 (arr 1 2 3) 0.001/0.001 (empty) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (false) 0.001/0.001 (s 1) 0.001/0.001 (true) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 cons(s(x:S),cons(s(y:S),arr(ys:S,empty,empty))) -> arr(s(x:S),s(y:S),ys:S) | lt(s(x:S),s(y:S)) ->* true 0.001/0.001 cons(x:S,cons(y:S,arr(ys:S,empty,empty))) -> arr(x:S,y:S,ys:S) | lt(x:S,y:S) ->* true 0.001/0.001 lt(0,s(y:S)) -> true | nat(s(y:S)) ->* true 0.001/0.001 lt(s(x:S),s(y:S)) -> lt(x:S,y:S) 0.001/0.001 lt(x:S,0) -> false | nat(x:S) ->* true 0.001/0.001 nat(x:S) -> lt(0,x: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 cons(s(x:S),cons(s(y:S),arr(ys:S,empty,empty))) -> arr(s(x:S),s(y:S),ys:S) | lt(s(x:S),s(y:S)) ->* true 0.001/0.001 cons(x:S,cons(y:S,arr(ys:S,empty,empty))) -> arr(x:S,y:S,ys:S) | lt(x:S,y:S) ->* true 0.001/0.001 lt(0,s(y:S)) -> true | nat(s(y:S)) ->* true 0.001/0.001 lt(s(x:S),s(y:S)) -> lt(x:S,y:S) 0.001/0.001 lt(x:S,0) -> false | nat(x:S) ->* true 0.001/0.001 nat(x:S) -> lt(0,x:S) 0.001/0.001 -> Vars: 0.001/0.001 "x", "y", "ys", "x", "y", "ys", "y", "x", "y", "x", "x" 0.001/0.001 -> FVars: 0.001/0.001 "x6", "x7", "x8", "x9", "x10", "x11", "x12", "x13", "x14", "x15", "x16" 0.001/0.001 -> PVars: 0.001/0.001 "x": ["x6", "x9", "x13", "x15", "x16"], "y": ["x7", "x10", "x12", "x14"], "ys": ["x8", "x11"] 0.001/0.001 0.001/0.001 -> Rlps: 0.001/0.001 crule: cons(s(x6:S),cons(s(x7:S),arr(x8:S,empty,empty))) -> arr(s(x6:S),s(x7:S),x8:S) | lt(s(x6:S),s(x7:S)) ->* true, id: 1, possubterms: cons(s(x6:S),cons(s(x7:S),arr(x8:S,empty,empty)))-> [], s(x6:S)-> [1], cons(s(x7:S),arr(x8:S,empty,empty))-> [2], s(x7:S)-> [2,1], arr(x8:S,empty,empty)-> [2,2], empty-> [2,2,2], empty-> [2,2,3] 0.001/0.001 crule: cons(x9:S,cons(x10:S,arr(x11:S,empty,empty))) -> arr(x9:S,x10:S,x11:S) | lt(x9:S,x10:S) ->* true, id: 2, possubterms: cons(x9:S,cons(x10:S,arr(x11:S,empty,empty)))-> [], cons(x10:S,arr(x11:S,empty,empty))-> [2], arr(x11:S,empty,empty)-> [2,2], empty-> [2,2,2], empty-> [2,2,3] 0.001/0.001 crule: lt(0,s(x12:S)) -> true | nat(s(x12:S)) ->* true, id: 3, possubterms: lt(0,s(x12:S))-> [], 0-> [1], s(x12:S)-> [2] 0.001/0.001 crule: lt(s(x13:S),s(x14:S)) -> lt(x13:S,x14:S), id: 4, possubterms: lt(s(x13:S),s(x14:S))-> [], s(x13:S)-> [1], s(x14:S)-> [2] 0.001/0.001 crule: lt(x15:S,0) -> false | nat(x15:S) ->* true, id: 5, possubterms: lt(x15:S,0)-> [], 0-> [2] 0.001/0.001 crule: nat(x16:S) -> lt(0,x16:S), id: 6, possubterms: nat(x16:S)-> [] 0.001/0.001 0.001/0.001 -> Unifications: 0.001/0.001 R2 unifies with R1 at p: [], l: cons(x9:S,cons(x10:S,arr(x11:S,empty,empty))), lp: cons(x9:S,cons(x10:S,arr(x11:S,empty,empty))), conds: {lt(x9:S,x10:S) ->* true, lt(s(x:S),s(y:S)) ->* true}, sig: {x9:S -> s(x:S),x10:S -> s(y:S),x11:S -> ys:S}, l': cons(s(x:S),cons(s(y:S),arr(ys:S,empty,empty))), r: arr(x9:S,x10:S,x11:S), r': arr(s(x:S),s(y:S),ys:S) 0.001/0.001 0.001/0.001 -> Critical pairs info: 0.001/0.001 | lt(s(x:S),s(y:S)) ->* true => Trivial, Overlay, N1 0.001/0.001 0.001/0.001 -> Problem conclusions: 0.001/0.001 Left linear, Right linear, Linear 0.001/0.001 Weakly orthogonal, Almost orthogonal, Not orthogonal 0.001/0.001 CTRS Type: 1 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 x1:S y:S y1:S ys:S) 0.001/0.001 (STRATEGY CONTEXTSENSITIVE 0.001/0.001 (cons 1 2) 0.001/0.001 (lt 1 2) 0.001/0.001 (nat 1) 0.001/0.001 (0) 0.001/0.001 (arr 1 2 3) 0.001/0.001 (empty) 0.001/0.001 (fSNonEmpty) 0.001/0.001 (false) 0.001/0.001 (s 1) 0.001/0.001 (true) 0.001/0.001 ) 0.001/0.001 (RULES 0.001/0.001 cons(s(x:S),cons(s(y:S),arr(ys:S,empty,empty))) -> arr(s(x:S),s(y:S),ys:S) | lt(s(x:S),s(y:S)) ->* true 0.001/0.001 cons(x:S,cons(y:S,arr(ys:S,empty,empty))) -> arr(x:S,y:S,ys:S) | lt(x:S,y:S) ->* true 0.001/0.001 lt(0,s(y:S)) -> true | nat(s(y:S)) ->* true 0.001/0.001 lt(s(x:S),s(y:S)) -> lt(x:S,y:S) 0.001/0.001 lt(x:S,0) -> false | nat(x:S) ->* true 0.001/0.001 nat(x:S) -> lt(0,x: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: true 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 0.001/0.001 -> Term right-stability conditions: 0.001/0.001 Term: true 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 0.001/0.001 -> Term right-stability conditions: 0.001/0.001 Term: true 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 0.001/0.001 -> Term right-stability conditions: 0.001/0.001 Term: true 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, Right linear, Linear 0.001/0.001 Weakly orthogonal, Almost orthogonal, Orthogonal 0.001/0.001 CTRS Type: 1 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 66%CPU (0avgtext+0avgdata 8728maxresident)k 0.001/0.001 0inputs+0outputs (0major+732minor)pagefaults 0swaps