MAYBE Time: 0.004716 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()), f(t, x) -> f'(t, g x), foldC(t, 0()) -> t, foldC(t, s n) -> f(foldC(t, n), C()), f'(triple(a, b, c), A()) -> f'' foldB(triple(s a, 0(), c), b), f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()), f'(triple(a, b, c), C()) -> triple(a, b, s c), 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)} DP: DP: { foldB#(t, s n) -> foldB#(t, n), foldB#(t, s n) -> f#(foldB(t, n), B()), f#(t, x) -> g# x, f#(t, x) -> f'#(t, g x), foldC#(t, s n) -> f#(foldC(t, n), C()), foldC#(t, s n) -> foldC#(t, n), f'#(triple(a, b, c), A()) -> foldB#(triple(s a, 0(), c), b), f'#(triple(a, b, c), A()) -> f''# foldB(triple(s a, 0(), c), b), f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()), f''# triple(a, b, c) -> foldC#(triple(a, b, 0()), c), fold#(t, x, s n) -> f#(fold(t, x, n), x), fold#(t, x, s n) -> fold#(t, x, n)} 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()), f(t, x) -> f'(t, g x), foldC(t, 0()) -> t, foldC(t, s n) -> f(foldC(t, n), C()), f'(triple(a, b, c), A()) -> f'' foldB(triple(s a, 0(), c), b), f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()), f'(triple(a, b, c), C()) -> triple(a, b, s c), 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)} EDG: {(foldB#(t, s n) -> f#(foldB(t, n), B()), f#(t, x) -> f'#(t, g x)) (foldB#(t, s n) -> f#(foldB(t, n), B()), f#(t, x) -> g# x) (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)) (foldB#(t, s n) -> foldB#(t, n), foldB#(t, s n) -> f#(foldB(t, n), B())) (foldB#(t, s n) -> foldB#(t, n), foldB#(t, s n) -> foldB#(t, n)) (f''# triple(a, b, c) -> foldC#(triple(a, b, 0()), c), foldC#(t, s n) -> foldC#(t, n)) (f''# triple(a, b, c) -> foldC#(triple(a, b, 0()), c), foldC#(t, s n) -> f#(foldC(t, n), C())) (fold#(t, x, s n) -> f#(fold(t, x, n), x), f#(t, x) -> f'#(t, g x)) (fold#(t, x, s n) -> f#(fold(t, x, n), x), f#(t, x) -> g# x) (f'#(triple(a, b, c), A()) -> foldB#(triple(s a, 0(), c), b), foldB#(t, s n) -> foldB#(t, n)) (f'#(triple(a, b, c), A()) -> foldB#(triple(s a, 0(), c), b), foldB#(t, s n) -> f#(foldB(t, n), B())) (foldC#(t, s n) -> foldC#(t, n), foldC#(t, s n) -> f#(foldC(t, n), C())) (foldC#(t, s n) -> foldC#(t, n), foldC#(t, s n) -> foldC#(t, n)) (f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()), f#(t, x) -> g# x) (f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()), f#(t, x) -> f'#(t, g x)) (foldC#(t, s n) -> f#(foldC(t, n), C()), f#(t, x) -> g# x) (foldC#(t, s n) -> f#(foldC(t, n), C()), f#(t, x) -> f'#(t, g x)) (f#(t, x) -> f'#(t, g x), f'#(triple(a, b, c), A()) -> foldB#(triple(s a, 0(), c), b)) (f#(t, x) -> f'#(t, g x), f'#(triple(a, b, c), A()) -> f''# foldB(triple(s a, 0(), c), b)) (f#(t, x) -> f'#(t, g x), f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A())) (fold#(t, x, s n) -> fold#(t, x, n), fold#(t, x, s n) -> f#(fold(t, x, n), x)) (fold#(t, x, s n) -> fold#(t, x, n), fold#(t, x, s n) -> fold#(t, x, n))} STATUS: arrows: 0.847222 SCCS (2): Scc: {fold#(t, x, s n) -> fold#(t, x, n)} Scc: { foldB#(t, s n) -> foldB#(t, n), foldB#(t, s n) -> f#(foldB(t, n), B()), f#(t, x) -> f'#(t, g x), foldC#(t, s n) -> f#(foldC(t, n), C()), foldC#(t, s n) -> foldC#(t, n), f'#(triple(a, b, c), A()) -> foldB#(triple(s a, 0(), c), b), f'#(triple(a, b, c), A()) -> f''# foldB(triple(s a, 0(), c), b), f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()), f''# triple(a, b, c) -> foldC#(triple(a, b, 0()), c)} SCC (1): Strict: {fold#(t, x, s n) -> fold#(t, x, n)} Weak: { 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()), f(t, x) -> f'(t, g x), foldC(t, 0()) -> t, foldC(t, s n) -> f(foldC(t, n), C()), f'(triple(a, b, c), A()) -> f'' foldB(triple(s a, 0(), c), b), f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()), f'(triple(a, b, c), C()) -> triple(a, b, s c), 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)} Open SCC (9): Strict: { foldB#(t, s n) -> foldB#(t, n), foldB#(t, s n) -> f#(foldB(t, n), B()), f#(t, x) -> f'#(t, g x), foldC#(t, s n) -> f#(foldC(t, n), C()), foldC#(t, s n) -> foldC#(t, n), f'#(triple(a, b, c), A()) -> foldB#(triple(s a, 0(), c), b), f'#(triple(a, b, c), A()) -> f''# foldB(triple(s a, 0(), c), b), f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()), f''# triple(a, b, c) -> foldC#(triple(a, b, 0()), c)} Weak: { 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()), f(t, x) -> f'(t, g x), foldC(t, 0()) -> t, foldC(t, s n) -> f(foldC(t, n), C()), f'(triple(a, b, c), A()) -> f'' foldB(triple(s a, 0(), c), b), f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()), f'(triple(a, b, c), C()) -> triple(a, b, s c), 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)} Open