YES Time: 0.068172 TRS: { 1() -> s 0(), fac 0() -> 1(), fac 0() -> s 0(), fac s x -> *(s x, fac x), *(x, 0()) -> 0(), *(x, s y) -> +(*(x, y), x), floop(0(), y) -> y, floop(s x, y) -> floop(x, *(s x, y)), +(x, 0()) -> x, +(x, s y) -> s +(x, y)} DP: DP: { fac# 0() -> 1#(), fac# s x -> fac# x, fac# s x -> *#(s x, fac x), *#(x, s y) -> *#(x, y), *#(x, s y) -> +#(*(x, y), x), floop#(s x, y) -> *#(s x, y), floop#(s x, y) -> floop#(x, *(s x, y)), +#(x, s y) -> +#(x, y)} TRS: { 1() -> s 0(), fac 0() -> 1(), fac 0() -> s 0(), fac s x -> *(s x, fac x), *(x, 0()) -> 0(), *(x, s y) -> +(*(x, y), x), floop(0(), y) -> y, floop(s x, y) -> floop(x, *(s x, y)), +(x, 0()) -> x, +(x, s y) -> s +(x, y)} EDG: {(floop#(s x, y) -> *#(s x, y), *#(x, s y) -> +#(*(x, y), x)) (floop#(s x, y) -> *#(s x, y), *#(x, s y) -> *#(x, y)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> +#(*(x, y), x)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> *#(x, y)) (fac# s x -> *#(s x, fac x), *#(x, s y) -> +#(*(x, y), x)) (fac# s x -> *#(s x, fac x), *#(x, s y) -> *#(x, y)) (*#(x, s y) -> +#(*(x, y), x), +#(x, s y) -> +#(x, y)) (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y)) (floop#(s x, y) -> floop#(x, *(s x, y)), floop#(s x, y) -> *#(s x, y)) (floop#(s x, y) -> floop#(x, *(s x, y)), floop#(s x, y) -> floop#(x, *(s x, y))) (fac# s x -> fac# x, fac# 0() -> 1#()) (fac# s x -> fac# x, fac# s x -> fac# x) (fac# s x -> fac# x, fac# s x -> *#(s x, fac x))} EDG: {(floop#(s x, y) -> *#(s x, y), *#(x, s y) -> +#(*(x, y), x)) (floop#(s x, y) -> *#(s x, y), *#(x, s y) -> *#(x, y)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> +#(*(x, y), x)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> *#(x, y)) (fac# s x -> *#(s x, fac x), *#(x, s y) -> +#(*(x, y), x)) (fac# s x -> *#(s x, fac x), *#(x, s y) -> *#(x, y)) (*#(x, s y) -> +#(*(x, y), x), +#(x, s y) -> +#(x, y)) (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y)) (floop#(s x, y) -> floop#(x, *(s x, y)), floop#(s x, y) -> *#(s x, y)) (floop#(s x, y) -> floop#(x, *(s x, y)), floop#(s x, y) -> floop#(x, *(s x, y))) (fac# s x -> fac# x, fac# 0() -> 1#()) (fac# s x -> fac# x, fac# s x -> fac# x) (fac# s x -> fac# x, fac# s x -> *#(s x, fac x))} EDG: {(floop#(s x, y) -> *#(s x, y), *#(x, s y) -> +#(*(x, y), x)) (floop#(s x, y) -> *#(s x, y), *#(x, s y) -> *#(x, y)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> +#(*(x, y), x)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> *#(x, y)) (fac# s x -> *#(s x, fac x), *#(x, s y) -> +#(*(x, y), x)) (fac# s x -> *#(s x, fac x), *#(x, s y) -> *#(x, y)) (*#(x, s y) -> +#(*(x, y), x), +#(x, s y) -> +#(x, y)) (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y)) (floop#(s x, y) -> floop#(x, *(s x, y)), floop#(s x, y) -> *#(s x, y)) (floop#(s x, y) -> floop#(x, *(s x, y)), floop#(s x, y) -> floop#(x, *(s x, y))) (fac# s x -> fac# x, fac# 0() -> 1#()) (fac# s x -> fac# x, fac# s x -> fac# x) (fac# s x -> fac# x, fac# s x -> *#(s x, fac x))} EDG: {(floop#(s x, y) -> *#(s x, y), *#(x, s y) -> +#(*(x, y), x)) (floop#(s x, y) -> *#(s x, y), *#(x, s y) -> *#(x, y)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> +#(*(x, y), x)) (*#(x, s y) -> *#(x, y), *#(x, s y) -> *#(x, y)) (fac# s x -> *#(s x, fac x), *#(x, s y) -> +#(*(x, y), x)) (fac# s x -> *#(s x, fac x), *#(x, s y) -> *#(x, y)) (*#(x, s y) -> +#(*(x, y), x), +#(x, s y) -> +#(x, y)) (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y)) (floop#(s x, y) -> floop#(x, *(s x, y)), floop#(s x, y) -> *#(s x, y)) (floop#(s x, y) -> floop#(x, *(s x, y)), floop#(s x, y) -> floop#(x, *(s x, y))) (fac# s x -> fac# x, fac# 0() -> 1#()) (fac# s x -> fac# x, fac# s x -> fac# x) (fac# s x -> fac# x, fac# s x -> *#(s x, fac x))} STATUS: arrows: 0.796875 SCCS (4): Scc: {floop#(s x, y) -> floop#(x, *(s x, y))} Scc: {fac# s x -> fac# x} Scc: {*#(x, s y) -> *#(x, y)} Scc: {+#(x, s y) -> +#(x, y)} SCC (1): Strict: {floop#(s x, y) -> floop#(x, *(s x, y))} Weak: { 1() -> s 0(), fac 0() -> 1(), fac 0() -> s 0(), fac s x -> *(s x, fac x), *(x, 0()) -> 0(), *(x, s y) -> +(*(x, y), x), floop(0(), y) -> y, floop(s x, y) -> floop(x, *(s x, y)), +(x, 0()) -> x, +(x, s y) -> s +(x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [*](x0, x1) = 0, [floop](x0, x1) = 0, [+](x0, x1) = 0, [fac](x0) = x0 + 1, [s](x0) = x0 + 1, [1] = 0, [0] = 1, [floop#](x0, x1) = x0 Strict: floop#(s x, y) -> floop#(x, *(s x, y)) 1 + 1x + 0y >= 0 + 1x + 0y Weak: +(x, s y) -> s +(x, y) 0 + 0x + 0y >= 1 + 0x + 0y +(x, 0()) -> x 0 + 0x >= 1x floop(s x, y) -> floop(x, *(s x, y)) 0 + 0x + 0y >= 0 + 0x + 0y floop(0(), y) -> y 0 + 0y >= 1y *(x, s y) -> +(*(x, y), x) 0 + 0x + 0y >= 0 + 0x + 0y *(x, 0()) -> 0() 0 + 0x >= 1 fac s x -> *(s x, fac x) 2 + 1x >= 0 + 0x fac 0() -> s 0() 2 >= 2 fac 0() -> 1() 2 >= 0 1() -> s 0() 0 >= 2 Qed SCC (1): Strict: {fac# s x -> fac# x} Weak: { 1() -> s 0(), fac 0() -> 1(), fac 0() -> s 0(), fac s x -> *(s x, fac x), *(x, 0()) -> 0(), *(x, s y) -> +(*(x, y), x), floop(0(), y) -> y, floop(s x, y) -> floop(x, *(s x, y)), +(x, 0()) -> x, +(x, s y) -> s +(x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [*](x0, x1) = 0, [floop](x0, x1) = 0, [+](x0, x1) = 0, [fac](x0) = x0 + 1, [s](x0) = x0 + 1, [1] = 0, [0] = 1, [fac#](x0) = x0 Strict: fac# s x -> fac# x 1 + 1x >= 0 + 1x Weak: +(x, s y) -> s +(x, y) 0 + 0x + 0y >= 1 + 0x + 0y +(x, 0()) -> x 0 + 0x >= 1x floop(s x, y) -> floop(x, *(s x, y)) 0 + 0x + 0y >= 0 + 0x + 0y floop(0(), y) -> y 0 + 0y >= 1y *(x, s y) -> +(*(x, y), x) 0 + 0x + 0y >= 0 + 0x + 0y *(x, 0()) -> 0() 0 + 0x >= 1 fac s x -> *(s x, fac x) 2 + 1x >= 0 + 0x fac 0() -> s 0() 2 >= 2 fac 0() -> 1() 2 >= 0 1() -> s 0() 0 >= 2 Qed SCC (1): Strict: {*#(x, s y) -> *#(x, y)} Weak: { 1() -> s 0(), fac 0() -> 1(), fac 0() -> s 0(), fac s x -> *(s x, fac x), *(x, 0()) -> 0(), *(x, s y) -> +(*(x, y), x), floop(0(), y) -> y, floop(s x, y) -> floop(x, *(s x, y)), +(x, 0()) -> x, +(x, s y) -> s +(x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [*](x0, x1) = 0, [floop](x0, x1) = 0, [+](x0, x1) = 0, [fac](x0) = x0 + 1, [s](x0) = x0 + 1, [1] = 0, [0] = 1, [*#](x0, x1) = x0 Strict: *#(x, s y) -> *#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: +(x, s y) -> s +(x, y) 0 + 0x + 0y >= 1 + 0x + 0y +(x, 0()) -> x 0 + 0x >= 1x floop(s x, y) -> floop(x, *(s x, y)) 0 + 0x + 0y >= 0 + 0x + 0y floop(0(), y) -> y 0 + 0y >= 1y *(x, s y) -> +(*(x, y), x) 0 + 0x + 0y >= 0 + 0x + 0y *(x, 0()) -> 0() 0 + 0x >= 1 fac s x -> *(s x, fac x) 2 + 1x >= 0 + 0x fac 0() -> s 0() 2 >= 2 fac 0() -> 1() 2 >= 0 1() -> s 0() 0 >= 2 Qed SCC (1): Strict: {+#(x, s y) -> +#(x, y)} Weak: { 1() -> s 0(), fac 0() -> 1(), fac 0() -> s 0(), fac s x -> *(s x, fac x), *(x, 0()) -> 0(), *(x, s y) -> +(*(x, y), x), floop(0(), y) -> y, floop(s x, y) -> floop(x, *(s x, y)), +(x, 0()) -> x, +(x, s y) -> s +(x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [*](x0, x1) = 0, [floop](x0, x1) = 0, [+](x0, x1) = 0, [fac](x0) = x0 + 1, [s](x0) = x0 + 1, [1] = 0, [0] = 1, [+#](x0, x1) = x0 Strict: +#(x, s y) -> +#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: +(x, s y) -> s +(x, y) 0 + 0x + 0y >= 1 + 0x + 0y +(x, 0()) -> x 0 + 0x >= 1x floop(s x, y) -> floop(x, *(s x, y)) 0 + 0x + 0y >= 0 + 0x + 0y floop(0(), y) -> y 0 + 0y >= 1y *(x, s y) -> +(*(x, y), x) 0 + 0x + 0y >= 0 + 0x + 0y *(x, 0()) -> 0() 0 + 0x >= 1 fac s x -> *(s x, fac x) 2 + 1x >= 0 + 0x fac 0() -> s 0() 2 >= 2 fac 0() -> 1() 2 >= 0 1() -> s 0() 0 >= 2 Qed