YES Time: 0.019018 TRS: { f 0() -> true(), f 1() -> false(), f s x -> f x, if(true(), s x, s y) -> s x, if(false(), s x, s y) -> s y, g(x, c y) -> c g(x, y), g(x, c y) -> g(x, if(f x, c g(s x, y), c y))} DP: DP: { f# s x -> f# x, g#(x, c y) -> f# x, g#(x, c y) -> if#(f x, c g(s x, y), c y), g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y)), g#(x, c y) -> g#(s x, y)} TRS: { f 0() -> true(), f 1() -> false(), f s x -> f x, if(true(), s x, s y) -> s x, if(false(), s x, s y) -> s y, g(x, c y) -> c g(x, y), g(x, c y) -> g(x, if(f x, c g(s x, y), c y))} UR: { f 0() -> true(), f 1() -> false(), f s x -> f x, g(x, c y) -> c g(x, y), g(x, c y) -> g(x, if(f x, c g(s x, y), c y)), a(z, w) -> z, a(z, w) -> w} EDG: {(g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(s x, y)) (g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y))) (g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(x, y)) (g#(x, c y) -> g#(x, y), g#(x, c y) -> if#(f x, c g(s x, y), c y)) (g#(x, c y) -> g#(x, y), g#(x, c y) -> f# x) (f# s x -> f# x, f# s x -> f# x) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(s x, y)) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y))) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(x, y)) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> if#(f x, c g(s x, y), c y)) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> f# x) (g#(x, c y) -> f# x, f# s x -> f# x) (g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y)), g#(x, c y) -> f# x) (g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y)), g#(x, c y) -> if#(f x, c g(s x, y), c y)) (g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y)), g#(x, c y) -> g#(x, y)) (g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y)), g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y))) (g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y)), g#(x, c y) -> g#(s x, y))} EDG: {(g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(s x, y)) (g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y))) (g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(x, y)) (g#(x, c y) -> g#(x, y), g#(x, c y) -> if#(f x, c g(s x, y), c y)) (g#(x, c y) -> g#(x, y), g#(x, c y) -> f# x) (f# s x -> f# x, f# s x -> f# x) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(s x, y)) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y))) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(x, y)) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> if#(f x, c g(s x, y), c y)) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> f# x) (g#(x, c y) -> f# x, f# s x -> f# x)} EDG: {(g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(s x, y)) (g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y))) (g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(x, y)) (g#(x, c y) -> g#(x, y), g#(x, c y) -> if#(f x, c g(s x, y), c y)) (g#(x, c y) -> g#(x, y), g#(x, c y) -> f# x) (f# s x -> f# x, f# s x -> f# x) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(s x, y)) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y))) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(x, y)) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> if#(f x, c g(s x, y), c y)) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> f# x) (g#(x, c y) -> f# x, f# s x -> f# x)} EDG: {(g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(s x, y)) (g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y))) (g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(x, y)) (g#(x, c y) -> g#(x, y), g#(x, c y) -> if#(f x, c g(s x, y), c y)) (g#(x, c y) -> g#(x, y), g#(x, c y) -> f# x) (f# s x -> f# x, f# s x -> f# x) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(s x, y)) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y))) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(x, y)) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> if#(f x, c g(s x, y), c y)) (g#(x, c y) -> g#(s x, y), g#(x, c y) -> f# x) (g#(x, c y) -> f# x, f# s x -> f# x)} STATUS: arrows: 0.666667 SCCS (2): Scc: {g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(s x, y)} Scc: {f# s x -> f# x} SCC (2): Strict: {g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(s x, y)} Weak: { f 0() -> true(), f 1() -> false(), f s x -> f x, if(true(), s x, s y) -> s x, if(false(), s x, s y) -> s y, g(x, c y) -> c g(x, y), g(x, c y) -> g(x, if(f x, c g(s x, y), c y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [g](x0, x1) = x0 + 1, [f](x0) = 0, [s](x0) = 1, [c](x0) = x0 + 1, [true] = 0, [0] = 0, [false] = 0, [1] = 0, [g#](x0, x1) = x0 + 1 Strict: g#(x, c y) -> g#(s x, y) 2 + 0x + 1y >= 1 + 0x + 1y g#(x, c y) -> g#(x, y) 2 + 0x + 1y >= 1 + 0x + 1y Weak: g(x, c y) -> g(x, if(f x, c g(s x, y), c y)) 2 + 0x + 1y >= 3 + 0x + 1y g(x, c y) -> c g(x, y) 2 + 0x + 1y >= 2 + 0x + 1y if(false(), s x, s y) -> s y 2 + 0x + 0y >= 1 + 0y if(true(), s x, s y) -> s x 2 + 0x + 0y >= 1 + 0x f s x -> f x 0 + 0x >= 0 + 0x f 1() -> false() 0 >= 0 f 0() -> true() 0 >= 0 Qed SCC (1): Strict: {f# s x -> f# x} Weak: { f 0() -> true(), f 1() -> false(), f s x -> f x, if(true(), s x, s y) -> s x, if(false(), s x, s y) -> s y, g(x, c y) -> c g(x, y), g(x, c y) -> g(x, if(f x, c g(s x, y), c y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [g](x0, x1) = x0 + 1, [f](x0) = 0, [s](x0) = x0 + 1, [c](x0) = x0 + 1, [true] = 0, [0] = 0, [false] = 0, [1] = 0, [f#](x0) = x0 Strict: f# s x -> f# x 1 + 1x >= 0 + 1x Weak: g(x, c y) -> g(x, if(f x, c g(s x, y), c y)) 2 + 0x + 1y >= 3 + 0x + 1y g(x, c y) -> c g(x, y) 2 + 0x + 1y >= 2 + 0x + 1y if(false(), s x, s y) -> s y 2 + 0x + 1y >= 1 + 1y if(true(), s x, s y) -> s x 2 + 0x + 1y >= 1 + 1x f s x -> f x 0 + 0x >= 0 + 0x f 1() -> false() 0 >= 0 f 0() -> true() 0 >= 0 Qed