13.30/4.37	YES
13.30/4.37	
13.30/4.37	Proof:
13.30/4.37	This system is confluent.
13.30/4.37	By \cite{ALS94}, Theorem 4.1.
13.30/4.37	This system is of type 3 or smaller.
13.30/4.37	This system is strongly deterministic.
13.30/4.37	This system is quasi-decreasing.
13.30/4.37	By \cite{O02}, p. 214, Proposition 7.2.50.
13.30/4.37	This system is of type 3 or smaller.
13.30/4.37	This system is deterministic.
13.30/4.37	System R transformed to optimized U(R).
13.30/4.37	This system is terminating.
13.30/4.37	Call external tool:
13.30/4.37	./ttt2.sh
13.30/4.37	Input:
13.30/4.37	(VAR m n l)
13.30/4.37	(RULES
13.30/4.37	  ordered(cons(m, cons(n, l))) -> ?2(lte(m, n), m, n, l)
13.30/4.37	  ?2(true, m, n, l) -> ordered(cons(n, l))
13.30/4.37	  lte(s(m), s(n)) -> lte(m, n)
13.30/4.37	  ordered(cons(m, nil)) -> true
13.30/4.37	  ordered(nil) -> true
13.30/4.37	  ordered(cons(m, cons(n, l))) -> ?2(lte(m, n), m, n, l)
13.30/4.37	  ?2(false, m, n, l) -> false
13.30/4.37	  insert(cons(n, l), m) -> ?1(lte(m, n), n, l, m)
13.30/4.37	  ?1(false, n, l, m) -> cons(n, insert(l, m))
13.30/4.37	  lte(s(m), 0) -> false
13.30/4.37	  lte(0, n) -> true
13.30/4.37	  insert(nil, m) -> cons(m, nil)
13.30/4.37	  insert(cons(n, l), m) -> ?1(lte(m, n), n, l, m)
13.30/4.37	  ?1(true, n, l, m) -> cons(m, cons(n, l))
13.30/4.37	)
13.30/4.37	
13.30/4.37	 DP Processor:
13.30/4.37	  DPs:
13.30/4.37	   ordered#(cons(m,cons(n,l))) -> lte#(m,n)
13.30/4.37	   ordered#(cons(m,cons(n,l))) -> ?2#(lte(m,n),m,n,l)
13.30/4.37	   ?2#(true(),m,n,l) -> ordered#(cons(n,l))
13.30/4.37	   lte#(s(m),s(n)) -> lte#(m,n)
13.30/4.37	   insert#(cons(n,l),m) -> lte#(m,n)
13.30/4.37	   insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m)
13.30/4.37	   ?1#(false(),n,l,m) -> insert#(l,m)
13.30/4.37	  TRS:
13.30/4.37	   ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
13.30/4.37	   ?2(true(),m,n,l) -> ordered(cons(n,l))
13.30/4.37	   lte(s(m),s(n)) -> lte(m,n)
13.30/4.37	   ordered(cons(m,nil())) -> true()
13.30/4.37	   ordered(nil()) -> true()
13.30/4.37	   ?2(false(),m,n,l) -> false()
13.30/4.37	   insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
13.30/4.37	   ?1(false(),n,l,m) -> cons(n,insert(l,m))
13.30/4.37	   lte(s(m),0()) -> false()
13.30/4.37	   lte(0(),n) -> true()
13.30/4.37	   insert(nil(),m) -> cons(m,nil())
13.30/4.37	   ?1(true(),n,l,m) -> cons(m,cons(n,l))
13.30/4.37	  TDG Processor:
13.30/4.37	   DPs:
13.30/4.37	    ordered#(cons(m,cons(n,l))) -> lte#(m,n)
13.30/4.37	    ordered#(cons(m,cons(n,l))) -> ?2#(lte(m,n),m,n,l)
13.30/4.37	    ?2#(true(),m,n,l) -> ordered#(cons(n,l))
13.30/4.37	    lte#(s(m),s(n)) -> lte#(m,n)
13.30/4.37	    insert#(cons(n,l),m) -> lte#(m,n)
13.30/4.37	    insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m)
13.30/4.37	    ?1#(false(),n,l,m) -> insert#(l,m)
13.30/4.37	   TRS:
13.30/4.37	    ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
13.30/4.37	    ?2(true(),m,n,l) -> ordered(cons(n,l))
13.30/4.37	    lte(s(m),s(n)) -> lte(m,n)
13.30/4.37	    ordered(cons(m,nil())) -> true()
13.30/4.37	    ordered(nil()) -> true()
13.30/4.37	    ?2(false(),m,n,l) -> false()
13.30/4.37	    insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
13.30/4.37	    ?1(false(),n,l,m) -> cons(n,insert(l,m))
13.30/4.37	    lte(s(m),0()) -> false()
13.30/4.37	    lte(0(),n) -> true()
13.30/4.37	    insert(nil(),m) -> cons(m,nil())
13.30/4.37	    ?1(true(),n,l,m) -> cons(m,cons(n,l))
13.30/4.37	   graph:
13.30/4.37	    ?1#(false(),n,l,m) -> insert#(l,m) ->
13.30/4.37	    insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m)
13.30/4.37	    ?1#(false(),n,l,m) -> insert#(l,m) ->
13.30/4.37	    insert#(cons(n,l),m) -> lte#(m,n)
13.30/4.37	    insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m) ->
13.30/4.37	    ?1#(false(),n,l,m) -> insert#(l,m)
13.30/4.37	    insert#(cons(n,l),m) -> lte#(m,n) ->
13.30/4.37	    lte#(s(m),s(n)) -> lte#(m,n)
13.30/4.37	    ?2#(true(),m,n,l) -> ordered#(cons(n,l)) ->
13.30/4.37	    ordered#(cons(m,cons(n,l))) -> ?2#(lte(m,n),m,n,l)
13.30/4.37	    ?2#(true(),m,n,l) -> ordered#(cons(n,l)) ->
13.30/4.37	    ordered#(cons(m,cons(n,l))) -> lte#(m,n)
13.30/4.37	    lte#(s(m),s(n)) -> lte#(m,n) ->
13.30/4.37	    lte#(s(m),s(n)) -> lte#(m,n)
13.30/4.37	    ordered#(cons(m,cons(n,l))) -> ?2#(lte(m,n),m,n,l) ->
13.30/4.37	    ?2#(true(),m,n,l) -> ordered#(cons(n,l))
13.30/4.37	    ordered#(cons(m,cons(n,l))) -> lte#(m,n) -> lte#(s(m),s(n)) -> lte#(m,n)
13.30/4.37	   SCC Processor:
13.30/4.37	    #sccs: 3
13.30/4.37	    #rules: 5
13.30/4.38	    #arcs: 9/49
13.30/4.38	    DPs:
13.30/4.38	     ?2#(true(),m,n,l) -> ordered#(cons(n,l))
13.30/4.38	     ordered#(cons(m,cons(n,l))) -> ?2#(lte(m,n),m,n,l)
13.30/4.38	    TRS:
13.30/4.38	     ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
13.30/4.38	     ?2(true(),m,n,l) -> ordered(cons(n,l))
13.30/4.38	     lte(s(m),s(n)) -> lte(m,n)
13.30/4.38	     ordered(cons(m,nil())) -> true()
13.30/4.38	     ordered(nil()) -> true()
13.30/4.38	     ?2(false(),m,n,l) -> false()
13.30/4.38	     insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
13.30/4.38	     ?1(false(),n,l,m) -> cons(n,insert(l,m))
13.30/4.38	     lte(s(m),0()) -> false()
13.30/4.38	     lte(0(),n) -> true()
13.30/4.38	     insert(nil(),m) -> cons(m,nil())
13.30/4.38	     ?1(true(),n,l,m) -> cons(m,cons(n,l))
13.30/4.38	    Subterm Criterion Processor:
13.30/4.38	     simple projection:
13.30/4.38	      pi(cons) = [0,0,1,1]
13.30/4.38	      pi(ordered#) = 0
13.30/4.38	      pi(?2#) = [1,2,2,3,3]
13.30/4.38	     problem:
13.30/4.38	      DPs:
13.30/4.38	       
13.30/4.38	      TRS:
13.30/4.38	       ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
13.30/4.38	       ?2(true(),m,n,l) -> ordered(cons(n,l))
13.30/4.38	       lte(s(m),s(n)) -> lte(m,n)
13.30/4.38	       ordered(cons(m,nil())) -> true()
13.30/4.38	       ordered(nil()) -> true()
13.30/4.38	       ?2(false(),m,n,l) -> false()
13.30/4.38	       insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
13.30/4.38	       ?1(false(),n,l,m) -> cons(n,insert(l,m))
13.30/4.38	       lte(s(m),0()) -> false()
13.30/4.38	       lte(0(),n) -> true()
13.30/4.38	       insert(nil(),m) -> cons(m,nil())
13.30/4.38	       ?1(true(),n,l,m) -> cons(m,cons(n,l))
13.30/4.38	     Qed
13.30/4.38	    
13.30/4.38	    DPs:
13.30/4.38	     ?1#(false(),n,l,m) -> insert#(l,m)
13.30/4.38	     insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m)
13.30/4.38	    TRS:
13.30/4.38	     ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
13.30/4.38	     ?2(true(),m,n,l) -> ordered(cons(n,l))
13.30/4.38	     lte(s(m),s(n)) -> lte(m,n)
13.30/4.38	     ordered(cons(m,nil())) -> true()
13.30/4.38	     ordered(nil()) -> true()
13.30/4.39	     ?2(false(),m,n,l) -> false()
13.30/4.39	     insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
13.30/4.39	     ?1(false(),n,l,m) -> cons(n,insert(l,m))
13.30/4.39	     lte(s(m),0()) -> false()
13.30/4.39	     lte(0(),n) -> true()
13.30/4.39	     insert(nil(),m) -> cons(m,nil())
13.30/4.39	     ?1(true(),n,l,m) -> cons(m,cons(n,l))
13.30/4.39	    Subterm Criterion Processor:
13.30/4.39	     simple projection:
13.30/4.39	      pi(insert#) = 0
13.30/4.39	      pi(?1#) = 2
13.30/4.39	     problem:
13.30/4.39	      DPs:
13.30/4.39	       ?1#(false(),n,l,m) -> insert#(l,m)
13.30/4.39	      TRS:
13.30/4.39	       ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
13.30/4.39	       ?2(true(),m,n,l) -> ordered(cons(n,l))
13.30/4.39	       lte(s(m),s(n)) -> lte(m,n)
13.30/4.39	       ordered(cons(m,nil())) -> true()
13.30/4.39	       ordered(nil()) -> true()
13.30/4.39	       ?2(false(),m,n,l) -> false()
13.30/4.39	       insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
13.30/4.39	       ?1(false(),n,l,m) -> cons(n,insert(l,m))
13.30/4.39	       lte(s(m),0()) -> false()
13.30/4.39	       lte(0(),n) -> true()
13.30/4.39	       insert(nil(),m) -> cons(m,nil())
13.30/4.40	       ?1(true(),n,l,m) -> cons(m,cons(n,l))
13.30/4.40	     SCC Processor:
13.30/4.40	      #sccs: 0
13.30/4.40	      #rules: 0
13.30/4.40	      #arcs: 2/1
13.30/4.40	      
13.30/4.40	    
13.30/4.40	    DPs:
13.30/4.40	     lte#(s(m),s(n)) -> lte#(m,n)
13.30/4.40	    TRS:
13.30/4.40	     ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
13.30/4.40	     ?2(true(),m,n,l) -> ordered(cons(n,l))
13.30/4.40	     lte(s(m),s(n)) -> lte(m,n)
13.30/4.40	     ordered(cons(m,nil())) -> true()
13.30/4.40	     ordered(nil()) -> true()
13.30/4.40	     ?2(false(),m,n,l) -> false()
13.30/4.40	     insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
13.30/4.40	     ?1(false(),n,l,m) -> cons(n,insert(l,m))
13.30/4.40	     lte(s(m),0()) -> false()
13.30/4.40	     lte(0(),n) -> true()
13.30/4.40	     insert(nil(),m) -> cons(m,nil())
13.30/4.40	     ?1(true(),n,l,m) -> cons(m,cons(n,l))
13.30/4.40	    Subterm Criterion Processor:
13.30/4.40	     simple projection:
13.30/4.40	      pi(lte#) = 0
13.30/4.40	     problem:
13.30/4.40	      DPs:
13.30/4.40	       
13.30/4.40	      TRS:
13.30/4.40	       ordered(cons(m,cons(n,l))) -> ?2(lte(m,n),m,n,l)
13.30/4.40	       ?2(true(),m,n,l) -> ordered(cons(n,l))
13.30/4.40	       lte(s(m),s(n)) -> lte(m,n)
13.30/4.40	       ordered(cons(m,nil())) -> true()
13.30/4.40	       ordered(nil()) -> true()
13.30/4.40	       ?2(false(),m,n,l) -> false()
13.30/4.40	       insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
13.30/4.41	       ?1(false(),n,l,m) -> cons(n,insert(l,m))
13.30/4.41	       lte(s(m),0()) -> false()
13.30/4.41	       lte(0(),n) -> true()
13.30/4.41	       insert(nil(),m) -> cons(m,nil())
13.30/4.41	       ?1(true(),n,l,m) -> cons(m,cons(n,l))
13.30/4.41	     Qed
13.30/4.41	All 4 critical pairs are joinable.
13.30/4.41	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')})
13.30/4.41	CP: cons(y', cons(z', x')) = cons(z', insert(x', y')) <= lte(y', z') = false, lte(y', z') = true
13.30/4.41	This critical pair is unfeasible.
13.30/4.41	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')})
13.30/4.41	CP: cons(z', insert(x', y')) = cons(y', cons(z', x')) <= lte(y', z') = true, lte(y', z') = false
13.30/4.41	This critical pair is unfeasible.
13.30/4.41	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')})
13.30/4.41	CP: ordered(cons(z', x')) = false <= lte(y', z') = false, lte(y', z') = true
13.30/4.41	This critical pair is unfeasible.
13.30/4.41	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')})
13.30/4.41	CP: false = ordered(cons(z', x')) <= lte(y', z') = true, lte(y', z') = false
13.30/4.41	This critical pair is unfeasible.
13.30/4.41	
13.56/4.47	EOF