16.23/4.79	YES
16.23/4.79	
16.23/4.79	Proof:
16.23/4.79	This system is confluent.
16.23/4.79	By \cite{ALS94}, Theorem 4.1.
16.23/4.79	This system is of type 3 or smaller.
16.23/4.79	This system is strongly deterministic.
16.23/4.79	This system is quasi-decreasing.
16.23/4.79	By \cite{O02}, p. 214, Proposition 7.2.50.
16.23/4.79	This system is of type 3 or smaller.
16.23/4.79	This system is deterministic.
16.23/4.79	System R transformed to optimized U(R).
16.23/4.79	This system is terminating.
16.23/4.79	Call external tool:
16.23/4.79	./ttt2.sh
16.23/4.79	Input:
16.23/4.79	  ordered(cons(m, cons(n, l))) -> ?2(lte(m, n), m, n, l)
16.23/4.79	  ?2(true, m, n, l) -> ordered(cons(n, l))
16.23/4.79	  lte(s(m), s(n)) -> lte(m, n)
16.23/4.79	  ordered(cons(m, nil)) -> true
16.23/4.79	  ordered(nil) -> true
16.23/4.79	  ordered(cons(m, cons(n, l))) -> ?2(lte(m, n), m, n, l)
16.23/4.79	  ?2(false, m, n, l) -> false
16.23/4.79	  insert(cons(n, l), m) -> ?1(lte(m, n), n, l, m)
16.23/4.79	  ?1(false, n, l, m) -> cons(n, insert(l, m))
16.23/4.79	  lte(s(m), 0) -> false
16.23/4.79	  lte(0, n) -> true
16.23/4.79	  insert(nil, m) -> cons(m, nil)
16.23/4.79	  insert(cons(n, l), m) -> ?1(lte(m, n), n, l, m)
16.23/4.79	  ?1(true, n, l, m) -> cons(m, cons(n, l))
16.23/4.79	
16.23/4.79	 DP Processor:
16.23/4.79	  DPs:
16.23/4.79	   ordered#(cons(m,cons(n,l))) -> lte#(m,n)
16.23/4.79	   ordered#(cons(m,cons(n,l))) -> ?2#(lte(m,n),m,n,l)
16.23/4.80	   ?2#(true(),m,n,l) -> ordered#(cons(n,l))
16.23/4.80	   lte#(s(m),s(n)) -> lte#(m,n)
16.23/4.80	   insert#(cons(n,l),m) -> lte#(m,n)
16.23/4.80	   insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m)
16.23/4.80	   ?1#(false(),n,l,m) -> insert#(l,m)
16.23/4.80	  TRS:
16.23/4.80	   ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
16.23/4.80	   ?2(true(),m,n,l) -> ordered(cons(n,l))
16.23/4.80	   lte(s(m),s(n)) -> lte(m,n)
16.23/4.80	   ordered(cons(m,nil())) -> true()
16.23/4.80	   ordered(nil()) -> true()
16.23/4.80	   ?2(false(),m,n,l) -> false()
16.23/4.80	   insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
16.23/4.80	   ?1(false(),n,l,m) -> cons(n,insert(l,m))
16.23/4.80	   lte(s(m),0()) -> false()
16.23/4.80	   lte(0(),n) -> true()
16.23/4.80	   insert(nil(),m) -> cons(m,nil())
16.23/4.80	   ?1(true(),n,l,m) -> cons(m,cons(n,l))
16.23/4.80	  TDG Processor:
16.23/4.80	   DPs:
16.23/4.80	    ordered#(cons(m,cons(n,l))) -> lte#(m,n)
16.23/4.80	    ordered#(cons(m,cons(n,l))) -> ?2#(lte(m,n),m,n,l)
16.23/4.80	    ?2#(true(),m,n,l) -> ordered#(cons(n,l))
16.23/4.80	    lte#(s(m),s(n)) -> lte#(m,n)
16.23/4.80	    insert#(cons(n,l),m) -> lte#(m,n)
16.23/4.80	    insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m)
16.23/4.80	    ?1#(false(),n,l,m) -> insert#(l,m)
16.23/4.80	   TRS:
16.23/4.80	    ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
16.23/4.80	    ?2(true(),m,n,l) -> ordered(cons(n,l))
16.23/4.80	    lte(s(m),s(n)) -> lte(m,n)
16.23/4.80	    ordered(cons(m,nil())) -> true()
16.23/4.80	    ordered(nil()) -> true()
16.23/4.80	    ?2(false(),m,n,l) -> false()
16.23/4.80	    insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
16.23/4.80	    ?1(false(),n,l,m) -> cons(n,insert(l,m))
16.23/4.80	    lte(s(m),0()) -> false()
16.23/4.80	    lte(0(),n) -> true()
16.23/4.80	    insert(nil(),m) -> cons(m,nil())
16.23/4.80	    ?1(true(),n,l,m) -> cons(m,cons(n,l))
16.23/4.80	   graph:
16.23/4.80	    ?1#(false(),n,l,m) -> insert#(l,m) ->
16.23/4.80	    insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m)
16.23/4.80	    ?1#(false(),n,l,m) -> insert#(l,m) ->
16.23/4.80	    insert#(cons(n,l),m) -> lte#(m,n)
16.23/4.80	    insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m) ->
16.23/4.80	    ?1#(false(),n,l,m) -> insert#(l,m)
16.23/4.80	    insert#(cons(n,l),m) -> lte#(m,n) ->
16.23/4.80	    lte#(s(m),s(n)) -> lte#(m,n)
16.23/4.80	    ?2#(true(),m,n,l) -> ordered#(cons(n,l)) ->
16.23/4.80	    ordered#(cons(m,cons(n,l))) -> ?2#(lte(m,n),m,n,l)
16.23/4.80	    ?2#(true(),m,n,l) -> ordered#(cons(n,l)) ->
16.23/4.80	    ordered#(cons(m,cons(n,l))) -> lte#(m,n)
16.23/4.80	    lte#(s(m),s(n)) -> lte#(m,n) ->
16.23/4.80	    lte#(s(m),s(n)) -> lte#(m,n)
16.23/4.80	    ordered#(cons(m,cons(n,l))) -> ?2#(lte(m,n),m,n,l) ->
16.23/4.80	    ?2#(true(),m,n,l) -> ordered#(cons(n,l))
16.23/4.80	    ordered#(cons(m,cons(n,l))) -> lte#(m,n) -> lte#(s(m),s(n)) -> lte#(m,n)
16.23/4.80	   SCC Processor:
16.23/4.80	    #sccs: 3
16.23/4.80	    #rules: 5
16.23/4.80	    #arcs: 9/49
16.23/4.80	    DPs:
16.23/4.80	     ?2#(true(),m,n,l) -> ordered#(cons(n,l))
16.23/4.80	     ordered#(cons(m,cons(n,l))) -> ?2#(lte(m,n),m,n,l)
16.23/4.80	    TRS:
16.23/4.80	     ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
16.23/4.80	     ?2(true(),m,n,l) -> ordered(cons(n,l))
16.23/4.80	     lte(s(m),s(n)) -> lte(m,n)
16.23/4.80	     ordered(cons(m,nil())) -> true()
16.23/4.80	     ordered(nil()) -> true()
16.23/4.80	     ?2(false(),m,n,l) -> false()
16.23/4.80	     insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
16.23/4.80	     ?1(false(),n,l,m) -> cons(n,insert(l,m))
16.23/4.80	     lte(s(m),0()) -> false()
16.23/4.80	     lte(0(),n) -> true()
16.23/4.80	     insert(nil(),m) -> cons(m,nil())
16.23/4.80	     ?1(true(),n,l,m) -> cons(m,cons(n,l))
16.23/4.80	    Subterm Criterion Processor:
16.23/4.80	     simple projection:
16.23/4.80	      pi(cons) = [0,0,1,1]
16.23/4.80	      pi(ordered#) = 0
16.23/4.80	      pi(?2#) = [1,2,2,3,3]
16.23/4.80	     problem:
16.23/4.80	      DPs:
16.23/4.80	       
16.23/4.80	      TRS:
16.23/4.80	       ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
16.23/4.80	       ?2(true(),m,n,l) -> ordered(cons(n,l))
16.23/4.80	       lte(s(m),s(n)) -> lte(m,n)
16.23/4.80	       ordered(cons(m,nil())) -> true()
16.23/4.80	       ordered(nil()) -> true()
16.23/4.80	       ?2(false(),m,n,l) -> false()
16.23/4.80	       insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
16.23/4.80	       ?1(false(),n,l,m) -> cons(n,insert(l,m))
16.23/4.80	       lte(s(m),0()) -> false()
16.23/4.80	       lte(0(),n) -> true()
16.23/4.80	       insert(nil(),m) -> cons(m,nil())
16.23/4.80	       ?1(true(),n,l,m) -> cons(m,cons(n,l))
16.23/4.80	     Qed
16.23/4.80	    
16.23/4.80	    DPs:
16.23/4.80	     ?1#(false(),n,l,m) -> insert#(l,m)
16.23/4.80	     insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m)
16.23/4.80	    TRS:
16.23/4.80	     ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
16.23/4.80	     ?2(true(),m,n,l) -> ordered(cons(n,l))
16.23/4.80	     lte(s(m),s(n)) -> lte(m,n)
16.23/4.80	     ordered(cons(m,nil())) -> true()
16.23/4.80	     ordered(nil()) -> true()
16.23/4.80	     ?2(false(),m,n,l) -> false()
16.23/4.80	     insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
16.23/4.80	     ?1(false(),n,l,m) -> cons(n,insert(l,m))
16.23/4.80	     lte(s(m),0()) -> false()
16.23/4.80	     lte(0(),n) -> true()
16.23/4.80	     insert(nil(),m) -> cons(m,nil())
16.23/4.80	     ?1(true(),n,l,m) -> cons(m,cons(n,l))
16.23/4.80	    Subterm Criterion Processor:
16.23/4.80	     simple projection:
16.23/4.80	      pi(insert#) = 0
16.23/4.80	      pi(?1#) = 2
16.23/4.80	     problem:
16.23/4.80	      DPs:
16.23/4.80	       ?1#(false(),n,l,m) -> insert#(l,m)
16.23/4.80	      TRS:
16.23/4.80	       ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
16.23/4.80	       ?2(true(),m,n,l) -> ordered(cons(n,l))
16.23/4.80	       lte(s(m),s(n)) -> lte(m,n)
16.23/4.80	       ordered(cons(m,nil())) -> true()
16.23/4.80	       ordered(nil()) -> true()
16.23/4.80	       ?2(false(),m,n,l) -> false()
16.23/4.80	       insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
16.23/4.80	       ?1(false(),n,l,m) -> cons(n,insert(l,m))
16.23/4.80	       lte(s(m),0()) -> false()
16.23/4.80	       lte(0(),n) -> true()
16.23/4.80	       insert(nil(),m) -> cons(m,nil())
16.23/4.80	       ?1(true(),n,l,m) -> cons(m,cons(n,l))
16.23/4.80	     SCC Processor:
16.23/4.80	      #sccs: 0
16.23/4.80	      #rules: 0
16.23/4.80	      #arcs: 2/1
16.23/4.80	      
16.23/4.80	    
16.23/4.80	    DPs:
16.23/4.80	     lte#(s(m),s(n)) -> lte#(m,n)
16.23/4.80	    TRS:
16.23/4.80	     ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
16.23/4.80	     ?2(true(),m,n,l) -> ordered(cons(n,l))
16.23/4.80	     lte(s(m),s(n)) -> lte(m,n)
16.23/4.80	     ordered(cons(m,nil())) -> true()
16.23/4.80	     ordered(nil()) -> true()
16.23/4.80	     ?2(false(),m,n,l) -> false()
16.23/4.80	     insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
16.23/4.80	     ?1(false(),n,l,m) -> cons(n,insert(l,m))
16.23/4.80	     lte(s(m),0()) -> false()
16.23/4.80	     lte(0(),n) -> true()
16.23/4.80	     insert(nil(),m) -> cons(m,nil())
16.23/4.80	     ?1(true(),n,l,m) -> cons(m,cons(n,l))
16.23/4.80	    Subterm Criterion Processor:
16.23/4.80	     simple projection:
16.23/4.80	      pi(lte#) = 0
16.23/4.80	     problem:
16.23/4.80	      DPs:
16.23/4.81	       
16.23/4.81	      TRS:
16.23/4.81	       ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
16.23/4.81	       ?2(true(),m,n,l) -> ordered(cons(n,l))
16.23/4.81	       lte(s(m),s(n)) -> lte(m,n)
16.23/4.81	       ordered(cons(m,nil())) -> true()
16.23/4.81	       ordered(nil()) -> true()
16.23/4.81	       ?2(false(),m,n,l) -> false()
16.23/4.81	       insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
16.23/4.81	       ?1(false(),n,l,m) -> cons(n,insert(l,m))
16.23/4.81	       lte(s(m),0()) -> false()
16.23/4.81	       lte(0(),n) -> true()
16.23/4.81	       insert(nil(),m) -> cons(m,nil())
16.23/4.81	       ?1(true(),n,l,m) -> cons(m,cons(n,l))
16.23/4.81	     Qed
16.23/4.81	All 4 critical pairs are joinable.
16.23/4.81	Overlap: (rule1: insert(cons(z, x), y) -> cons(z, insert(x, y)) <= lte(y, z) = false, rule2: insert(cons(z', x'), y') -> cons(y', cons(z', x')) <= lte(y', z') = true, pos: ε, mgu: {(z',z), (x',x), (y',y)})
16.23/4.81	CP: cons(y, cons(z, x)) = cons(z, insert(x, y)) <= lte(y, z) = false, lte(y, z) = true
16.23/4.81	This critical pair is unfeasible.
16.23/4.81	Overlap: (rule1: insert(cons(z, x), y) -> cons(y, cons(z, x)) <= lte(y, z) = true, rule2: insert(cons(z', x'), y') -> cons(z', insert(x', y')) <= lte(y', z') = false, pos: ε, mgu: {(z',z), (x',x), (y',y)})
16.23/4.82	CP: cons(z, insert(x, y)) = cons(y, cons(z, x)) <= lte(y, z) = true, lte(y, z) = false
16.23/4.82	This critical pair is unfeasible.
16.23/4.82	Overlap: (rule1: ordered(cons(y, cons(z, x))) -> false <= lte(y, z) = false, rule2: ordered(cons(y', cons(z', x'))) -> ordered(cons(z', x')) <= lte(y', z') = true, pos: ε, mgu: {(y',y), (z',z), (x',x)})
16.23/4.82	CP: ordered(cons(z, x)) = false <= lte(y, z) = false, lte(y, z) = true
16.23/4.82	This critical pair is unfeasible.
16.23/4.82	Overlap: (rule1: ordered(cons(y, cons(z, x))) -> ordered(cons(z, x)) <= lte(y, z) = true, rule2: ordered(cons(y', cons(z', x'))) -> false <= lte(y', z') = false, pos: ε, mgu: {(y',y), (z',z), (x',x)})
16.23/4.82	CP: false = ordered(cons(z, x)) <= lte(y, z) = true, lte(y, z) = false
16.23/4.82	This critical pair is unfeasible.
16.23/4.82	
17.18/5.05	EOF