Problem Secret 06 TRS reverse

MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(nil()) -> true()
     , isEmpty(cons(x, xs)) -> false()
     , last(cons(x, nil())) -> x
     , last(cons(x, cons(y, ys))) -> last(cons(y, ys))
     , dropLast(nil()) -> nil()
     , dropLast(cons(x, nil())) -> nil()
     , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))
     , append(nil(), ys) -> ys
     , append(cons(x, xs), ys) -> cons(x, append(xs, ys))
     , reverse(xs) -> rev(xs, nil())
     , rev(xs, ys) ->
       if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys)
     , if(true(), xs, ys, zs) -> zs
     , if(false(), xs, ys, zs) -> rev(xs, ys)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(nil()) -> true()
     , isEmpty(cons(x, xs)) -> false()
     , last(cons(x, nil())) -> x
     , last(cons(x, cons(y, ys))) -> last(cons(y, ys))
     , dropLast(nil()) -> nil()
     , dropLast(cons(x, nil())) -> nil()
     , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))
     , append(nil(), ys) -> ys
     , append(cons(x, xs), ys) -> cons(x, append(xs, ys))
     , reverse(xs) -> rev(xs, nil())
     , rev(xs, ys) ->
       if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys)
     , if(true(), xs, ys, zs) -> zs
     , if(false(), xs, ys, zs) -> rev(xs, ys)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(nil()) -> true()
     , isEmpty(cons(x, xs)) -> false()
     , last(cons(x, nil())) -> x
     , last(cons(x, cons(y, ys))) -> last(cons(y, ys))
     , dropLast(nil()) -> nil()
     , dropLast(cons(x, nil())) -> nil()
     , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))
     , append(nil(), ys) -> ys
     , append(cons(x, xs), ys) -> cons(x, append(xs, ys))
     , reverse(xs) -> rev(xs, nil())
     , rev(xs, ys) ->
       if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys)
     , if(true(), xs, ys, zs) -> zs
     , if(false(), xs, ys, zs) -> rev(xs, ys)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(nil()) -> true()
     , isEmpty(cons(x, xs)) -> false()
     , last(cons(x, nil())) -> x
     , last(cons(x, cons(y, ys))) -> last(cons(y, ys))
     , dropLast(nil()) -> nil()
     , dropLast(cons(x, nil())) -> nil()
     , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))
     , append(nil(), ys) -> ys
     , append(cons(x, xs), ys) -> cons(x, append(xs, ys))
     , reverse(xs) -> rev(xs, nil())
     , rev(xs, ys) ->
       if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys)
     , if(true(), xs, ys, zs) -> zs
     , if(false(), xs, ys, zs) -> rev(xs, ys)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(nil()) -> true()
     , isEmpty(cons(x, xs)) -> false()
     , last(cons(x, nil())) -> x
     , last(cons(x, cons(y, ys))) -> last(cons(y, ys))
     , dropLast(nil()) -> nil()
     , dropLast(cons(x, nil())) -> nil()
     , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))
     , append(nil(), ys) -> ys
     , append(cons(x, xs), ys) -> cons(x, append(xs, ys))
     , reverse(xs) -> rev(xs, nil())
     , rev(xs, ys) ->
       if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys)
     , if(true(), xs, ys, zs) -> zs
     , if(false(), xs, ys, zs) -> rev(xs, ys)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(nil()) -> true()
     , isEmpty(cons(x, xs)) -> false()
     , last(cons(x, nil())) -> x
     , last(cons(x, cons(y, ys))) -> last(cons(y, ys))
     , dropLast(nil()) -> nil()
     , dropLast(cons(x, nil())) -> nil()
     , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))
     , append(nil(), ys) -> ys
     , append(cons(x, xs), ys) -> cons(x, append(xs, ys))
     , reverse(xs) -> rev(xs, nil())
     , rev(xs, ys) ->
       if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys)
     , if(true(), xs, ys, zs) -> zs
     , if(false(), xs, ys, zs) -> rev(xs, ys)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..