27.68/7.95	YES
27.68/7.95	
27.68/7.95	Problem:
27.68/7.95	lte(0(), n) -> true()
27.68/7.95	lte(s(m), 0()) -> false()
27.68/7.95	lte(s(m), s(n)) -> lte(m, n)
27.68/7.95	insert(nil(), m) -> cons(m, nil())
27.68/7.95	insert(cons(n, l), m) -> cons(m, cons(n, l)) <= lte(m, n) = true()
27.68/7.95	insert(cons(n, l), m) -> cons(n, insert(l, m)) <= lte(m, n) = false()
27.68/7.95	ordered(nil()) -> true()
27.68/7.95	ordered(cons(m, nil())) -> true()
27.68/7.95	ordered(cons(m, cons(n, l))) -> ordered(cons(n, l)) <= lte(m, n) = true()
27.68/7.95	ordered(cons(m, cons(n, l))) -> false() <= lte(m, n) = false()
27.68/7.95	
27.68/7.95	Proof:
27.68/7.95	This system is confluent.
27.68/7.95	By \cite{ALS94}, Theorem 4.1.
27.68/7.95	This system is of type 3 or smaller.
27.68/7.95	This system is strongly deterministic.
27.68/7.95	All 4 critical pairs are joinable.
27.68/7.95	CP: cons(x', cons(y', z')) = cons(y', insert(z', x')) <= lte(x', y') = false(), lte(x', y') = true():
27.68/7.95	This critical pair is unfeasible.
27.68/7.95	CP: cons(x', insert(y', z')) = cons(z', cons(x', y')) <= lte(z', x') = true(), lte(z', x') = false():
27.68/7.95	This critical pair is unfeasible.
27.68/7.95	CP: ordered(cons(x', y')) = false() <= lte(z', x') = false(), lte(z', x') = true():
27.68/7.95	This critical pair is unfeasible.
27.68/7.95	CP: false() = ordered(cons(x', y')) <= lte(z', x') = true(), lte(z', x') = false():
27.68/7.95	This critical pair is unfeasible.
27.68/7.95	This system is quasi-decreasing.
27.68/7.95	By \cite{O02}, p. 214, Proposition 7.2.50.
27.68/7.95	This system is of type 3 or smaller.
27.68/7.95	This system is deterministic.
27.68/7.95	System R transformed to U(R).
27.68/7.95	This system is terminating.
27.68/7.95	Call external tool:
27.68/7.95	./ttt2.sh
27.68/7.95	Input:
27.68/7.95	  lte(0(), n) -> true()
27.68/7.95	  lte(s(m), 0()) -> false()
27.68/7.95	  lte(s(m), s(n)) -> lte(m, n)
27.68/7.95	  insert(nil(), m) -> cons(m, nil())
27.68/7.95	  ?1(true(), n, l, m) -> cons(m, cons(n, l))
27.68/7.95	  insert(cons(n, l), m) -> ?1(lte(m, n), n, l, m)
27.68/7.95	  ?2(false(), n, l, m) -> cons(n, insert(l, m))
27.68/7.95	  insert(cons(n, l), m) -> ?2(lte(m, n), n, l, m)
27.68/7.95	  ordered(nil()) -> true()
27.68/7.95	  ordered(cons(m, nil())) -> true()
27.68/7.95	  ?4(true(), m, n, l) -> ordered(cons(n, l))
27.68/7.95	  ordered(cons(m, cons(n, l))) -> ?4(lte(m, n), m, n, l)
27.68/7.95	  ?3(false(), m, n, l) -> false()
27.68/7.95	  ordered(cons(m, cons(n, l))) -> ?3(lte(m, n), m, n, l)
27.68/7.95	
27.68/7.95	 DP Processor:
27.68/7.95	  DPs:
27.68/7.95	   lte#(s(m),s(n)) -> lte#(m,n)
27.68/7.95	   insert#(cons(n,l),m) -> lte#(m,n)
27.68/7.95	   insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m)
27.68/7.95	   ?2#(false(),n,l,m) -> insert#(l,m)
27.68/7.95	   insert#(cons(n,l),m) -> ?2#(lte(m,n),n,l,m)
27.68/7.95	   ?4#(true(),m,n,l) -> ordered#(cons(n,l))
27.68/7.95	   ordered#(cons(m,cons(n,l))) -> lte#(m,n)
27.68/7.95	   ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l)
27.68/7.95	   ordered#(cons(m,cons(n,l))) -> ?3#(lte(m,n),m,n,l)
27.68/7.95	  TRS:
27.68/7.95	   lte(0(),n) -> true()
27.68/7.95	   lte(s(m),0()) -> false()
27.68/7.95	   lte(s(m),s(n)) -> lte(m,n)
27.68/7.95	   insert(nil(),m) -> cons(m,nil())
27.68/7.95	   ?1(true(),n,l,m) -> cons(m,cons(n,l))
27.68/7.95	   insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
27.68/7.95	   ?2(false(),n,l,m) -> cons(n,insert(l,m))
27.68/7.95	   insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m)
27.68/7.95	   ordered(nil()) -> true()
27.68/7.95	   ordered(cons(m,nil())) -> true()
27.68/7.95	   ?4(true(),m,n,l) -> ordered(cons(n,l))
27.68/7.95	   ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l)
27.68/7.95	   ?3(false(),m,n,l) -> false()
27.68/7.95	   ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l)
27.68/7.95	  TDG Processor:
27.68/7.95	   DPs:
27.68/7.95	    lte#(s(m),s(n)) -> lte#(m,n)
27.68/7.95	    insert#(cons(n,l),m) -> lte#(m,n)
27.68/7.95	    insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m)
27.68/7.95	    ?2#(false(),n,l,m) -> insert#(l,m)
27.68/7.96	    insert#(cons(n,l),m) -> ?2#(lte(m,n),n,l,m)
27.68/7.96	    ?4#(true(),m,n,l) -> ordered#(cons(n,l))
27.68/7.96	    ordered#(cons(m,cons(n,l))) -> lte#(m,n)
27.68/7.96	    ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l)
27.68/7.96	    ordered#(cons(m,cons(n,l))) -> ?3#(lte(m,n),m,n,l)
27.68/7.96	   TRS:
27.68/7.96	    lte(0(),n) -> true()
27.68/7.96	    lte(s(m),0()) -> false()
27.68/7.96	    lte(s(m),s(n)) -> lte(m,n)
27.68/7.96	    insert(nil(),m) -> cons(m,nil())
27.68/7.96	    ?1(true(),n,l,m) -> cons(m,cons(n,l))
27.68/7.96	    insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
27.68/7.96	    ?2(false(),n,l,m) -> cons(n,insert(l,m))
27.68/7.96	    insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m)
27.68/7.96	    ordered(nil()) -> true()
27.68/7.96	    ordered(cons(m,nil())) -> true()
27.68/7.96	    ?4(true(),m,n,l) -> ordered(cons(n,l))
27.68/7.96	    ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l)
27.68/7.96	    ?3(false(),m,n,l) -> false()
27.68/7.96	    ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l)
27.68/7.96	   graph:
27.68/7.96	    ?4#(true(),m,n,l) -> ordered#(cons(n,l)) ->
27.68/7.96	    ordered#(cons(m,cons(n,l))) -> ?3#(lte(m,n),m,n,l)
27.68/7.96	    ?4#(true(),m,n,l) -> ordered#(cons(n,l)) ->
27.68/7.96	    ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l)
27.68/7.96	    ?4#(true(),m,n,l) -> ordered#(cons(n,l)) ->
27.68/7.96	    ordered#(cons(m,cons(n,l))) -> lte#(m,n)
27.68/7.96	    ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l) ->
27.68/7.96	    ?4#(true(),m,n,l) -> ordered#(cons(n,l))
27.68/7.96	    ordered#(cons(m,cons(n,l))) -> lte#(m,n) ->
27.68/7.96	    lte#(s(m),s(n)) -> lte#(m,n)
27.68/7.96	    ?2#(false(),n,l,m) -> insert#(l,m) ->
27.68/7.96	    insert#(cons(n,l),m) -> ?2#(lte(m,n),n,l,m)
27.68/7.96	    ?2#(false(),n,l,m) -> insert#(l,m) ->
27.68/7.96	    insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m)
27.68/7.96	    ?2#(false(),n,l,m) -> insert#(l,m) ->
27.68/7.96	    insert#(cons(n,l),m) -> lte#(m,n)
27.68/7.96	    insert#(cons(n,l),m) -> ?2#(lte(m,n),n,l,m) ->
27.68/7.96	    ?2#(false(),n,l,m) -> insert#(l,m)
27.68/7.96	    insert#(cons(n,l),m) -> lte#(m,n) -> lte#(s(m),s(n)) -> lte#(m,n)
27.68/7.96	    lte#(s(m),s(n)) -> lte#(m,n) -> lte#(s(m),s(n)) -> lte#(m,n)
27.68/7.96	   SCC Processor:
27.68/7.96	    #sccs: 3
27.68/7.96	    #rules: 5
27.68/7.96	    #arcs: 11/81
27.68/7.96	    DPs:
27.68/7.96	     ?2#(false(),n,l,m) -> insert#(l,m)
27.68/7.96	     insert#(cons(n,l),m) -> ?2#(lte(m,n),n,l,m)
27.68/7.96	    TRS:
27.68/7.96	     lte(0(),n) -> true()
27.68/7.96	     lte(s(m),0()) -> false()
27.68/7.96	     lte(s(m),s(n)) -> lte(m,n)
27.68/7.96	     insert(nil(),m) -> cons(m,nil())
27.68/7.96	     ?1(true(),n,l,m) -> cons(m,cons(n,l))
27.68/7.96	     insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
27.68/7.96	     ?2(false(),n,l,m) -> cons(n,insert(l,m))
27.68/7.96	     insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m)
27.68/7.96	     ordered(nil()) -> true()
27.68/7.96	     ordered(cons(m,nil())) -> true()
27.68/7.96	     ?4(true(),m,n,l) -> ordered(cons(n,l))
27.68/7.96	     ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l)
27.68/7.96	     ?3(false(),m,n,l) -> false()
27.68/7.96	     ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l)
27.68/7.96	    Subterm Criterion Processor:
27.68/7.96	     simple projection:
27.68/7.96	      pi(insert#) = 0
27.68/7.96	      pi(?2#) = 2
27.68/7.96	     problem:
27.68/7.96	      DPs:
27.68/7.96	       ?2#(false(),n,l,m) -> insert#(l,m)
27.68/7.96	      TRS:
27.68/7.96	       lte(0(),n) -> true()
27.68/7.96	       lte(s(m),0()) -> false()
27.68/7.96	       lte(s(m),s(n)) -> lte(m,n)
27.68/7.96	       insert(nil(),m) -> cons(m,nil())
27.68/7.96	       ?1(true(),n,l,m) -> cons(m,cons(n,l))
27.68/7.96	       insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
27.68/7.96	       ?2(false(),n,l,m) -> cons(n,insert(l,m))
27.68/7.96	       insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m)
27.68/7.96	       ordered(nil()) -> true()
27.68/7.96	       ordered(cons(m,nil())) -> true()
27.68/7.96	       ?4(true(),m,n,l) -> ordered(cons(n,l))
27.68/7.96	       ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l)
27.68/7.96	       ?3(false(),m,n,l) -> false()
27.68/7.96	       ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l)
27.68/7.96	     SCC Processor:
27.68/7.96	      #sccs: 0
27.68/7.96	      #rules: 0
27.68/7.96	      #arcs: 2/1
27.68/7.96	      
27.68/7.96	    
27.68/7.96	    DPs:
27.68/7.96	     ?4#(true(),m,n,l) -> ordered#(cons(n,l))
27.68/7.96	     ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l)
27.68/7.96	    TRS:
27.68/7.96	     lte(0(),n) -> true()
27.68/7.96	     lte(s(m),0()) -> false()
27.68/7.96	     lte(s(m),s(n)) -> lte(m,n)
27.68/7.96	     insert(nil(),m) -> cons(m,nil())
27.68/7.96	     ?1(true(),n,l,m) -> cons(m,cons(n,l))
27.68/7.96	     insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
27.68/7.96	     ?2(false(),n,l,m) -> cons(n,insert(l,m))
27.68/7.96	     insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m)
27.68/7.96	     ordered(nil()) -> true()
27.68/7.96	     ordered(cons(m,nil())) -> true()
27.68/7.96	     ?4(true(),m,n,l) -> ordered(cons(n,l))
27.68/7.96	     ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l)
27.68/7.96	     ?3(false(),m,n,l) -> false()
27.68/7.96	     ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l)
27.68/7.96	    Usable Rule Processor:
27.68/7.96	     DPs:
27.68/7.96	      ?4#(true(),m,n,l) -> ordered#(cons(n,l))
27.68/7.96	      ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l)
27.68/7.96	     TRS:
27.68/7.96	      lte(0(),n) -> true()
27.68/7.96	      lte(s(m),0()) -> false()
27.68/7.96	      lte(s(m),s(n)) -> lte(m,n)
27.68/7.96	     Arctic Interpretation Processor:
29.30/8.12	      dimension: 1
29.30/8.12	      usable rules:
29.30/8.12	       lte(0(),n) -> true()
29.30/8.12	       lte(s(m),0()) -> false()
29.30/8.12	       lte(s(m),s(n)) -> lte(m,n)
29.30/8.12	      interpretation:
29.30/8.12	       [?4#](x0, x1, x2, x3) = x0 + -1x1 + 4x2 + 2x3 + -16,
29.30/8.12	       
29.30/8.12	       [ordered#](x0) = x0 + -16,
29.30/8.12	       
29.30/8.12	       [cons](x0, x1) = 3x0 + 1x1 + -1,
29.30/8.12	       
29.30/8.12	       [false] = 0,
29.30/8.12	       
29.30/8.12	       [s](x0) = 4x0,
29.30/8.12	       
29.30/8.12	       [true] = 0,
29.30/8.12	       
29.30/8.12	       [lte](x0, x1) = x0 + -4x1 + 0,
29.30/8.12	       
29.30/8.12	       [0] = 1
29.30/8.12	      orientation:
29.30/8.12	       ?4#(true(),m,n,l) = 2l + -1m + 4n + 0 >= 1l + 3n + -1 = ordered#(cons(n,l))
29.30/8.12	       
29.30/8.12	       ordered#(cons(m,cons(n,l))) = 2l + 3m + 4n + 0 >= 2l + m + 4n + 0 = ?4#(lte(m,n),m,n,l)
29.30/8.12	       
29.30/8.12	       lte(0(),n) = -4n + 1 >= 0 = true()
29.30/8.12	       
29.30/8.12	       lte(s(m),0()) = 4m + 0 >= 0 = false()
29.30/8.12	       
29.30/8.12	       lte(s(m),s(n)) = 4m + n + 0 >= m + -4n + 0 = lte(m,n)
29.30/8.12	      problem:
29.30/8.12	       DPs:
29.30/8.12	        ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l)
29.30/8.12	       TRS:
29.30/8.12	        lte(0(),n) -> true()
29.30/8.12	        lte(s(m),0()) -> false()
29.30/8.12	        lte(s(m),s(n)) -> lte(m,n)
29.30/8.12	      Restore Modifier:
29.30/8.12	       DPs:
29.30/8.12	        ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l)
29.30/8.12	       TRS:
29.30/8.12	        lte(0(),n) -> true()
29.30/8.12	        lte(s(m),0()) -> false()
29.30/8.12	        lte(s(m),s(n)) -> lte(m,n)
29.30/8.12	        insert(nil(),m) -> cons(m,nil())
29.30/8.12	        ?1(true(),n,l,m) -> cons(m,cons(n,l))
29.30/8.12	        insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
29.30/8.12	        ?2(false(),n,l,m) -> cons(n,insert(l,m))
29.30/8.12	        insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m)
29.30/8.12	        ordered(nil()) -> true()
29.30/8.12	        ordered(cons(m,nil())) -> true()
29.30/8.12	        ?4(true(),m,n,l) -> ordered(cons(n,l))
29.30/8.12	        ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l)
29.30/8.12	        ?3(false(),m,n,l) -> false()
29.30/8.12	        ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l)
29.30/8.12	       SCC Processor:
29.30/8.12	        #sccs: 0
29.30/8.12	        #rules: 0
29.30/8.12	        #arcs: 2/1
29.30/8.12	        
29.30/8.12	    
29.30/8.12	    DPs:
29.30/8.12	     lte#(s(m),s(n)) -> lte#(m,n)
29.30/8.12	    TRS:
29.30/8.12	     lte(0(),n) -> true()
29.30/8.12	     lte(s(m),0()) -> false()
29.30/8.12	     lte(s(m),s(n)) -> lte(m,n)
29.30/8.12	     insert(nil(),m) -> cons(m,nil())
29.30/8.12	     ?1(true(),n,l,m) -> cons(m,cons(n,l))
29.30/8.12	     insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
29.30/8.12	     ?2(false(),n,l,m) -> cons(n,insert(l,m))
29.30/8.12	     insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m)
29.30/8.12	     ordered(nil()) -> true()
29.30/8.12	     ordered(cons(m,nil())) -> true()
29.30/8.12	     ?4(true(),m,n,l) -> ordered(cons(n,l))
29.30/8.12	     ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l)
29.30/8.12	     ?3(false(),m,n,l) -> false()
29.30/8.12	     ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l)
29.30/8.12	    Subterm Criterion Processor:
29.30/8.12	     simple projection:
29.30/8.12	      pi(lte#) = 0
29.30/8.12	     problem:
29.30/8.12	      DPs:
29.30/8.12	       
29.30/8.12	      TRS:
29.30/8.12	       lte(0(),n) -> true()
29.30/8.12	       lte(s(m),0()) -> false()
29.30/8.12	       lte(s(m),s(n)) -> lte(m,n)
29.30/8.12	       insert(nil(),m) -> cons(m,nil())
29.30/8.12	       ?1(true(),n,l,m) -> cons(m,cons(n,l))
29.30/8.12	       insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m)
29.30/8.12	       ?2(false(),n,l,m) -> cons(n,insert(l,m))
29.30/8.12	       insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m)
29.30/8.12	       ordered(nil()) -> true()
29.30/8.12	       ordered(cons(m,nil())) -> true()
29.30/8.12	       ?4(true(),m,n,l) -> ordered(cons(n,l))
29.30/8.12	       ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l)
29.30/8.12	       ?3(false(),m,n,l) -> false()
29.30/8.12	       ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l)
29.30/8.12	     Qed
29.30/8.12	
29.88/8.50	EOF