YES Time: 0.062357 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))} 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)} SPSC: Simple Projection: pi(fold#) = 2 Strict: {} Qed 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [triple](x0, x1, x2) = x0 + x1 + 1, [fold](x0, x1, x2) = 0, [foldB](x0, x1) = x0 + x1, [f](x0, x1) = x0 + 1, [foldC](x0, x1) = x0 + x1 + 1, [f'](x0, x1) = x0 + 1, [g](x0) = 0, [s](x0) = x0 + 1, [f''](x0) = x0 + 1, [A] = 0, [B] = 0, [C] = 0, [0] = 0, [foldB#](x0, x1) = x0 + x1, [f#](x0, x1) = x0 + 1, [foldC#](x0, x1) = x0 + x1 + 1, [f'#](x0, x1) = x0 + 1, [f''#](x0) = x0 + 1 Strict: f''# triple(a, b, c) -> foldC#(triple(a, b, 0()), c) 2 + 0a + 1b + 1c >= 2 + 0a + 1b + 1c f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()) 2 + 0a + 1b + 1c >= 2 + 0a + 1b + 1c f'#(triple(a, b, c), A()) -> f''# foldB(triple(s a, 0(), c), b) 2 + 0a + 1b + 1c >= 2 + 0a + 1b + 1c f'#(triple(a, b, c), A()) -> foldB#(triple(s a, 0(), c), b) 2 + 0a + 1b + 1c >= 1 + 0a + 1b + 1c foldC#(t, s n) -> foldC#(t, n) 2 + 1t + 1n >= 1 + 1t + 1n foldC#(t, s n) -> f#(foldC(t, n), C()) 2 + 1t + 1n >= 2 + 1t + 1n f#(t, x) -> f'#(t, g x) 1 + 1t + 0x >= 1 + 1t + 0x foldB#(t, s n) -> f#(foldB(t, n), B()) 1 + 1t + 1n >= 1 + 1t + 1n foldB#(t, s n) -> foldB#(t, n) 1 + 1t + 1n >= 0 + 1t + 1n Weak: EDG: {(foldB#(t, s n) -> f#(foldB(t, n), B()), f#(t, x) -> f'#(t, 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)) (f''# triple(a, b, c) -> foldC#(triple(a, b, 0()), c), foldC#(t, s n) -> f#(foldC(t, n), C())) (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) -> f'#(t, g x)) (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()))} SCCS (1): Scc: { f#(t, x) -> f'#(t, g x), 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) -> foldC#(triple(a, b, 0()), c)} SCC (5): Strict: { f#(t, x) -> f'#(t, g x), 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) -> 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [triple](x0, x1, x2) = x0, [fold](x0, x1, x2) = 0, [foldB](x0, x1) = x0, [f](x0, x1) = x0 + x1, [foldC](x0, x1) = x0 + x1, [f'](x0, x1) = x0 + x1, [g](x0) = x0, [s](x0) = x0 + 1, [f''](x0) = x0, [A] = 0, [B] = 0, [C] = 1, [0] = 0, [f#](x0, x1) = x0, [foldC#](x0, x1) = x0 + x1, [f'#](x0, x1) = x0, [f''#](x0) = x0 Strict: f''# triple(a, b, c) -> foldC#(triple(a, b, 0()), c) 0 + 0a + 0b + 1c >= 0 + 0a + 0b + 1c f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()) 0 + 0a + 0b + 1c >= 0 + 0a + 0b + 1c f'#(triple(a, b, c), A()) -> f''# foldB(triple(s a, 0(), c), b) 0 + 0a + 0b + 1c >= 0 + 0a + 0b + 1c foldC#(t, s n) -> f#(foldC(t, n), C()) 1 + 1t + 1n >= 0 + 1t + 1n f#(t, x) -> f'#(t, g x) 0 + 1t + 0x >= 0 + 1t + 0x Weak: EDG: {(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)) (f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()), f#(t, x) -> f'#(t, g x)) (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()))} SCCS (1): Scc: { f#(t, x) -> f'#(t, g x), f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A())} SCC (2): Strict: { f#(t, x) -> f'#(t, g x), f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A())} 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [triple](x0, x1, x2) = 1, [fold](x0, x1, x2) = 0, [foldB](x0, x1) = x0 + x1 + 1, [f](x0, x1) = 0, [foldC](x0, x1) = x0 + x1 + 1, [f'](x0, x1) = 0, [g](x0) = x0, [s](x0) = 1, [f''](x0) = x0, [A] = 0, [B] = 1, [C] = 1, [0] = 1, [f#](x0, x1) = x0 + x1 + 1, [f'#](x0, x1) = x0 + x1 + 1 Strict: f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()) 3 + 0a + 0b + 0c >= 2 + 0a + 0b + 0c f#(t, x) -> f'#(t, g x) 1 + 1t + 1x >= 1 + 1t + 1x Weak: EDG: {} SCCS (0): Qed