MAYBE Time: 0.043677 TRS: { from X -> cons(X, from s X), 2ndspos(s N, cons(X, cons(Y, Z))) -> rcons(posrecip Y, 2ndsneg(N, Z)), 2ndspos(0(), Z) -> rnil(), 2ndsneg(s N, cons(X, cons(Y, Z))) -> rcons(negrecip Y, 2ndspos(N, Z)), 2ndsneg(0(), Z) -> rnil(), pi X -> 2ndspos(X, from 0()), plus(s X, Y) -> s plus(X, Y), plus(0(), Y) -> Y, times(s X, Y) -> plus(Y, times(X, Y)), times(0(), Y) -> 0(), square X -> times(X, X)} DP: DP: { from# X -> from# s X, 2ndspos#(s N, cons(X, cons(Y, Z))) -> 2ndsneg#(N, Z), 2ndsneg#(s N, cons(X, cons(Y, Z))) -> 2ndspos#(N, Z), pi# X -> from# 0(), pi# X -> 2ndspos#(X, from 0()), plus#(s X, Y) -> plus#(X, Y), times#(s X, Y) -> plus#(Y, times(X, Y)), times#(s X, Y) -> times#(X, Y), square# X -> times#(X, X)} TRS: { from X -> cons(X, from s X), 2ndspos(s N, cons(X, cons(Y, Z))) -> rcons(posrecip Y, 2ndsneg(N, Z)), 2ndspos(0(), Z) -> rnil(), 2ndsneg(s N, cons(X, cons(Y, Z))) -> rcons(negrecip Y, 2ndspos(N, Z)), 2ndsneg(0(), Z) -> rnil(), pi X -> 2ndspos(X, from 0()), plus(s X, Y) -> s plus(X, Y), plus(0(), Y) -> Y, times(s X, Y) -> plus(Y, times(X, Y)), times(0(), Y) -> 0(), square X -> times(X, X)} UR: { from X -> cons(X, from s X), plus(s X, Y) -> s plus(X, Y), plus(0(), Y) -> Y, times(s X, Y) -> plus(Y, times(X, Y)), times(0(), Y) -> 0(), a(x, y) -> x, a(x, y) -> y} EDG: {(times#(s X, Y) -> times#(X, Y), times#(s X, Y) -> times#(X, Y)) (times#(s X, Y) -> times#(X, Y), times#(s X, Y) -> plus#(Y, times(X, Y))) (2ndsneg#(s N, cons(X, cons(Y, Z))) -> 2ndspos#(N, Z), 2ndspos#(s N, cons(X, cons(Y, Z))) -> 2ndsneg#(N, Z)) (from# X -> from# s X, from# X -> from# s X) (pi# X -> 2ndspos#(X, from 0()), 2ndspos#(s N, cons(X, cons(Y, Z))) -> 2ndsneg#(N, Z)) (times#(s X, Y) -> plus#(Y, times(X, Y)), plus#(s X, Y) -> plus#(X, Y)) (pi# X -> from# 0(), from# X -> from# s X) (square# X -> times#(X, X), times#(s X, Y) -> plus#(Y, times(X, Y))) (square# X -> times#(X, X), times#(s X, Y) -> times#(X, Y)) (2ndspos#(s N, cons(X, cons(Y, Z))) -> 2ndsneg#(N, Z), 2ndsneg#(s N, cons(X, cons(Y, Z))) -> 2ndspos#(N, Z)) (plus#(s X, Y) -> plus#(X, Y), plus#(s X, Y) -> plus#(X, Y))} STATUS: arrows: 0.864198 SCCS (4): Scc: {from# X -> from# s X} Scc: {2ndspos#(s N, cons(X, cons(Y, Z))) -> 2ndsneg#(N, Z), 2ndsneg#(s N, cons(X, cons(Y, Z))) -> 2ndspos#(N, Z)} Scc: {times#(s X, Y) -> times#(X, Y)} Scc: {plus#(s X, Y) -> plus#(X, Y)} SCC (1): Strict: {from# X -> from# s X} Weak: { from X -> cons(X, from s X), 2ndspos(s N, cons(X, cons(Y, Z))) -> rcons(posrecip Y, 2ndsneg(N, Z)), 2ndspos(0(), Z) -> rnil(), 2ndsneg(s N, cons(X, cons(Y, Z))) -> rcons(negrecip Y, 2ndspos(N, Z)), 2ndsneg(0(), Z) -> rnil(), pi X -> 2ndspos(X, from 0()), plus(s X, Y) -> s plus(X, Y), plus(0(), Y) -> Y, times(s X, Y) -> plus(Y, times(X, Y)), times(0(), Y) -> 0(), square X -> times(X, X)} Fail SCC (2): Strict: {2ndspos#(s N, cons(X, cons(Y, Z))) -> 2ndsneg#(N, Z), 2ndsneg#(s N, cons(X, cons(Y, Z))) -> 2ndspos#(N, Z)} Weak: { from X -> cons(X, from s X), 2ndspos(s N, cons(X, cons(Y, Z))) -> rcons(posrecip Y, 2ndsneg(N, Z)), 2ndspos(0(), Z) -> rnil(), 2ndsneg(s N, cons(X, cons(Y, Z))) -> rcons(negrecip Y, 2ndspos(N, Z)), 2ndsneg(0(), Z) -> rnil(), pi X -> 2ndspos(X, from 0()), plus(s X, Y) -> s plus(X, Y), plus(0(), Y) -> Y, times(s X, Y) -> plus(Y, times(X, Y)), times(0(), Y) -> 0(), square X -> times(X, X)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + 1, [2ndspos](x0, x1) = x0 + 1, [rcons](x0, x1) = 0, [2ndsneg](x0, x1) = x0 + 1, [plus](x0, x1) = x0 + 1, [times](x0, x1) = 0, [from](x0) = 0, [s](x0) = x0 + 1, [posrecip](x0) = 0, [negrecip](x0) = 0, [pi](x0) = 0, [square](x0) = 0, [rnil] = 0, [0] = 1, [2ndspos#](x0, x1) = x0 + 1, [2ndsneg#](x0, x1) = x0 + 1 Strict: 2ndsneg#(s N, cons(X, cons(Y, Z))) -> 2ndspos#(N, Z) 2 + 0X + 0Z + 0Y + 1N >= 1 + 0Z + 1N 2ndspos#(s N, cons(X, cons(Y, Z))) -> 2ndsneg#(N, Z) 2 + 0X + 0Z + 0Y + 1N >= 1 + 0Z + 1N Weak: square X -> times(X, X) 0 + 0X >= 0 + 0X times(0(), Y) -> 0() 0 + 0Y >= 1 times(s X, Y) -> plus(Y, times(X, Y)) 0 + 0X + 0Y >= 1 + 0X + 1Y plus(0(), Y) -> Y 2 + 0Y >= 1Y plus(s X, Y) -> s plus(X, Y) 2 + 1X + 0Y >= 2 + 1X + 0Y pi X -> 2ndspos(X, from 0()) 0 + 0X >= 1 + 1X 2ndsneg(0(), Z) -> rnil() 2 + 0Z >= 0 2ndsneg(s N, cons(X, cons(Y, Z))) -> rcons(negrecip Y, 2ndspos(N, Z)) 2 + 0X + 0Z + 0Y + 1N >= 0 + 0Z + 0Y + 0N 2ndspos(0(), Z) -> rnil() 2 + 0Z >= 0 2ndspos(s N, cons(X, cons(Y, Z))) -> rcons(posrecip Y, 2ndsneg(N, Z)) 2 + 0X + 0Z + 0Y + 1N >= 0 + 0Z + 0Y + 0N from X -> cons(X, from s X) 0 + 0X >= 1 + 0X Qed SCC (1): Strict: {times#(s X, Y) -> times#(X, Y)} Weak: { from X -> cons(X, from s X), 2ndspos(s N, cons(X, cons(Y, Z))) -> rcons(posrecip Y, 2ndsneg(N, Z)), 2ndspos(0(), Z) -> rnil(), 2ndsneg(s N, cons(X, cons(Y, Z))) -> rcons(negrecip Y, 2ndspos(N, Z)), 2ndsneg(0(), Z) -> rnil(), pi X -> 2ndspos(X, from 0()), plus(s X, Y) -> s plus(X, Y), plus(0(), Y) -> Y, times(s X, Y) -> plus(Y, times(X, Y)), times(0(), Y) -> 0(), square X -> times(X, X)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [2ndspos](x0, x1) = 0, [rcons](x0, x1) = 0, [2ndsneg](x0, x1) = x0 + 1, [plus](x0, x1) = 0, [times](x0, x1) = x0 + 1, [from](x0) = x0 + 1, [s](x0) = x0 + 1, [posrecip](x0) = 0, [negrecip](x0) = 0, [pi](x0) = 0, [square](x0) = 0, [rnil] = 0, [0] = 1, [times#](x0, x1) = x0 Strict: times#(s X, Y) -> times#(X, Y) 1 + 1X + 0Y >= 0 + 1X + 0Y Weak: square X -> times(X, X) 0 + 0X >= 1 + 1X times(0(), Y) -> 0() 2 + 0Y >= 1 times(s X, Y) -> plus(Y, times(X, Y)) 2 + 1X + 0Y >= 0 + 0X + 0Y plus(0(), Y) -> Y 0 + 0Y >= 1Y plus(s X, Y) -> s plus(X, Y) 0 + 0X + 0Y >= 1 + 0X + 0Y pi X -> 2ndspos(X, from 0()) 0 + 0X >= 0 + 0X 2ndsneg(0(), Z) -> rnil() 2 + 0Z >= 0 2ndsneg(s N, cons(X, cons(Y, Z))) -> rcons(negrecip Y, 2ndspos(N, Z)) 2 + 0X + 0Z + 0Y + 1N >= 0 + 0Z + 0Y + 0N 2ndspos(0(), Z) -> rnil() 0 + 0Z >= 0 2ndspos(s N, cons(X, cons(Y, Z))) -> rcons(posrecip Y, 2ndsneg(N, Z)) 0 + 0X + 0Z + 0Y + 0N >= 0 + 0Z + 0Y + 0N from X -> cons(X, from s X) 1 + 1X >= 0 + 0X Qed SCC (1): Strict: {plus#(s X, Y) -> plus#(X, Y)} Weak: { from X -> cons(X, from s X), 2ndspos(s N, cons(X, cons(Y, Z))) -> rcons(posrecip Y, 2ndsneg(N, Z)), 2ndspos(0(), Z) -> rnil(), 2ndsneg(s N, cons(X, cons(Y, Z))) -> rcons(negrecip Y, 2ndspos(N, Z)), 2ndsneg(0(), Z) -> rnil(), pi X -> 2ndspos(X, from 0()), plus(s X, Y) -> s plus(X, Y), plus(0(), Y) -> Y, times(s X, Y) -> plus(Y, times(X, Y)), times(0(), Y) -> 0(), square X -> times(X, X)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [2ndspos](x0, x1) = 0, [rcons](x0, x1) = 0, [2ndsneg](x0, x1) = x0 + 1, [plus](x0, x1) = 0, [times](x0, x1) = x0 + 1, [from](x0) = x0 + 1, [s](x0) = x0 + 1, [posrecip](x0) = 0, [negrecip](x0) = 0, [pi](x0) = 0, [square](x0) = 0, [rnil] = 0, [0] = 1, [plus#](x0, x1) = x0 Strict: plus#(s X, Y) -> plus#(X, Y) 1 + 1X + 0Y >= 0 + 1X + 0Y Weak: square X -> times(X, X) 0 + 0X >= 1 + 1X times(0(), Y) -> 0() 2 + 0Y >= 1 times(s X, Y) -> plus(Y, times(X, Y)) 2 + 1X + 0Y >= 0 + 0X + 0Y plus(0(), Y) -> Y 0 + 0Y >= 1Y plus(s X, Y) -> s plus(X, Y) 0 + 0X + 0Y >= 1 + 0X + 0Y pi X -> 2ndspos(X, from 0()) 0 + 0X >= 0 + 0X 2ndsneg(0(), Z) -> rnil() 2 + 0Z >= 0 2ndsneg(s N, cons(X, cons(Y, Z))) -> rcons(negrecip Y, 2ndspos(N, Z)) 2 + 0X + 0Z + 0Y + 1N >= 0 + 0Z + 0Y + 0N 2ndspos(0(), Z) -> rnil() 0 + 0Z >= 0 2ndspos(s N, cons(X, cons(Y, Z))) -> rcons(posrecip Y, 2ndsneg(N, Z)) 0 + 0X + 0Z + 0Y + 0N >= 0 + 0Z + 0Y + 0N from X -> cons(X, from s X) 1 + 1X >= 0 + 0X Qed