MAYBE

Problem:
 lessElements(l,t) -> lessE(l,t,0())
 lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
 if(true(),b,l,t,n) -> l
 if(false(),true(),l,t,n) -> t
 if(false(),false(),l,t,n) -> lessE(l,t,s(n))
 length(nil()) -> 0()
 length(cons(n,l)) -> s(length(l))
 toList(leaf()) -> nil()
 toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
 append(nil(),l2) -> l2
 append(cons(n,l1),l2) -> cons(n,append(l1,l2))
 le(s(n),0()) -> false()
 le(0(),m) -> true()
 le(s(n),s(m)) -> le(n,m)
 a() -> c()
 a() -> d()

Proof:
 DP Processor:
  DPs:
   lessElements#(l,t) -> lessE#(l,t,0())
   lessE#(l,t,n) -> toList#(t)
   lessE#(l,t,n) -> length#(toList(t))
   lessE#(l,t,n) -> le#(length(toList(t)),n)
   lessE#(l,t,n) -> length#(l)
   lessE#(l,t,n) -> le#(length(l),n)
   lessE#(l,t,n) -> if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
   if#(false(),false(),l,t,n) -> lessE#(l,t,s(n))
   length#(cons(n,l)) -> length#(l)
   toList#(node(t1,n,t2)) -> toList#(t2)
   toList#(node(t1,n,t2)) -> toList#(t1)
   toList#(node(t1,n,t2)) -> append#(toList(t1),cons(n,toList(t2)))
   append#(cons(n,l1),l2) -> append#(l1,l2)
   le#(s(n),s(m)) -> le#(n,m)
  TRS:
   lessElements(l,t) -> lessE(l,t,0())
   lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
   if(true(),b,l,t,n) -> l
   if(false(),true(),l,t,n) -> t
   if(false(),false(),l,t,n) -> lessE(l,t,s(n))
   length(nil()) -> 0()
   length(cons(n,l)) -> s(length(l))
   toList(leaf()) -> nil()
   toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
   append(nil(),l2) -> l2
   append(cons(n,l1),l2) -> cons(n,append(l1,l2))
   le(s(n),0()) -> false()
   le(0(),m) -> true()
   le(s(n),s(m)) -> le(n,m)
   a() -> c()
   a() -> d()
  TDG Processor:
   DPs:
    lessElements#(l,t) -> lessE#(l,t,0())
    lessE#(l,t,n) -> toList#(t)
    lessE#(l,t,n) -> length#(toList(t))
    lessE#(l,t,n) -> le#(length(toList(t)),n)
    lessE#(l,t,n) -> length#(l)
    lessE#(l,t,n) -> le#(length(l),n)
    lessE#(l,t,n) -> if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
    if#(false(),false(),l,t,n) -> lessE#(l,t,s(n))
    length#(cons(n,l)) -> length#(l)
    toList#(node(t1,n,t2)) -> toList#(t2)
    toList#(node(t1,n,t2)) -> toList#(t1)
    toList#(node(t1,n,t2)) -> append#(toList(t1),cons(n,toList(t2)))
    append#(cons(n,l1),l2) -> append#(l1,l2)
    le#(s(n),s(m)) -> le#(n,m)
   TRS:
    lessElements(l,t) -> lessE(l,t,0())
    lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
    if(true(),b,l,t,n) -> l
    if(false(),true(),l,t,n) -> t
    if(false(),false(),l,t,n) -> lessE(l,t,s(n))
    length(nil()) -> 0()
    length(cons(n,l)) -> s(length(l))
    toList(leaf()) -> nil()
    toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
    append(nil(),l2) -> l2
    append(cons(n,l1),l2) -> cons(n,append(l1,l2))
    le(s(n),0()) -> false()
    le(0(),m) -> true()
    le(s(n),s(m)) -> le(n,m)
    a() -> c()
    a() -> d()
   graph:
    append#(cons(n,l1),l2) -> append#(l1,l2) ->
    append#(cons(n,l1),l2) -> append#(l1,l2)
    if#(false(),false(),l,t,n) -> lessE#(l,t,s(n)) ->
    lessE#(l,t,n) -> if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
    if#(false(),false(),l,t,n) -> lessE#(l,t,s(n)) ->
    lessE#(l,t,n) -> le#(length(l),n)
    if#(false(),false(),l,t,n) -> lessE#(l,t,s(n)) ->
    lessE#(l,t,n) -> length#(l)
    if#(false(),false(),l,t,n) -> lessE#(l,t,s(n)) ->
    lessE#(l,t,n) -> le#(length(toList(t)),n)
    if#(false(),false(),l,t,n) -> lessE#(l,t,s(n)) ->
    lessE#(l,t,n) -> length#(toList(t))
    if#(false(),false(),l,t,n) -> lessE#(l,t,s(n)) ->
    lessE#(l,t,n) -> toList#(t)
    le#(s(n),s(m)) -> le#(n,m) -> le#(s(n),s(m)) -> le#(n,m)
    length#(cons(n,l)) -> length#(l) ->
    length#(cons(n,l)) -> length#(l)
    toList#(node(t1,n,t2)) -> append#(toList(t1),cons(n,toList(t2))) ->
    append#(cons(n,l1),l2) -> append#(l1,l2)
    toList#(node(t1,n,t2)) -> toList#(t2) ->
    toList#(node(t1,n,t2)) -> append#(toList(t1),cons(n,toList(t2)))
    toList#(node(t1,n,t2)) -> toList#(t2) ->
    toList#(node(t1,n,t2)) -> toList#(t1)
    toList#(node(t1,n,t2)) -> toList#(t2) ->
    toList#(node(t1,n,t2)) -> toList#(t2)
    toList#(node(t1,n,t2)) -> toList#(t1) ->
    toList#(node(t1,n,t2)) -> append#(toList(t1),cons(n,toList(t2)))
    toList#(node(t1,n,t2)) -> toList#(t1) ->
    toList#(node(t1,n,t2)) -> toList#(t1)
    toList#(node(t1,n,t2)) -> toList#(t1) ->
    toList#(node(t1,n,t2)) -> toList#(t2)
    lessE#(l,t,n) -> if#(le(length(l),n),le(length(toList(t)),n),l,t,n) ->
    if#(false(),false(),l,t,n) -> lessE#(l,t,s(n))
    lessE#(l,t,n) -> le#(length(toList(t)),n) ->
    le#(s(n),s(m)) -> le#(n,m)
    lessE#(l,t,n) -> le#(length(l),n) ->
    le#(s(n),s(m)) -> le#(n,m)
    lessE#(l,t,n) -> length#(toList(t)) ->
    length#(cons(n,l)) -> length#(l)
    lessE#(l,t,n) -> length#(l) -> length#(cons(n,l)) -> length#(l)
    lessE#(l,t,n) -> toList#(t) ->
    toList#(node(t1,n,t2)) -> append#(toList(t1),cons(n,toList(t2)))
    lessE#(l,t,n) -> toList#(t) -> toList#(node(t1,n,t2)) -> toList#(t1)
    lessE#(l,t,n) -> toList#(t) ->
    toList#(node(t1,n,t2)) -> toList#(t2)
    lessElements#(l,t) -> lessE#(l,t,0()) ->
    lessE#(l,t,n) -> if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
    lessElements#(l,t) -> lessE#(l,t,0()) ->
    lessE#(l,t,n) -> le#(length(l),n)
    lessElements#(l,t) -> lessE#(l,t,0()) ->
    lessE#(l,t,n) -> length#(l)
    lessElements#(l,t) -> lessE#(l,t,0()) ->
    lessE#(l,t,n) -> le#(length(toList(t)),n)
    lessElements#(l,t) -> lessE#(l,t,0()) ->
    lessE#(l,t,n) -> length#(toList(t))
    lessElements#(l,t) -> lessE#(l,t,0()) -> lessE#(l,t,n) -> toList#(t)
   SCC Processor:
    #sccs: 5
    #rules: 7
    #arcs: 30/196
    DPs:
     if#(false(),false(),l,t,n) -> lessE#(l,t,s(n))
     lessE#(l,t,n) -> if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
    TRS:
     lessElements(l,t) -> lessE(l,t,0())
     lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
     if(true(),b,l,t,n) -> l
     if(false(),true(),l,t,n) -> t
     if(false(),false(),l,t,n) -> lessE(l,t,s(n))
     length(nil()) -> 0()
     length(cons(n,l)) -> s(length(l))
     toList(leaf()) -> nil()
     toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
     append(nil(),l2) -> l2
     append(cons(n,l1),l2) -> cons(n,append(l1,l2))
     le(s(n),0()) -> false()
     le(0(),m) -> true()
     le(s(n),s(m)) -> le(n,m)
     a() -> c()
     a() -> d()
    Open
    
    DPs:
     le#(s(n),s(m)) -> le#(n,m)
    TRS:
     lessElements(l,t) -> lessE(l,t,0())
     lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
     if(true(),b,l,t,n) -> l
     if(false(),true(),l,t,n) -> t
     if(false(),false(),l,t,n) -> lessE(l,t,s(n))
     length(nil()) -> 0()
     length(cons(n,l)) -> s(length(l))
     toList(leaf()) -> nil()
     toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
     append(nil(),l2) -> l2
     append(cons(n,l1),l2) -> cons(n,append(l1,l2))
     le(s(n),0()) -> false()
     le(0(),m) -> true()
     le(s(n),s(m)) -> le(n,m)
     a() -> c()
     a() -> d()
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 1
     problem:
      DPs:
       
      TRS:
       lessElements(l,t) -> lessE(l,t,0())
       lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
       if(true(),b,l,t,n) -> l
       if(false(),true(),l,t,n) -> t
       if(false(),false(),l,t,n) -> lessE(l,t,s(n))
       length(nil()) -> 0()
       length(cons(n,l)) -> s(length(l))
       toList(leaf()) -> nil()
       toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
       append(nil(),l2) -> l2
       append(cons(n,l1),l2) -> cons(n,append(l1,l2))
       le(s(n),0()) -> false()
       le(0(),m) -> true()
       le(s(n),s(m)) -> le(n,m)
       a() -> c()
       a() -> d()
     Qed
    
    DPs:
     length#(cons(n,l)) -> length#(l)
    TRS:
     lessElements(l,t) -> lessE(l,t,0())
     lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
     if(true(),b,l,t,n) -> l
     if(false(),true(),l,t,n) -> t
     if(false(),false(),l,t,n) -> lessE(l,t,s(n))
     length(nil()) -> 0()
     length(cons(n,l)) -> s(length(l))
     toList(leaf()) -> nil()
     toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
     append(nil(),l2) -> l2
     append(cons(n,l1),l2) -> cons(n,append(l1,l2))
     le(s(n),0()) -> false()
     le(0(),m) -> true()
     le(s(n),s(m)) -> le(n,m)
     a() -> c()
     a() -> d()
    Subterm Criterion Processor:
     simple projection:
      pi(length#) = 0
     problem:
      DPs:
       
      TRS:
       lessElements(l,t) -> lessE(l,t,0())
       lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
       if(true(),b,l,t,n) -> l
       if(false(),true(),l,t,n) -> t
       if(false(),false(),l,t,n) -> lessE(l,t,s(n))
       length(nil()) -> 0()
       length(cons(n,l)) -> s(length(l))
       toList(leaf()) -> nil()
       toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
       append(nil(),l2) -> l2
       append(cons(n,l1),l2) -> cons(n,append(l1,l2))
       le(s(n),0()) -> false()
       le(0(),m) -> true()
       le(s(n),s(m)) -> le(n,m)
       a() -> c()
       a() -> d()
     Qed
    
    DPs:
     toList#(node(t1,n,t2)) -> toList#(t2)
     toList#(node(t1,n,t2)) -> toList#(t1)
    TRS:
     lessElements(l,t) -> lessE(l,t,0())
     lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
     if(true(),b,l,t,n) -> l
     if(false(),true(),l,t,n) -> t
     if(false(),false(),l,t,n) -> lessE(l,t,s(n))
     length(nil()) -> 0()
     length(cons(n,l)) -> s(length(l))
     toList(leaf()) -> nil()
     toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
     append(nil(),l2) -> l2
     append(cons(n,l1),l2) -> cons(n,append(l1,l2))
     le(s(n),0()) -> false()
     le(0(),m) -> true()
     le(s(n),s(m)) -> le(n,m)
     a() -> c()
     a() -> d()
    Subterm Criterion Processor:
     simple projection:
      pi(toList#) = 0
     problem:
      DPs:
       
      TRS:
       lessElements(l,t) -> lessE(l,t,0())
       lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
       if(true(),b,l,t,n) -> l
       if(false(),true(),l,t,n) -> t
       if(false(),false(),l,t,n) -> lessE(l,t,s(n))
       length(nil()) -> 0()
       length(cons(n,l)) -> s(length(l))
       toList(leaf()) -> nil()
       toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
       append(nil(),l2) -> l2
       append(cons(n,l1),l2) -> cons(n,append(l1,l2))
       le(s(n),0()) -> false()
       le(0(),m) -> true()
       le(s(n),s(m)) -> le(n,m)
       a() -> c()
       a() -> d()
     Qed
    
    DPs:
     append#(cons(n,l1),l2) -> append#(l1,l2)
    TRS:
     lessElements(l,t) -> lessE(l,t,0())
     lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
     if(true(),b,l,t,n) -> l
     if(false(),true(),l,t,n) -> t
     if(false(),false(),l,t,n) -> lessE(l,t,s(n))
     length(nil()) -> 0()
     length(cons(n,l)) -> s(length(l))
     toList(leaf()) -> nil()
     toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
     append(nil(),l2) -> l2
     append(cons(n,l1),l2) -> cons(n,append(l1,l2))
     le(s(n),0()) -> false()
     le(0(),m) -> true()
     le(s(n),s(m)) -> le(n,m)
     a() -> c()
     a() -> d()
    Subterm Criterion Processor:
     simple projection:
      pi(append#) = 0
     problem:
      DPs:
       
      TRS:
       lessElements(l,t) -> lessE(l,t,0())
       lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
       if(true(),b,l,t,n) -> l
       if(false(),true(),l,t,n) -> t
       if(false(),false(),l,t,n) -> lessE(l,t,s(n))
       length(nil()) -> 0()
       length(cons(n,l)) -> s(length(l))
       toList(leaf()) -> nil()
       toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
       append(nil(),l2) -> l2
       append(cons(n,l1),l2) -> cons(n,append(l1,l2))
       le(s(n),0()) -> false()
       le(0(),m) -> true()
       le(s(n),s(m)) -> le(n,m)
       a() -> c()
       a() -> d()
     Qed