Problem Secret 07 TRS aprove10

MAYBE

We consider the following Problem:

  Strict 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()}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict 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()}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict 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()}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict 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()}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict 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()}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict 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()}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..