11.69/3.55 YES 11.69/3.55 11.69/3.55 Problem: 11.69/3.55 split(x, nil()) -> tp2(nil(), nil()) 11.69/3.55 split(x, cons(y, ys)) -> tp2(zs1, cons(y, zs2)) <= split(x, ys) = tp2(zs1, zs2), le(x, y) = true() 11.69/3.55 split(x, cons(y, ys)) -> tp2(cons(y, zs1), zs2) <= split(x, ys) = tp2(zs1, zs2), le(x, y) = false() 11.69/3.55 le(0(), y) -> true() 11.69/3.55 le(s(x), 0()) -> false() 11.69/3.55 le(s(x), s(y)) -> le(x, y) 11.69/3.55 11.69/3.55 Proof: 11.69/3.55 This system is confluent. 11.69/3.55 By \cite{ALS94}, Theorem 4.1. 11.69/3.55 This system is of type 3 or smaller. 11.69/3.55 This system is strongly deterministic. 11.69/3.55 All 2 critical pairs are joinable. 11.69/3.55 CP: tp2($7, cons($6, y)) = tp2(cons($6, x), $3) <= split($5, $8) = tp2(x, $3), le($5, $6) = false(), split($5, $8) = tp2($7, y), le($5, $6) = true(): 11.69/3.55 This critical pair is unfeasible. 11.69/3.55 CP: tp2(cons($6, $7), y) = tp2(x, cons($6, $3)) <= split($5, $8) = tp2(x, $3), le($5, $6) = true(), split($5, $8) = tp2($7, y), le($5, $6) = false(): 11.69/3.55 This critical pair is unfeasible. 11.69/3.55 This system is quasi-decreasing. 11.69/3.55 By \cite{O02}, p. 214, Proposition 7.2.50. 11.69/3.55 This system is of type 3 or smaller. 11.69/3.55 This system is deterministic. 11.69/3.55 System R transformed to U(R). 11.69/3.55 This system is terminating. 11.69/3.55 Call external tool: 11.69/3.55 ./ttt2.sh 11.69/3.55 Input: 11.69/3.55 split(x, nil()) -> tp2(nil(), nil()) 11.69/3.55 ?4(true(), zs2, x, ys, zs1, y) -> tp2(zs1, cons(y, zs2)) 11.69/3.55 ?3(tp2(zs1, zs2), x, y, ys) -> ?4(le(x, y), zs2, x, ys, zs1, y) 11.69/3.55 split(x, cons(y, ys)) -> ?3(split(x, ys), x, y, ys) 11.69/3.55 ?2(false(), zs2, x, ys, zs1, y) -> tp2(cons(y, zs1), zs2) 11.69/3.55 ?1(tp2(zs1, zs2), x, y, ys) -> ?2(le(x, y), zs2, x, ys, zs1, y) 11.69/3.55 split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys) 11.69/3.55 le(0(), y) -> true() 11.69/3.55 le(s(x), 0()) -> false() 11.69/3.55 le(s(x), s(y)) -> le(x, y) 11.69/3.55 11.69/3.55 DP Processor: 11.69/3.55 DPs: 11.69/3.55 ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) 11.69/3.55 ?3#(tp2(zs1,zs2),x,y,ys) -> ?4#(le(x,y),zs2,x,ys,zs1,y) 11.69/3.55 split#(x,cons(y,ys)) -> split#(x,ys) 11.69/3.55 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) 11.69/3.55 ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) 11.69/3.55 ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y) 11.69/3.55 split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) 11.69/3.55 le#(s(x),s(y)) -> le#(x,y) 11.69/3.55 TRS: 11.69/3.55 split(x,nil()) -> tp2(nil(),nil()) 11.69/3.55 ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2)) 11.69/3.55 ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y) 11.69/3.55 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 11.69/3.55 ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2) 11.69/3.55 ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y) 11.69/3.55 split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys) 11.69/3.55 le(0(),y) -> true() 11.69/3.55 le(s(x),0()) -> false() 11.69/3.55 le(s(x),s(y)) -> le(x,y) 11.69/3.55 TDG Processor: 11.69/3.55 DPs: 11.69/3.55 ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) 11.69/3.55 ?3#(tp2(zs1,zs2),x,y,ys) -> ?4#(le(x,y),zs2,x,ys,zs1,y) 11.69/3.55 split#(x,cons(y,ys)) -> split#(x,ys) 11.69/3.55 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) 11.69/3.55 ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) 11.69/3.55 ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y) 11.69/3.55 split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) 11.69/3.55 le#(s(x),s(y)) -> le#(x,y) 11.69/3.55 TRS: 11.69/3.55 split(x,nil()) -> tp2(nil(),nil()) 11.69/3.55 ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2)) 11.69/3.55 ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y) 11.69/3.55 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 11.69/3.55 ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2) 11.69/3.55 ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y) 11.69/3.55 split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys) 11.69/3.55 le(0(),y) -> true() 11.69/3.55 le(s(x),0()) -> false() 11.69/3.55 le(s(x),s(y)) -> le(x,y) 11.69/3.55 graph: 11.69/3.55 ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) 11.69/3.55 le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) 11.69/3.55 ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) -> 11.69/3.55 le#(s(x),s(y)) -> le#(x,y) 11.69/3.55 split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) -> 11.69/3.55 ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y) 11.69/3.55 split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) -> 11.69/3.55 ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) 11.69/3.55 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) -> 11.69/3.55 ?3#(tp2(zs1,zs2),x,y,ys) -> ?4#(le(x,y),zs2,x,ys,zs1,y) 11.69/3.55 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) -> 11.69/3.55 ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) 11.69/3.55 split#(x,cons(y,ys)) -> split#(x,ys) -> 11.69/3.55 split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) 11.69/3.55 split#(x,cons(y,ys)) -> split#(x,ys) -> 11.69/3.55 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) 11.69/3.55 split#(x,cons(y,ys)) -> split#(x,ys) -> split#(x,cons(y,ys)) -> split#(x,ys) 11.69/3.55 SCC Processor: 11.69/3.56 #sccs: 2 11.69/3.56 #rules: 2 11.69/3.56 #arcs: 10/64 11.69/3.56 DPs: 11.69/3.56 split#(x,cons(y,ys)) -> split#(x,ys) 11.69/3.56 TRS: 11.69/3.56 split(x,nil()) -> tp2(nil(),nil()) 11.69/3.56 ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2)) 11.69/3.56 ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y) 11.69/3.56 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 11.69/3.56 ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2) 11.69/3.56 ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y) 11.69/3.56 split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys) 11.69/3.56 le(0(),y) -> true() 11.69/3.56 le(s(x),0()) -> false() 11.69/3.56 le(s(x),s(y)) -> le(x,y) 11.69/3.56 Subterm Criterion Processor: 11.69/3.56 simple projection: 11.69/3.56 pi(split#) = 1 11.69/3.56 problem: 11.69/3.56 DPs: 11.69/3.56 11.69/3.56 TRS: 11.69/3.56 split(x,nil()) -> tp2(nil(),nil()) 11.69/3.56 ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2)) 11.69/3.56 ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y) 11.69/3.56 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 11.69/3.56 ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2) 11.69/3.56 ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y) 11.69/3.56 split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys) 11.69/3.56 le(0(),y) -> true() 11.69/3.56 le(s(x),0()) -> false() 11.69/3.56 le(s(x),s(y)) -> le(x,y) 11.69/3.56 Qed 11.69/3.56 11.69/3.56 DPs: 11.69/3.56 le#(s(x),s(y)) -> le#(x,y) 11.69/3.56 TRS: 11.69/3.56 split(x,nil()) -> tp2(nil(),nil()) 11.69/3.56 ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2)) 11.69/3.56 ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y) 11.69/3.56 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 11.69/3.56 ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2) 11.69/3.56 ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y) 11.69/3.56 split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys) 11.69/3.56 le(0(),y) -> true() 11.69/3.56 le(s(x),0()) -> false() 11.69/3.56 le(s(x),s(y)) -> le(x,y) 11.69/3.56 Subterm Criterion Processor: 11.69/3.56 simple projection: 11.69/3.56 pi(le#) = 0 11.69/3.56 problem: 11.69/3.56 DPs: 11.69/3.56 11.69/3.56 TRS: 11.69/3.56 split(x,nil()) -> tp2(nil(),nil()) 11.69/3.56 ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2)) 11.69/3.56 ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y) 11.69/3.56 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 11.69/3.56 ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2) 11.69/3.56 ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y) 11.69/3.56 split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys) 11.69/3.56 le(0(),y) -> true() 11.69/3.56 le(s(x),0()) -> false() 11.69/3.56 le(s(x),s(y)) -> le(x,y) 11.69/3.56 Qed 11.69/3.56 13.23/4.02 EOF