Problem CiME 04 filliatre3

MAYBE

We consider the following Problem:

  Strict Trs:
    {  g(A()) -> A()
     , g(B()) -> A()
     , g(B()) -> B()
     , g(C()) -> A()
     , g(C()) -> B()
     , g(C()) -> C()
     , foldB(t, 0()) -> t
     , foldB(t, s(n)) -> f(foldB(t, n), B())
     , foldC(t, 0()) -> t
     , foldC(t, s(n)) -> f(foldC(t, n), C())
     , f(t, x) -> f'(t, g(x))
     , f'(triple(a, b, c), C()) -> triple(a, b, s(c))
     , f'(triple(a, b, c), B()) -> f(triple(a, b, c), A())
     , f'(triple(a, b, c), A()) -> f''(foldB(triple(s(a), 0(), c), b))
     , f''(triple(a, b, c)) -> foldC(triple(a, b, 0()), c)
     , fold(t, x, 0()) -> t
     , fold(t, x, s(n)) -> f(fold(t, x, n), x)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  g(A()) -> A()
     , g(B()) -> A()
     , g(B()) -> B()
     , g(C()) -> A()
     , g(C()) -> B()
     , g(C()) -> C()
     , foldB(t, 0()) -> t
     , foldB(t, s(n)) -> f(foldB(t, n), B())
     , foldC(t, 0()) -> t
     , foldC(t, s(n)) -> f(foldC(t, n), C())
     , f(t, x) -> f'(t, g(x))
     , f'(triple(a, b, c), C()) -> triple(a, b, s(c))
     , f'(triple(a, b, c), B()) -> f(triple(a, b, c), A())
     , f'(triple(a, b, c), A()) -> f''(foldB(triple(s(a), 0(), c), b))
     , f''(triple(a, b, c)) -> foldC(triple(a, b, 0()), c)
     , fold(t, x, 0()) -> t
     , fold(t, x, s(n)) -> f(fold(t, x, n), x)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  g(A()) -> A()
     , g(B()) -> A()
     , g(B()) -> B()
     , g(C()) -> A()
     , g(C()) -> B()
     , g(C()) -> C()
     , foldB(t, 0()) -> t
     , foldB(t, s(n)) -> f(foldB(t, n), B())
     , foldC(t, 0()) -> t
     , foldC(t, s(n)) -> f(foldC(t, n), C())
     , f(t, x) -> f'(t, g(x))
     , f'(triple(a, b, c), C()) -> triple(a, b, s(c))
     , f'(triple(a, b, c), B()) -> f(triple(a, b, c), A())
     , f'(triple(a, b, c), A()) -> f''(foldB(triple(s(a), 0(), c), b))
     , f''(triple(a, b, c)) -> foldC(triple(a, b, 0()), c)
     , fold(t, x, 0()) -> t
     , fold(t, x, s(n)) -> f(fold(t, x, n), x)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  g(A()) -> A()
     , g(B()) -> A()
     , g(B()) -> B()
     , g(C()) -> A()
     , g(C()) -> B()
     , g(C()) -> C()
     , foldB(t, 0()) -> t
     , foldB(t, s(n)) -> f(foldB(t, n), B())
     , foldC(t, 0()) -> t
     , foldC(t, s(n)) -> f(foldC(t, n), C())
     , f(t, x) -> f'(t, g(x))
     , f'(triple(a, b, c), C()) -> triple(a, b, s(c))
     , f'(triple(a, b, c), B()) -> f(triple(a, b, c), A())
     , f'(triple(a, b, c), A()) -> f''(foldB(triple(s(a), 0(), c), b))
     , f''(triple(a, b, c)) -> foldC(triple(a, b, 0()), c)
     , fold(t, x, 0()) -> t
     , fold(t, x, s(n)) -> f(fold(t, x, n), x)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  g(A()) -> A()
     , g(B()) -> A()
     , g(B()) -> B()
     , g(C()) -> A()
     , g(C()) -> B()
     , g(C()) -> C()
     , foldB(t, 0()) -> t
     , foldB(t, s(n)) -> f(foldB(t, n), B())
     , foldC(t, 0()) -> t
     , foldC(t, s(n)) -> f(foldC(t, n), C())
     , f(t, x) -> f'(t, g(x))
     , f'(triple(a, b, c), C()) -> triple(a, b, s(c))
     , f'(triple(a, b, c), B()) -> f(triple(a, b, c), A())
     , f'(triple(a, b, c), A()) -> f''(foldB(triple(s(a), 0(), c), b))
     , f''(triple(a, b, c)) -> foldC(triple(a, b, 0()), c)
     , fold(t, x, 0()) -> t
     , fold(t, x, s(n)) -> f(fold(t, x, n), x)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  g(A()) -> A()
     , g(B()) -> A()
     , g(B()) -> B()
     , g(C()) -> A()
     , g(C()) -> B()
     , g(C()) -> C()
     , foldB(t, 0()) -> t
     , foldB(t, s(n)) -> f(foldB(t, n), B())
     , foldC(t, 0()) -> t
     , foldC(t, s(n)) -> f(foldC(t, n), C())
     , f(t, x) -> f'(t, g(x))
     , f'(triple(a, b, c), C()) -> triple(a, b, s(c))
     , f'(triple(a, b, c), B()) -> f(triple(a, b, c), A())
     , f'(triple(a, b, c), A()) -> f''(foldB(triple(s(a), 0(), c), b))
     , f''(triple(a, b, c)) -> foldC(triple(a, b, 0()), c)
     , fold(t, x, 0()) -> t
     , fold(t, x, s(n)) -> f(fold(t, x, n), x)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..