14.66/4.78	YES
14.66/4.78	
14.66/4.78	Proof:
14.66/4.78	This system is confluent.
14.66/4.78	Inlined conditions in System R.
14.66/4.78	By \cite{ALS94}, Theorem 4.1.
14.66/4.78	This system is of type 3 or smaller.
14.66/4.78	This system is strongly deterministic.
14.66/4.78	This system is quasi-decreasing.
14.66/4.78	By \cite{O02}, p. 214, Proposition 7.2.50.
14.66/4.78	This system is of type 3 or smaller.
14.66/4.78	This system is deterministic.
14.66/4.78	System R transformed to optimized U(R).
14.66/4.78	This system is terminating.
14.66/4.78	Call external tool:
14.66/4.78	./ttt2.sh
14.66/4.78	Input:
14.66/4.78	(VAR x r y n xs)
14.66/4.78	(RULES
14.66/4.78	  m(x, 0) -> x
14.66/4.78	  mod(s(x), 0) -> 0
14.66/4.78	  lte(s(x), 0) -> false
14.66/4.78	  filter(n, r, nil) -> nil
14.66/4.78	  m(s(x), s(y)) -> m(x, y)
14.66/4.78	  mod(s(x), s(y)) -> ?1(lte(y, x), x, y)
14.66/4.78	  ?1(false, x, y) -> s(x)
14.66/4.78	  filter(n, r, cons(x, xs)) -> ?2(eq(r, mod(x, n)), n, r, x, xs)
14.66/4.78	  ?2(false, n, r, x, xs) -> filter(n, r, xs)
14.66/4.78	  eq(0, 0) -> true
14.66/4.78	  filter(n, r, cons(x, xs)) -> ?2(eq(r, mod(x, n)), n, r, x, xs)
14.66/4.78	  ?2(true, n, r, x, xs) -> cons(x, filter(n, r, xs))
14.66/4.78	  lte(s(x), s(y)) -> lte(x, y)
14.66/4.78	  eq(s(x), 0) -> false
14.66/4.78	  eq(s(x), s(y)) -> eq(x, y)
14.66/4.78	  mod(0, y) -> 0
14.66/4.78	  eq(0, s(y)) -> false
14.66/4.78	  lte(0, y) -> true
14.66/4.78	  mod(s(x), s(y)) -> ?1(lte(y, x), x, y)
14.66/4.78	  ?1(true, x, y) -> mod(m(x, y), s(y))
14.66/4.78	  m(0, s(y)) -> 0
14.66/4.78	)
14.66/4.78	
14.66/4.78	 DP Processor:
14.66/4.78	  DPs:
14.66/4.78	   m#(s(x),s(y)) -> m#(x,y)
14.66/4.78	   mod#(s(x),s(y)) -> lte#(y,x)
14.66/4.78	   mod#(s(x),s(y)) -> ?1#(lte(y,x),x,y)
14.66/4.78	   filter#(n,r,cons(x,xs)) -> mod#(x,n)
14.66/4.78	   filter#(n,r,cons(x,xs)) -> eq#(r,mod(x,n))
14.66/4.78	   filter#(n,r,cons(x,xs)) -> ?2#(eq(r,mod(x,n)),n,r,x,xs)
14.66/4.78	   ?2#(false(),n,r,x,xs) -> filter#(n,r,xs)
14.66/4.78	   ?2#(true(),n,r,x,xs) -> filter#(n,r,xs)
14.66/4.78	   lte#(s(x),s(y)) -> lte#(x,y)
14.66/4.78	   eq#(s(x),s(y)) -> eq#(x,y)
14.66/4.78	   ?1#(true(),x,y) -> m#(x,y)
14.66/4.78	   ?1#(true(),x,y) -> mod#(m(x,y),s(y))
14.66/4.78	  TRS:
14.66/4.78	   m(x,0()) -> x
14.66/4.78	   mod(s(x),0()) -> 0()
14.66/4.78	   lte(s(x),0()) -> false()
14.66/4.78	   filter(n,r,nil()) -> nil()
14.66/4.78	   m(s(x),s(y)) -> m(x,y)
14.66/4.78	   mod(s(x),s(y)) -> ?1(lte(y,x),x,y)
14.66/4.78	   ?1(false(),x,y) -> s(x)
14.66/4.78	   filter(n,r,cons(x,xs)) -> ?2(eq(r,mod(x,n)),n,r,x,xs)
14.66/4.78	   ?2(false(),n,r,x,xs) -> filter(n,r,xs)
14.66/4.78	   eq(0(),0()) -> true()
14.66/4.78	   ?2(true(),n,r,x,xs) -> cons(x,filter(n,r,xs))
14.66/4.78	   lte(s(x),s(y)) -> lte(x,y)
14.66/4.78	   eq(s(x),0()) -> false()
14.66/4.78	   eq(s(x),s(y)) -> eq(x,y)
14.66/4.78	   mod(0(),y) -> 0()
14.66/4.78	   eq(0(),s(y)) -> false()
14.66/4.78	   lte(0(),y) -> true()
14.66/4.78	   ?1(true(),x,y) -> mod(m(x,y),s(y))
14.66/4.78	   m(0(),s(y)) -> 0()
14.66/4.78	  TDG Processor:
14.66/4.78	   DPs:
14.66/4.78	    m#(s(x),s(y)) -> m#(x,y)
14.66/4.79	    mod#(s(x),s(y)) -> lte#(y,x)
14.66/4.79	    mod#(s(x),s(y)) -> ?1#(lte(y,x),x,y)
14.66/4.79	    filter#(n,r,cons(x,xs)) -> mod#(x,n)
14.66/4.79	    filter#(n,r,cons(x,xs)) -> eq#(r,mod(x,n))
14.66/4.79	    filter#(n,r,cons(x,xs)) -> ?2#(eq(r,mod(x,n)),n,r,x,xs)
14.66/4.79	    ?2#(false(),n,r,x,xs) -> filter#(n,r,xs)
14.66/4.79	    ?2#(true(),n,r,x,xs) -> filter#(n,r,xs)
14.66/4.79	    lte#(s(x),s(y)) -> lte#(x,y)
14.66/4.79	    eq#(s(x),s(y)) -> eq#(x,y)
14.66/4.79	    ?1#(true(),x,y) -> m#(x,y)
14.66/4.79	    ?1#(true(),x,y) -> mod#(m(x,y),s(y))
14.66/4.79	   TRS:
14.66/4.79	    m(x,0()) -> x
14.66/4.79	    mod(s(x),0()) -> 0()
14.66/4.79	    lte(s(x),0()) -> false()
14.66/4.79	    filter(n,r,nil()) -> nil()
14.66/4.79	    m(s(x),s(y)) -> m(x,y)
14.66/4.79	    mod(s(x),s(y)) -> ?1(lte(y,x),x,y)
14.66/4.79	    ?1(false(),x,y) -> s(x)
14.66/4.79	    filter(n,r,cons(x,xs)) -> ?2(eq(r,mod(x,n)),n,r,x,xs)
14.66/4.79	    ?2(false(),n,r,x,xs) -> filter(n,r,xs)
14.66/4.79	    eq(0(),0()) -> true()
14.66/4.79	    ?2(true(),n,r,x,xs) -> cons(x,filter(n,r,xs))
14.66/4.79	    lte(s(x),s(y)) -> lte(x,y)
14.66/4.79	    eq(s(x),0()) -> false()
14.66/4.79	    eq(s(x),s(y)) -> eq(x,y)
14.66/4.79	    mod(0(),y) -> 0()
14.66/4.79	    eq(0(),s(y)) -> false()
14.66/4.79	    lte(0(),y) -> true()
14.66/4.79	    ?1(true(),x,y) -> mod(m(x,y),s(y))
14.66/4.79	    m(0(),s(y)) -> 0()
14.66/4.79	   graph:
14.66/4.79	    ?2#(true(),n,r,x,xs) -> filter#(n,r,xs) ->
14.66/4.79	    filter#(n,r,cons(x,xs)) -> ?2#(eq(r,mod(x,n)),n,r,x,xs)
14.66/4.79	    ?2#(true(),n,r,x,xs) -> filter#(n,r,xs) ->
14.66/4.79	    filter#(n,r,cons(x,xs)) -> eq#(r,mod(x,n))
14.66/4.79	    ?2#(true(),n,r,x,xs) -> filter#(n,r,xs) ->
14.66/4.79	    filter#(n,r,cons(x,xs)) -> mod#(x,n)
14.66/4.79	    ?2#(false(),n,r,x,xs) -> filter#(n,r,xs) ->
14.66/4.79	    filter#(n,r,cons(x,xs)) -> ?2#(eq(r,mod(x,n)),n,r,x,xs)
14.66/4.79	    ?2#(false(),n,r,x,xs) -> filter#(n,r,xs) ->
14.66/4.79	    filter#(n,r,cons(x,xs)) -> eq#(r,mod(x,n))
14.66/4.79	    ?2#(false(),n,r,x,xs) -> filter#(n,r,xs) ->
14.66/4.79	    filter#(n,r,cons(x,xs)) -> mod#(x,n)
14.66/4.79	    eq#(s(x),s(y)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y)
14.66/4.79	    ?1#(true(),x,y) -> mod#(m(x,y),s(y)) ->
14.66/4.79	    mod#(s(x),s(y)) -> ?1#(lte(y,x),x,y)
14.66/4.79	    ?1#(true(),x,y) -> mod#(m(x,y),s(y)) -> mod#(s(x),s(y)) -> lte#(y,x)
14.66/4.79	    ?1#(true(),x,y) -> m#(x,y) ->
14.66/4.79	    m#(s(x),s(y)) -> m#(x,y)
14.66/4.79	    filter#(n,r,cons(x,xs)) -> ?2#(eq(r,mod(x,n)),n,r,x,xs) ->
14.66/4.79	    ?2#(true(),n,r,x,xs) -> filter#(n,r,xs)
14.66/4.79	    filter#(n,r,cons(x,xs)) -> ?2#(eq(r,mod(x,n)),n,r,x,xs) ->
14.66/4.79	    ?2#(false(),n,r,x,xs) -> filter#(n,r,xs)
14.98/4.79	    filter#(n,r,cons(x,xs)) -> eq#(r,mod(x,n)) ->
14.98/4.79	    eq#(s(x),s(y)) -> eq#(x,y)
14.98/4.79	    filter#(n,r,cons(x,xs)) -> mod#(x,n) ->
14.98/4.79	    mod#(s(x),s(y)) -> ?1#(lte(y,x),x,y)
14.98/4.79	    filter#(n,r,cons(x,xs)) -> mod#(x,n) ->
14.98/4.79	    mod#(s(x),s(y)) -> lte#(y,x)
14.98/4.79	    lte#(s(x),s(y)) -> lte#(x,y) ->
14.98/4.79	    lte#(s(x),s(y)) -> lte#(x,y)
14.98/4.79	    mod#(s(x),s(y)) -> ?1#(lte(y,x),x,y) ->
14.98/4.79	    ?1#(true(),x,y) -> mod#(m(x,y),s(y))
14.98/4.79	    mod#(s(x),s(y)) -> ?1#(lte(y,x),x,y) -> ?1#(true(),x,y) -> m#(x,y)
14.98/4.79	    mod#(s(x),s(y)) -> lte#(y,x) -> lte#(s(x),s(y)) -> lte#(x,y)
14.98/4.79	    m#(s(x),s(y)) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y)
14.98/4.79	   SCC Processor:
14.98/4.79	    #sccs: 5
14.98/4.79	    #rules: 8
14.98/4.79	    #arcs: 20/144
14.98/4.79	    DPs:
14.98/4.79	     ?2#(true(),n,r,x,xs) -> filter#(n,r,xs)
14.98/4.79	     filter#(n,r,cons(x,xs)) -> ?2#(eq(r,mod(x,n)),n,r,x,xs)
14.98/4.79	     ?2#(false(),n,r,x,xs) -> filter#(n,r,xs)
14.98/4.79	    TRS:
14.98/4.79	     m(x,0()) -> x
14.98/4.79	     mod(s(x),0()) -> 0()
14.98/4.79	     lte(s(x),0()) -> false()
14.98/4.79	     filter(n,r,nil()) -> nil()
14.98/4.79	     m(s(x),s(y)) -> m(x,y)
14.98/4.79	     mod(s(x),s(y)) -> ?1(lte(y,x),x,y)
14.98/4.79	     ?1(false(),x,y) -> s(x)
14.98/4.79	     filter(n,r,cons(x,xs)) -> ?2(eq(r,mod(x,n)),n,r,x,xs)
14.98/4.79	     ?2(false(),n,r,x,xs) -> filter(n,r,xs)
14.98/4.79	     eq(0(),0()) -> true()
14.98/4.79	     ?2(true(),n,r,x,xs) -> cons(x,filter(n,r,xs))
14.98/4.79	     lte(s(x),s(y)) -> lte(x,y)
14.98/4.79	     eq(s(x),0()) -> false()
14.98/4.79	     eq(s(x),s(y)) -> eq(x,y)
14.98/4.79	     mod(0(),y) -> 0()
14.98/4.79	     eq(0(),s(y)) -> false()
14.98/4.79	     lte(0(),y) -> true()
14.98/4.79	     ?1(true(),x,y) -> mod(m(x,y),s(y))
14.98/4.79	     m(0(),s(y)) -> 0()
14.98/4.79	    Subterm Criterion Processor:
14.98/4.79	     simple projection:
14.98/4.79	      pi(filter#) = 2
14.98/4.79	      pi(?2#) = 4
14.98/4.79	     problem:
14.98/4.79	      DPs:
14.98/4.79	       ?2#(true(),n,r,x,xs) -> filter#(n,r,xs)
14.98/4.79	       ?2#(false(),n,r,x,xs) -> filter#(n,r,xs)
14.98/4.79	      TRS:
14.98/4.79	       m(x,0()) -> x
14.98/4.79	       mod(s(x),0()) -> 0()
14.98/4.79	       lte(s(x),0()) -> false()
14.98/4.79	       filter(n,r,nil()) -> nil()
14.98/4.79	       m(s(x),s(y)) -> m(x,y)
14.98/4.79	       mod(s(x),s(y)) -> ?1(lte(y,x),x,y)
14.98/4.79	       ?1(false(),x,y) -> s(x)
14.98/4.79	       filter(n,r,cons(x,xs)) -> ?2(eq(r,mod(x,n)),n,r,x,xs)
14.98/4.79	       ?2(false(),n,r,x,xs) -> filter(n,r,xs)
14.98/4.79	       eq(0(),0()) -> true()
14.98/4.79	       ?2(true(),n,r,x,xs) -> cons(x,filter(n,r,xs))
14.98/4.79	       lte(s(x),s(y)) -> lte(x,y)
14.98/4.79	       eq(s(x),0()) -> false()
14.98/4.79	       eq(s(x),s(y)) -> eq(x,y)
14.98/4.79	       mod(0(),y) -> 0()
14.98/4.79	       eq(0(),s(y)) -> false()
14.98/4.79	       lte(0(),y) -> true()
14.98/4.80	       ?1(true(),x,y) -> mod(m(x,y),s(y))
14.98/4.80	       m(0(),s(y)) -> 0()
14.98/4.80	     SCC Processor:
14.98/4.80	      #sccs: 0
14.98/4.80	      #rules: 0
14.98/4.80	      #arcs: 4/4
14.98/4.80	      
14.98/4.80	    
14.98/4.80	    DPs:
14.98/4.80	     eq#(s(x),s(y)) -> eq#(x,y)
14.98/4.80	    TRS:
14.98/4.80	     m(x,0()) -> x
14.98/4.80	     mod(s(x),0()) -> 0()
14.98/4.80	     lte(s(x),0()) -> false()
14.98/4.80	     filter(n,r,nil()) -> nil()
14.98/4.80	     m(s(x),s(y)) -> m(x,y)
14.98/4.80	     mod(s(x),s(y)) -> ?1(lte(y,x),x,y)
14.98/4.80	     ?1(false(),x,y) -> s(x)
14.98/4.80	     filter(n,r,cons(x,xs)) -> ?2(eq(r,mod(x,n)),n,r,x,xs)
14.98/4.80	     ?2(false(),n,r,x,xs) -> filter(n,r,xs)
14.98/4.80	     eq(0(),0()) -> true()
14.98/4.80	     ?2(true(),n,r,x,xs) -> cons(x,filter(n,r,xs))
14.98/4.80	     lte(s(x),s(y)) -> lte(x,y)
14.98/4.80	     eq(s(x),0()) -> false()
14.98/4.80	     eq(s(x),s(y)) -> eq(x,y)
14.98/4.80	     mod(0(),y) -> 0()
14.98/4.80	     eq(0(),s(y)) -> false()
14.98/4.80	     lte(0(),y) -> true()
14.98/4.80	     ?1(true(),x,y) -> mod(m(x,y),s(y))
14.98/4.80	     m(0(),s(y)) -> 0()
14.98/4.80	    Subterm Criterion Processor:
14.98/4.80	     simple projection:
14.98/4.80	      pi(eq#) = 0
14.98/4.80	     problem:
14.98/4.80	      DPs:
14.98/4.80	       
14.98/4.80	      TRS:
14.98/4.80	       m(x,0()) -> x
14.98/4.80	       mod(s(x),0()) -> 0()
14.98/4.80	       lte(s(x),0()) -> false()
14.98/4.80	       filter(n,r,nil()) -> nil()
14.98/4.80	       m(s(x),s(y)) -> m(x,y)
14.98/4.80	       mod(s(x),s(y)) -> ?1(lte(y,x),x,y)
14.98/4.80	       ?1(false(),x,y) -> s(x)
14.98/4.80	       filter(n,r,cons(x,xs)) -> ?2(eq(r,mod(x,n)),n,r,x,xs)
14.98/4.80	       ?2(false(),n,r,x,xs) -> filter(n,r,xs)
14.98/4.80	       eq(0(),0()) -> true()
14.98/4.80	       ?2(true(),n,r,x,xs) -> cons(x,filter(n,r,xs))
14.98/4.80	       lte(s(x),s(y)) -> lte(x,y)
14.98/4.80	       eq(s(x),0()) -> false()
14.98/4.80	       eq(s(x),s(y)) -> eq(x,y)
14.98/4.80	       mod(0(),y) -> 0()
14.98/4.80	       eq(0(),s(y)) -> false()
14.98/4.80	       lte(0(),y) -> true()
14.98/4.80	       ?1(true(),x,y) -> mod(m(x,y),s(y))
14.98/4.80	       m(0(),s(y)) -> 0()
14.98/4.80	     Qed
14.98/4.80	    
14.98/4.80	    DPs:
14.98/4.80	     mod#(s(x),s(y)) -> ?1#(lte(y,x),x,y)
14.98/4.80	     ?1#(true(),x,y) -> mod#(m(x,y),s(y))
14.98/4.80	    TRS:
14.98/4.80	     m(x,0()) -> x
14.98/4.80	     mod(s(x),0()) -> 0()
14.98/4.80	     lte(s(x),0()) -> false()
14.98/4.80	     filter(n,r,nil()) -> nil()
14.98/4.80	     m(s(x),s(y)) -> m(x,y)
14.98/4.80	     mod(s(x),s(y)) -> ?1(lte(y,x),x,y)
14.98/4.80	     ?1(false(),x,y) -> s(x)
14.98/4.80	     filter(n,r,cons(x,xs)) -> ?2(eq(r,mod(x,n)),n,r,x,xs)
14.98/4.80	     ?2(false(),n,r,x,xs) -> filter(n,r,xs)
14.98/4.80	     eq(0(),0()) -> true()
14.98/4.80	     ?2(true(),n,r,x,xs) -> cons(x,filter(n,r,xs))
14.98/4.80	     lte(s(x),s(y)) -> lte(x,y)
14.98/4.80	     eq(s(x),0()) -> false()
14.98/4.80	     eq(s(x),s(y)) -> eq(x,y)
14.98/4.80	     mod(0(),y) -> 0()
14.98/4.80	     eq(0(),s(y)) -> false()
14.98/4.80	     lte(0(),y) -> true()
14.98/4.80	     ?1(true(),x,y) -> mod(m(x,y),s(y))
14.98/4.80	     m(0(),s(y)) -> 0()
14.98/4.80	    Subterm Criterion Processor:
14.98/4.80	     simple projection:
14.98/4.80	      pi(m) = 0
14.98/4.80	      pi(mod#) = 0
14.98/4.80	      pi(?1#) = 1
14.98/4.80	     problem:
14.98/4.80	      DPs:
14.98/4.80	       ?1#(true(),x,y) -> mod#(m(x,y),s(y))
14.98/4.80	      TRS:
14.98/4.80	       m(x,0()) -> x
14.98/4.80	       mod(s(x),0()) -> 0()
14.98/4.80	       lte(s(x),0()) -> false()
14.98/4.80	       filter(n,r,nil()) -> nil()
14.98/4.80	       m(s(x),s(y)) -> m(x,y)
14.98/4.80	       mod(s(x),s(y)) -> ?1(lte(y,x),x,y)
14.98/4.80	       ?1(false(),x,y) -> s(x)
14.98/4.80	       filter(n,r,cons(x,xs)) -> ?2(eq(r,mod(x,n)),n,r,x,xs)
14.98/4.80	       ?2(false(),n,r,x,xs) -> filter(n,r,xs)
14.98/4.80	       eq(0(),0()) -> true()
14.98/4.80	       ?2(true(),n,r,x,xs) -> cons(x,filter(n,r,xs))
14.98/4.80	       lte(s(x),s(y)) -> lte(x,y)
14.98/4.80	       eq(s(x),0()) -> false()
14.98/4.80	       eq(s(x),s(y)) -> eq(x,y)
14.98/4.80	       mod(0(),y) -> 0()
14.98/4.80	       eq(0(),s(y)) -> false()
14.98/4.80	       lte(0(),y) -> true()
14.98/4.80	       ?1(true(),x,y) -> mod(m(x,y),s(y))
14.98/4.80	       m(0(),s(y)) -> 0()
14.98/4.80	     SCC Processor:
14.98/4.80	      #sccs: 0
14.98/4.80	      #rules: 0
14.98/4.80	      #arcs: 2/1
14.98/4.81	      
14.98/4.81	    
14.98/4.81	    DPs:
14.98/4.81	     m#(s(x),s(y)) -> m#(x,y)
14.98/4.84	    TRS:
14.98/4.84	     m(x,0()) -> x
14.98/4.84	     mod(s(x),0()) -> 0()
14.98/4.84	     lte(s(x),0()) -> false()
14.98/4.84	     filter(n,r,nil()) -> nil()
14.98/4.84	     m(s(x),s(y)) -> m(x,y)
14.98/4.84	     mod(s(x),s(y)) -> ?1(lte(y,x),x,y)
14.98/4.84	     ?1(false(),x,y) -> s(x)
14.98/4.84	     filter(n,r,cons(x,xs)) -> ?2(eq(r,mod(x,n)),n,r,x,xs)
14.98/4.84	     ?2(false(),n,r,x,xs) -> filter(n,r,xs)
14.98/4.84	     eq(0(),0()) -> true()
14.98/4.84	     ?2(true(),n,r,x,xs) -> cons(x,filter(n,r,xs))
14.98/4.84	     lte(s(x),s(y)) -> lte(x,y)
14.98/4.84	     eq(s(x),0()) -> false()
14.98/4.84	     eq(s(x),s(y)) -> eq(x,y)
14.98/4.84	     mod(0(),y) -> 0()
14.98/4.84	     eq(0(),s(y)) -> false()
14.98/4.84	     lte(0(),y) -> true()
14.98/4.84	     ?1(true(),x,y) -> mod(m(x,y),s(y))
14.98/4.84	     m(0(),s(y)) -> 0()
14.98/4.84	    Subterm Criterion Processor:
14.98/4.84	     simple projection:
14.98/4.84	      pi(m#) = 0
14.98/4.84	     problem:
14.98/4.84	      DPs:
14.98/4.84	       
14.98/4.84	      TRS:
14.98/4.84	       m(x,0()) -> x
14.98/4.84	       mod(s(x),0()) -> 0()
14.98/4.84	       lte(s(x),0()) -> false()
14.98/4.84	       filter(n,r,nil()) -> nil()
14.98/4.84	       m(s(x),s(y)) -> m(x,y)
14.98/4.84	       mod(s(x),s(y)) -> ?1(lte(y,x),x,y)
14.98/4.84	       ?1(false(),x,y) -> s(x)
14.98/4.84	       filter(n,r,cons(x,xs)) -> ?2(eq(r,mod(x,n)),n,r,x,xs)
14.98/4.84	       ?2(false(),n,r,x,xs) -> filter(n,r,xs)
14.98/4.84	       eq(0(),0()) -> true()
14.98/4.84	       ?2(true(),n,r,x,xs) -> cons(x,filter(n,r,xs))
14.98/4.84	       lte(s(x),s(y)) -> lte(x,y)
14.98/4.84	       eq(s(x),0()) -> false()
14.98/4.84	       eq(s(x),s(y)) -> eq(x,y)
14.98/4.84	       mod(0(),y) -> 0()
14.98/4.84	       eq(0(),s(y)) -> false()
14.98/4.84	       lte(0(),y) -> true()
14.98/4.84	       ?1(true(),x,y) -> mod(m(x,y),s(y))
14.98/4.84	       m(0(),s(y)) -> 0()
14.98/4.84	     Qed
14.98/4.84	    
14.98/4.84	    DPs:
14.98/4.84	     lte#(s(x),s(y)) -> lte#(x,y)
14.98/4.84	    TRS:
14.98/4.84	     m(x,0()) -> x
14.98/4.84	     mod(s(x),0()) -> 0()
14.98/4.84	     lte(s(x),0()) -> false()
14.98/4.84	     filter(n,r,nil()) -> nil()
14.98/4.84	     m(s(x),s(y)) -> m(x,y)
14.98/4.84	     mod(s(x),s(y)) -> ?1(lte(y,x),x,y)
14.98/4.84	     ?1(false(),x,y) -> s(x)
14.98/4.84	     filter(n,r,cons(x,xs)) -> ?2(eq(r,mod(x,n)),n,r,x,xs)
14.98/4.84	     ?2(false(),n,r,x,xs) -> filter(n,r,xs)
14.98/4.84	     eq(0(),0()) -> true()
14.98/4.84	     ?2(true(),n,r,x,xs) -> cons(x,filter(n,r,xs))
14.98/4.84	     lte(s(x),s(y)) -> lte(x,y)
14.98/4.84	     eq(s(x),0()) -> false()
14.98/4.84	     eq(s(x),s(y)) -> eq(x,y)
14.98/4.84	     mod(0(),y) -> 0()
14.98/4.84	     eq(0(),s(y)) -> false()
14.98/4.84	     lte(0(),y) -> true()
14.98/4.84	     ?1(true(),x,y) -> mod(m(x,y),s(y))
14.98/4.84	     m(0(),s(y)) -> 0()
14.98/4.84	    Subterm Criterion Processor:
14.98/4.84	     simple projection:
14.98/4.84	      pi(lte#) = 0
14.98/4.84	     problem:
14.98/4.84	      DPs:
14.98/4.84	       
14.98/4.84	      TRS:
14.98/4.84	       m(x,0()) -> x
14.98/4.84	       mod(s(x),0()) -> 0()
14.98/4.84	       lte(s(x),0()) -> false()
14.98/4.84	       filter(n,r,nil()) -> nil()
14.98/4.84	       m(s(x),s(y)) -> m(x,y)
14.98/4.84	       mod(s(x),s(y)) -> ?1(lte(y,x),x,y)
14.98/4.84	       ?1(false(),x,y) -> s(x)
14.98/4.84	       filter(n,r,cons(x,xs)) -> ?2(eq(r,mod(x,n)),n,r,x,xs)
14.98/4.84	       ?2(false(),n,r,x,xs) -> filter(n,r,xs)
14.98/4.84	       eq(0(),0()) -> true()
14.98/4.84	       ?2(true(),n,r,x,xs) -> cons(x,filter(n,r,xs))
14.98/4.84	       lte(s(x),s(y)) -> lte(x,y)
14.98/4.84	       eq(s(x),0()) -> false()
14.98/4.84	       eq(s(x),s(y)) -> eq(x,y)
14.98/4.84	       mod(0(),y) -> 0()
14.98/4.84	       eq(0(),s(y)) -> false()
14.98/4.84	       lte(0(),y) -> true()
14.98/4.84	       ?1(true(),x,y) -> mod(m(x,y),s(y))
14.98/4.84	       m(0(),s(y)) -> 0()
14.98/4.84	     Qed
14.98/4.84	All 4 critical pairs are joinable.
14.98/4.84	Overlap: (rule1: mod(s(z), s(x')) -> s(z) <= lte(x', z) = false, rule2: mod(s(y'), s(z')) -> mod(m(y', z'), s(z')) <= lte(z', y') = true, pos: ε, mgu: {(z,y'), (x',z')})
14.98/4.84	CP: mod(m(y', z'), s(z')) = s(y') <= lte(z', y') = false, lte(z', y') = true
14.98/4.84	This critical pair is unfeasible.
14.98/4.84	Overlap: (rule1: mod(s(z), s(x')) -> mod(m(z, x'), s(x')) <= lte(x', z) = true, rule2: mod(s(y'), s(z')) -> s(y') <= lte(z', y') = false, pos: ε, mgu: {(z,y'), (x',z')})
14.98/4.84	CP: s(y') = mod(m(y', z'), s(z')) <= lte(z', y') = true, lte(z', y') = false
14.98/4.84	This critical pair is unfeasible.
14.98/4.84	Overlap: (rule1: filter(y, z, cons(x', y')) -> filter(y, z, y') <= eq(z, mod(x', y)) = false, rule2: filter(z', $1, cons($2, $3)) -> cons($2, filter(z', $1, $3)) <= eq($1, mod($2, z')) = true, pos: ε, mgu: {(y,z'), (z,$1), (x',$2), (y',$3)})
14.98/4.84	CP: cons($2, filter(z', $1, $3)) = filter(z', $1, $3) <= eq($1, mod($2, z')) = false, eq($1, mod($2, z')) = true
14.98/4.84	This critical pair is unfeasible.
14.98/4.84	Overlap: (rule1: filter(y, z, cons(x', y')) -> cons(x', filter(y, z, y')) <= eq(z, mod(x', y)) = true, rule2: filter(z', $1, cons($2, $3)) -> filter(z', $1, $3) <= eq($1, mod($2, z')) = false, pos: ε, mgu: {(y,z'), (z,$1), (x',$2), (y',$3)})
14.98/4.84	CP: filter(z', $1, $3) = cons($2, filter(z', $1, $3)) <= eq($1, mod($2, z')) = true, eq($1, mod($2, z')) = false
14.98/4.84	This critical pair is unfeasible.
14.98/4.84	
15.31/4.90	EOF