20.004/20.004 NO 20.004/20.004 20.004/20.004 Problem 1: 20.004/20.004 20.004/20.004 20.004/20.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.004/20.004 Confluence Problem: 20.004/20.004 (VAR vNonEmpty:S v:S w:S y:S z:S xs:S xs':S ys':S) 20.004/20.004 (STRATEGY CONTEXTSENSITIVE 20.004/20.004 (ssp 1 2) 20.004/20.004 (sub 1 2) 20.004/20.004 (0) 20.004/20.004 (cons 1 2) 20.004/20.004 (fSNonEmpty) 20.004/20.004 (nil) 20.004/20.004 (s 1) 20.004/20.004 ) 20.004/20.004 (RULES 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,xs':S) | sub(v:S,y:S) ->* w:S, ssp(ys':S,w:S) ->* xs':S 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> xs:S | ssp(ys':S,v:S) ->* xs:S 20.004/20.004 ssp(nil,0) -> nil 20.004/20.004 sub(s(v:S),s(w:S)) -> z:S | sub(v:S,w:S) ->* z:S 20.004/20.004 sub(z:S,0) -> z:S 20.004/20.004 ) 20.004/20.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.004/20.004 20.004/20.004 20.004/20.004 Problem 1: 20.004/20.004 20.004/20.004 Inlining of Conditions Processor [STERN17]: 20.004/20.004 20.004/20.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.004/20.004 Confluence Problem: 20.004/20.004 (VAR vNonEmpty:S v:S w:S y:S z:S xs:S xs':S ys':S) 20.004/20.004 (STRATEGY CONTEXTSENSITIVE 20.004/20.004 (ssp 1 2) 20.004/20.004 (sub 1 2) 20.004/20.004 (0) 20.004/20.004 (cons 1 2) 20.004/20.004 (fSNonEmpty) 20.004/20.004 (nil) 20.004/20.004 (s 1) 20.004/20.004 ) 20.004/20.004 (RULES 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> ssp(ys':S,v:S) 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,ssp(ys':S,sub(v:S,y:S))) 20.004/20.004 ssp(nil,0) -> nil 20.004/20.004 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 20.004/20.004 sub(z:S,0) -> z:S 20.004/20.004 ) 20.004/20.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.004/20.004 20.004/20.004 20.004/20.004 Problem 1: 20.004/20.004 20.004/20.004 Clean CTRS Processor: 20.004/20.004 20.004/20.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.004/20.004 Confluence Problem: 20.004/20.004 (VAR v:S w:S y:S z:S ys':S) 20.004/20.004 (STRATEGY CONTEXTSENSITIVE 20.004/20.004 (ssp 1 2) 20.004/20.004 (sub 1 2) 20.004/20.004 (0) 20.004/20.004 (cons 1 2) 20.004/20.004 (fSNonEmpty) 20.004/20.004 (nil) 20.004/20.004 (s 1) 20.004/20.004 ) 20.004/20.004 (RULES 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> ssp(ys':S,v:S) 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,ssp(ys':S,sub(v:S,y:S))) 20.004/20.004 ssp(nil,0) -> nil 20.004/20.004 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 20.004/20.004 sub(z:S,0) -> z:S 20.004/20.004 ) 20.004/20.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.004/20.004 20.004/20.004 CRule InfChecker Info: 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> ssp(ys':S,v:S) 20.004/20.004 Rule remains 20.004/20.004 Proof: 20.004/20.004 NO_CONDS 20.004/20.004 20.004/20.004 CRule InfChecker Info: 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,ssp(ys':S,sub(v:S,y:S))) 20.004/20.004 Rule remains 20.004/20.004 Proof: 20.004/20.004 NO_CONDS 20.004/20.004 20.004/20.004 CRule InfChecker Info: 20.004/20.004 ssp(nil,0) -> nil 20.004/20.004 Rule remains 20.004/20.004 Proof: 20.004/20.004 NO_CONDS 20.004/20.004 20.004/20.004 CRule InfChecker Info: 20.004/20.004 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 20.004/20.004 Rule remains 20.004/20.004 Proof: 20.004/20.004 NO_CONDS 20.004/20.004 20.004/20.004 CRule InfChecker Info: 20.004/20.004 sub(z:S,0) -> z:S 20.004/20.004 Rule remains 20.004/20.004 Proof: 20.004/20.004 NO_CONDS 20.004/20.004 20.004/20.004 Problem 1: 20.004/20.004 20.004/20.004 Transform No Conds CTRS Processor: 20.004/20.004 20.004/20.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.004/20.004 Confluence Problem: 20.004/20.004 (VAR v:S w:S y:S z:S ys':S) 20.004/20.004 (STRATEGY CONTEXTSENSITIVE 20.004/20.004 (ssp 1 2) 20.004/20.004 (sub 1 2) 20.004/20.004 (0) 20.004/20.004 (cons 1 2) 20.004/20.004 (fSNonEmpty) 20.004/20.004 (nil) 20.004/20.004 (s 1) 20.004/20.004 ) 20.004/20.004 (RULES 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> ssp(ys':S,v:S) 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,ssp(ys':S,sub(v:S,y:S))) 20.004/20.004 ssp(nil,0) -> nil 20.004/20.004 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 20.004/20.004 sub(z:S,0) -> z:S 20.004/20.004 ) 20.004/20.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.004/20.004 Resulting R: 20.004/20.004 (VAR v:S w:S y:S z:S ys':S) 20.004/20.004 (STRATEGY CONTEXTSENSITIVE 20.004/20.004 (ssp 1 2) 20.004/20.004 (sub 1 2) 20.004/20.004 (0) 20.004/20.004 (cons 1 2) 20.004/20.004 (fSNonEmpty) 20.004/20.004 (nil) 20.004/20.004 (s 1) 20.004/20.004 ) 20.004/20.004 (RULES 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> ssp(ys':S,v:S) 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,ssp(ys':S,sub(v:S,y:S))) 20.004/20.004 ssp(nil,0) -> nil 20.004/20.004 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 20.004/20.004 sub(z:S,0) -> z:S 20.004/20.004 ) 20.004/20.004 20.004/20.004 Problem 1: 20.004/20.004 20.004/20.004 CleanTRS Processor: 20.004/20.004 20.004/20.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.004/20.004 Confluence Problem: 20.004/20.004 (VAR v:S w:S y:S z:S ys':S) 20.004/20.004 (STRATEGY CONTEXTSENSITIVE 20.004/20.004 (ssp 1 2) 20.004/20.004 (sub 1 2) 20.004/20.004 (0) 20.004/20.004 (cons 1 2) 20.004/20.004 (fSNonEmpty) 20.004/20.004 (nil) 20.004/20.004 (s 1) 20.004/20.004 ) 20.004/20.004 (RULES 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> ssp(ys':S,v:S) 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,ssp(ys':S,sub(v:S,y:S))) 20.004/20.004 ssp(nil,0) -> nil 20.004/20.004 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 20.004/20.004 sub(z:S,0) -> z:S 20.004/20.004 ) 20.004/20.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.004/20.004 20.004/20.004 20.004/20.004 Problem 1: 20.004/20.004 20.004/20.004 Modular Confluence Combinations Decomposition Processor: 20.004/20.004 20.004/20.004 No usable combinations 20.004/20.004 20.004/20.004 Problem 1: 20.004/20.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.004/20.004 Confluence Problem: 20.004/20.004 (VAR v:S w:S y:S z:S ys':S) 20.004/20.004 (STRATEGY CONTEXTSENSITIVE 20.004/20.004 (ssp 1 2) 20.004/20.004 (sub 1 2) 20.004/20.004 (0) 20.004/20.004 (cons 1 2) 20.004/20.004 (fSNonEmpty) 20.004/20.004 (nil) 20.004/20.004 (s 1) 20.004/20.004 ) 20.004/20.004 (RULES 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> ssp(ys':S,v:S) 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,ssp(ys':S,sub(v:S,y:S))) 20.004/20.004 ssp(nil,0) -> nil 20.004/20.004 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 20.004/20.004 sub(z:S,0) -> z:S 20.004/20.004 ) 20.004/20.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.004/20.004 20.004/20.004 Huet Levy Processor: 20.004/20.004 -> Rules: 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> ssp(ys':S,v:S) 20.004/20.004 ssp(cons(y:S,ys':S),v:S) -> cons(y:S,ssp(ys':S,sub(v:S,y:S))) 20.004/20.004 ssp(nil,0) -> nil 20.004/20.004 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 20.004/20.004 sub(z:S,0) -> z:S 20.004/20.004 -> Vars: 20.004/20.004 v, y, ys', v, y, ys', v, w, z 20.004/20.004 -> FVars: 20.004/20.004 x8, x9, x10, x11, x12, x13, x14, x15, x16 20.004/20.004 -> PVars: 20.004/20.004 v: [x8, x11, x14], y: [x9, x12], ys': [x10, x13], w: [x15], z: [x16] 20.004/20.004 20.004/20.004 -> Rlps: 20.004/20.004 (rule: ssp(cons(x9:S,x10:S),x8:S) -> ssp(x10:S,x8:S), id: 1, possubterms: ssp(cons(x9:S,x10:S),x8:S)->[], cons(x9:S,x10:S)->[1]) 20.004/20.004 (rule: ssp(cons(x12:S,x13:S),x11:S) -> cons(x12:S,ssp(x13:S,sub(x11:S,x12:S))), id: 2, possubterms: ssp(cons(x12:S,x13:S),x11:S)->[], cons(x12:S,x13:S)->[1]) 20.004/20.004 (rule: ssp(nil,0) -> nil, id: 3, possubterms: ssp(nil,0)->[], nil->[1], 0->[2]) 20.004/20.004 (rule: sub(s(x14:S),s(x15:S)) -> sub(x14:S,x15:S), id: 4, possubterms: sub(s(x14:S),s(x15:S))->[], s(x14:S)->[1], s(x15:S)->[2]) 20.004/20.004 (rule: sub(x16:S,0) -> x16:S, id: 5, possubterms: sub(x16:S,0)->[], 0->[2]) 20.004/20.004 20.004/20.004 -> Unifications: 20.004/20.004 (R2 unifies with R1 at p: [], l: ssp(cons(x12:S,x13:S),x11:S), lp: ssp(cons(x12:S,x13:S),x11:S), sig: {x11:S -> v:S,x12:S -> y:S,x13:S -> ys':S}, l': ssp(cons(y:S,ys':S),v:S), r: cons(x12:S,ssp(x13:S,sub(x11:S,x12:S))), r': ssp(ys':S,v:S)) 20.004/20.004 20.004/20.004 -> Critical pairs info: 20.004/20.004 => Not trivial, Overlay, N1 20.004/20.004 20.004/20.004 -> Problem conclusions: 20.004/20.004 Left linear, Not right linear, Not linear 20.004/20.004 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 20.004/20.004 Not Huet-Levy confluent, Not Newman confluent 20.004/20.004 R is a TRS 20.004/20.004 20.004/20.004 20.004/20.004 Problem 1: 20.004/20.004 Different Normal CP Terms Processor: 20.004/20.004 => Not trivial, Overlay, N1, Normal and not trivial cp 20.004/20.004 20.004/20.004 The problem is not joinable. 20.004/20.004 0.65user 0.05system 0:20.04elapsed 3%CPU (0avgtext+0avgdata 16040maxresident)k 20.004/20.004 8inputs+0outputs (0major+11018minor)pagefaults 0swaps