YES Proof: This system is quasi-decreasing. By \cite{O02}, p. 214, Proposition 7.2.50. This system is of type 3 or smaller. This system is deterministic. System R transformed to U(R). Call external tool: ttt2 - trs 30 Input: le(0, s(x)) -> true le(x, 0) -> false le(s(x), s(y)) -> le(x, y) min(cons(x, nil)) -> x ?3(true, x, l) -> x min(cons(x, l)) -> ?3(le(x, min(l)), x, l) ?1(false, x, l) -> min(l) min(cons(x, l)) -> ?1(le(x, min(l)), x, l) ?2(x, x, l) -> min(l) min(cons(x, l)) -> ?2(min(l), x, l) DP Processor: DPs: le#(s(x),s(y)) -> le#(x,y) min#(cons(x,l)) -> min#(l) min#(cons(x,l)) -> le#(x,min(l)) min#(cons(x,l)) -> ?3#(le(x,min(l)),x,l) ?1#(false(),x,l) -> min#(l) min#(cons(x,l)) -> ?1#(le(x,min(l)),x,l) ?2#(x,x,l) -> min#(l) min#(cons(x,l)) -> ?2#(min(l),x,l) TRS: le(0(),s(x)) -> true() le(x,0()) -> false() le(s(x),s(y)) -> le(x,y) min(cons(x,nil())) -> x ?3(true(),x,l) -> x min(cons(x,l)) -> ?3(le(x,min(l)),x,l) ?1(false(),x,l) -> min(l) min(cons(x,l)) -> ?1(le(x,min(l)),x,l) ?2(x,x,l) -> min(l) min(cons(x,l)) -> ?2(min(l),x,l) TDG Processor: DPs: le#(s(x),s(y)) -> le#(x,y) min#(cons(x,l)) -> min#(l) min#(cons(x,l)) -> le#(x,min(l)) min#(cons(x,l)) -> ?3#(le(x,min(l)),x,l) ?1#(false(),x,l) -> min#(l) min#(cons(x,l)) -> ?1#(le(x,min(l)),x,l) ?2#(x,x,l) -> min#(l) min#(cons(x,l)) -> ?2#(min(l),x,l) TRS: le(0(),s(x)) -> true() le(x,0()) -> false() le(s(x),s(y)) -> le(x,y) min(cons(x,nil())) -> x ?3(true(),x,l) -> x min(cons(x,l)) -> ?3(le(x,min(l)),x,l) ?1(false(),x,l) -> min(l) min(cons(x,l)) -> ?1(le(x,min(l)),x,l) ?2(x,x,l) -> min(l) min(cons(x,l)) -> ?2(min(l),x,l) graph: ?2#(x,x,l) -> min#(l) -> min#(cons(x,l)) -> ?2#(min(l),x,l) ?2#(x,x,l) -> min#(l) -> min#(cons(x,l)) -> ?1#(le(x,min(l)),x,l) ?2#(x,x,l) -> min#(l) -> min#(cons(x,l)) -> ?3#(le(x,min(l)),x,l) ?2#(x,x,l) -> min#(l) -> min#(cons(x,l)) -> le#(x,min(l)) ?2#(x,x,l) -> min#(l) -> min#(cons(x,l)) -> min#(l) ?1#(false(),x,l) -> min#(l) -> min#(cons(x,l)) -> ?2#(min(l),x,l) ?1#(false(),x,l) -> min#(l) -> min#(cons(x,l)) -> ?1#(le(x,min(l)),x,l) ?1#(false(),x,l) -> min#(l) -> min#(cons(x,l)) -> ?3#(le(x,min(l)),x,l) ?1#(false(),x,l) -> min#(l) -> min#(cons(x,l)) -> le#(x,min(l)) ?1#(false(),x,l) -> min#(l) -> min#(cons(x,l)) -> min#(l) min#(cons(x,l)) -> ?2#(min(l),x,l) -> ?2#(x,x,l) -> min#(l) min#(cons(x,l)) -> ?1#(le(x,min(l)),x,l) -> ?1#(false(),x,l) -> min#(l) min#(cons(x,l)) -> min#(l) -> min#(cons(x,l)) -> ?2#(min(l),x,l) min#(cons(x,l)) -> min#(l) -> min#(cons(x,l)) -> ?1#(le(x,min(l)),x,l) min#(cons(x,l)) -> min#(l) -> min#(cons(x,l)) -> ?3#(le(x,min(l)),x,l) min#(cons(x,l)) -> min#(l) -> min#(cons(x,l)) -> le#(x,min(l)) min#(cons(x,l)) -> min#(l) -> min#(cons(x,l)) -> min#(l) min#(cons(x,l)) -> le#(x,min(l)) -> le#(s(x),s(y)) -> le#(x,y) le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) SCC Processor: #sccs: 2 #rules: 6 #arcs: 19/64 DPs: ?2#(x,x,l) -> min#(l) min#(cons(x,l)) -> min#(l) min#(cons(x,l)) -> ?1#(le(x,min(l)),x,l) ?1#(false(),x,l) -> min#(l) min#(cons(x,l)) -> ?2#(min(l),x,l) TRS: le(0(),s(x)) -> true() le(x,0()) -> false() le(s(x),s(y)) -> le(x,y) min(cons(x,nil())) -> x ?3(true(),x,l) -> x min(cons(x,l)) -> ?3(le(x,min(l)),x,l) ?1(false(),x,l) -> min(l) min(cons(x,l)) -> ?1(le(x,min(l)),x,l) ?2(x,x,l) -> min(l) min(cons(x,l)) -> ?2(min(l),x,l) Subterm Criterion Processor: simple projection: pi(min#) = 0 pi(?1#) = 2 pi(?2#) = 2 problem: DPs: ?2#(x,x,l) -> min#(l) ?1#(false(),x,l) -> min#(l) TRS: le(0(),s(x)) -> true() le(x,0()) -> false() le(s(x),s(y)) -> le(x,y) min(cons(x,nil())) -> x ?3(true(),x,l) -> x min(cons(x,l)) -> ?3(le(x,min(l)),x,l) ?1(false(),x,l) -> min(l) min(cons(x,l)) -> ?1(le(x,min(l)),x,l) ?2(x,x,l) -> min(l) min(cons(x,l)) -> ?2(min(l),x,l) SCC Processor: #sccs: 0 #rules: 0 #arcs: 11/4 DPs: le#(s(x),s(y)) -> le#(x,y) TRS: le(0(),s(x)) -> true() le(x,0()) -> false() le(s(x),s(y)) -> le(x,y) min(cons(x,nil())) -> x ?3(true(),x,l) -> x min(cons(x,l)) -> ?3(le(x,min(l)),x,l) ?1(false(),x,l) -> min(l) min(cons(x,l)) -> ?1(le(x,min(l)),x,l) ?2(x,x,l) -> min(l) min(cons(x,l)) -> ?2(min(l),x,l) Subterm Criterion Processor: simple projection: pi(le#) = 0 problem: DPs: TRS: le(0(),s(x)) -> true() le(x,0()) -> false() le(s(x),s(y)) -> le(x,y) min(cons(x,nil())) -> x ?3(true(),x,l) -> x min(cons(x,l)) -> ?3(le(x,min(l)),x,l) ?1(false(),x,l) -> min(l) min(cons(x,l)) -> ?1(le(x,min(l)),x,l) ?2(x,x,l) -> min(l) min(cons(x,l)) -> ?2(min(l),x,l) Qed