MAYBE
Time: 0.066823
TRS:
{ mark cons(X1, X2) -> cons(mark X1, X2),
mark from X -> a__from mark X,
mark s X -> s mark X,
mark rnil() -> rnil(),
mark 0() -> 0(),
mark rcons(X1, X2) -> rcons(mark X1, mark X2),
mark posrecip X -> posrecip mark X,
mark negrecip X -> negrecip mark X,
mark 2ndspos(X1, X2) -> a__2ndspos(mark X1, mark X2),
mark 2ndsneg(X1, X2) -> a__2ndsneg(mark X1, mark X2),
mark pi X -> a__pi mark X,
mark plus(X1, X2) -> a__plus(mark X1, mark X2),
mark times(X1, X2) -> a__times(mark X1, mark X2),
mark square X -> a__square mark X,
mark nil() -> nil(),
a__from X -> cons(mark X, from s X),
a__from X -> from X,
a__2ndspos(X1, X2) -> 2ndspos(X1, X2),
a__2ndspos(s N, cons(X, cons(Y, Z))) -> rcons(posrecip mark Y, a__2ndsneg(mark N, mark Z)),
a__2ndspos(0(), Z) -> rnil(),
a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2),
a__2ndsneg(s N, cons(X, cons(Y, Z))) -> rcons(negrecip mark Y, a__2ndspos(mark N, mark Z)),
a__2ndsneg(0(), Z) -> rnil(),
a__pi X -> a__2ndspos(mark X, a__from 0()),
a__pi X -> pi X,
a__plus(X1, X2) -> plus(X1, X2),
a__plus(s X, Y) -> s a__plus(mark X, mark Y),
a__plus(0(), Y) -> mark Y,
a__times(X1, X2) -> times(X1, X2),
a__times(s X, Y) -> a__plus(mark Y, a__times(mark X, mark Y)),
a__times(0(), Y) -> 0(),
a__square X -> a__times(mark X, mark X),
a__square X -> square X}
DP:
DP:
{ mark# cons(X1, X2) -> mark# X1,
mark# from X -> mark# X,
mark# from X -> a__from# mark X,
mark# s X -> mark# X,
mark# rcons(X1, X2) -> mark# X1,
mark# rcons(X1, X2) -> mark# X2,
mark# posrecip X -> mark# X,
mark# negrecip X -> mark# X,
mark# 2ndspos(X1, X2) -> mark# X1,
mark# 2ndspos(X1, X2) -> mark# X2,
mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2),
mark# 2ndsneg(X1, X2) -> mark# X1,
mark# 2ndsneg(X1, X2) -> mark# X2,
mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2),
mark# pi X -> mark# X,
mark# pi X -> a__pi# mark X,
mark# plus(X1, X2) -> mark# X1,
mark# plus(X1, X2) -> mark# X2,
mark# plus(X1, X2) -> a__plus#(mark X1, mark X2),
mark# times(X1, X2) -> mark# X1,
mark# times(X1, X2) -> mark# X2,
mark# times(X1, X2) -> a__times#(mark X1, mark X2),
mark# square X -> mark# X,
mark# square X -> a__square# mark X,
a__from# X -> mark# X,
a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z,
a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y,
a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N,
a__2ndspos#(s N, cons(X, cons(Y, Z))) -> a__2ndsneg#(mark N, mark Z),
a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z,
a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y,
a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N,
a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> a__2ndspos#(mark N, mark Z),
a__pi# X -> mark# X,
a__pi# X -> a__from# 0(),
a__pi# X -> a__2ndspos#(mark X, a__from 0()),
a__plus#(s X, Y) -> mark# X,
a__plus#(s X, Y) -> mark# Y,
a__plus#(s X, Y) -> a__plus#(mark X, mark Y),
a__plus#(0(), Y) -> mark# Y,
a__times#(s X, Y) -> mark# X,
a__times#(s X, Y) -> mark# Y,
a__times#(s X, Y) -> a__plus#(mark Y, a__times(mark X, mark Y)),
a__times#(s X, Y) -> a__times#(mark X, mark Y),
a__square# X -> mark# X,
a__square# X -> a__times#(mark X, mark X)}
TRS:
{ mark cons(X1, X2) -> cons(mark X1, X2),
mark from X -> a__from mark X,
mark s X -> s mark X,
mark rnil() -> rnil(),
mark 0() -> 0(),
mark rcons(X1, X2) -> rcons(mark X1, mark X2),
mark posrecip X -> posrecip mark X,
mark negrecip X -> negrecip mark X,
mark 2ndspos(X1, X2) -> a__2ndspos(mark X1, mark X2),
mark 2ndsneg(X1, X2) -> a__2ndsneg(mark X1, mark X2),
mark pi X -> a__pi mark X,
mark plus(X1, X2) -> a__plus(mark X1, mark X2),
mark times(X1, X2) -> a__times(mark X1, mark X2),
mark square X -> a__square mark X,
mark nil() -> nil(),
a__from X -> cons(mark X, from s X),
a__from X -> from X,
a__2ndspos(X1, X2) -> 2ndspos(X1, X2),
a__2ndspos(s N, cons(X, cons(Y, Z))) -> rcons(posrecip mark Y, a__2ndsneg(mark N, mark Z)),
a__2ndspos(0(), Z) -> rnil(),
a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2),
a__2ndsneg(s N, cons(X, cons(Y, Z))) -> rcons(negrecip mark Y, a__2ndspos(mark N, mark Z)),
a__2ndsneg(0(), Z) -> rnil(),
a__pi X -> a__2ndspos(mark X, a__from 0()),
a__pi X -> pi X,
a__plus(X1, X2) -> plus(X1, X2),
a__plus(s X, Y) -> s a__plus(mark X, mark Y),
a__plus(0(), Y) -> mark Y,
a__times(X1, X2) -> times(X1, X2),
a__times(s X, Y) -> a__plus(mark Y, a__times(mark X, mark Y)),
a__times(0(), Y) -> 0(),
a__square X -> a__times(mark X, mark X),
a__square X -> square X}
UR:
{ mark cons(X1, X2) -> cons(mark X1, X2),
mark from X -> a__from mark X,
mark s X -> s mark X,
mark rnil() -> rnil(),
mark 0() -> 0(),
mark rcons(X1, X2) -> rcons(mark X1, mark X2),
mark posrecip X -> posrecip mark X,
mark negrecip X -> negrecip mark X,
mark 2ndspos(X1, X2) -> a__2ndspos(mark X1, mark X2),
mark 2ndsneg(X1, X2) -> a__2ndsneg(mark X1, mark X2),
mark pi X -> a__pi mark X,
mark plus(X1, X2) -> a__plus(mark X1, mark X2),
mark times(X1, X2) -> a__times(mark X1, mark X2),
mark square X -> a__square mark X,
mark nil() -> nil(),
a__from X -> cons(mark X, from s X),
a__from X -> from X,
a__2ndspos(X1, X2) -> 2ndspos(X1, X2),
a__2ndspos(s N, cons(X, cons(Y, Z))) -> rcons(posrecip mark Y, a__2ndsneg(mark N, mark Z)),
a__2ndspos(0(), Z) -> rnil(),
a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2),
a__2ndsneg(s N, cons(X, cons(Y, Z))) -> rcons(negrecip mark Y, a__2ndspos(mark N, mark Z)),
a__2ndsneg(0(), Z) -> rnil(),
a__pi X -> a__2ndspos(mark X, a__from 0()),
a__pi X -> pi X,
a__plus(X1, X2) -> plus(X1, X2),
a__plus(s X, Y) -> s a__plus(mark X, mark Y),
a__plus(0(), Y) -> mark Y,
a__times(X1, X2) -> times(X1, X2),
a__times(s X, Y) -> a__plus(mark Y, a__times(mark X, mark Y)),
a__times(0(), Y) -> 0(),
a__square X -> a__times(mark X, mark X),
a__square X -> square X,
a(x, y) -> x,
a(x, y) -> y}
EDG:
{
(mark# from X -> a__from# mark X, a__from# X -> mark# X)
(mark# square X -> a__square# mark X, a__square# X -> a__times#(mark X, mark X))
(mark# square X -> a__square# mark X, a__square# X -> mark# X)
(mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2), a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> a__2ndspos#(mark N, mark Z))
(mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2), a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N)
(mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2), a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y)
(mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2), a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z)
(mark# times(X1, X2) -> a__times#(mark X1, mark X2), a__times#(s X, Y) -> a__times#(mark X, mark Y))
(mark# times(X1, X2) -> a__times#(mark X1, mark X2), a__times#(s X, Y) -> a__plus#(mark Y, a__times(mark X, mark Y)))
(mark# times(X1, X2) -> a__times#(mark X1, mark X2), a__times#(s X, Y) -> mark# Y)
(mark# times(X1, X2) -> a__times#(mark X1, mark X2), a__times#(s X, Y) -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> a__2ndspos#(mark N, mark Z), a__2ndspos#(s N, cons(X, cons(Y, Z))) -> a__2ndsneg#(mark N, mark Z))
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> a__2ndspos#(mark N, mark Z), a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> a__2ndspos#(mark N, mark Z), a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> a__2ndspos#(mark N, mark Z), a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z)
(a__times#(s X, Y) -> a__times#(mark X, mark Y), a__times#(s X, Y) -> a__times#(mark X, mark Y))
(a__times#(s X, Y) -> a__times#(mark X, mark Y), a__times#(s X, Y) -> a__plus#(mark Y, a__times(mark X, mark Y)))
(a__times#(s X, Y) -> a__times#(mark X, mark Y), a__times#(s X, Y) -> mark# Y)
(a__times#(s X, Y) -> a__times#(mark X, mark Y), a__times#(s X, Y) -> mark# X)
(mark# cons(X1, X2) -> mark# X1, mark# square X -> a__square# mark X)
(mark# cons(X1, X2) -> mark# X1, mark# square X -> mark# X)
(mark# cons(X1, X2) -> mark# X1, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# cons(X1, X2) -> mark# X1, mark# times(X1, X2) -> mark# X2)
(mark# cons(X1, X2) -> mark# X1, mark# times(X1, X2) -> mark# X1)
(mark# cons(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# cons(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
(mark# cons(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
(mark# cons(X1, X2) -> mark# X1, mark# pi X -> a__pi# mark X)
(mark# cons(X1, X2) -> mark# X1, mark# pi X -> mark# X)
(mark# cons(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# cons(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# cons(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# cons(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# cons(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# cons(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# cons(X1, X2) -> mark# X1, mark# negrecip X -> mark# X)
(mark# cons(X1, X2) -> mark# X1, mark# posrecip X -> mark# X)
(mark# cons(X1, X2) -> mark# X1, mark# rcons(X1, X2) -> mark# X2)
(mark# cons(X1, X2) -> mark# X1, mark# rcons(X1, X2) -> mark# X1)
(mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
(mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
(mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
(mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# square X -> a__square# mark X)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# square X -> mark# X)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# 2ndspos(X1, X2) -> mark# X1, mark# times(X1, X2) -> mark# X2)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# times(X1, X2) -> mark# X1)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# 2ndspos(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# pi X -> a__pi# mark X)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# pi X -> mark# X)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# 2ndspos(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# 2ndspos(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# negrecip X -> mark# X)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# posrecip X -> mark# X)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# rcons(X1, X2) -> mark# X2)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# rcons(X1, X2) -> mark# X1)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# s X -> mark# X)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# from X -> mark# X)
(mark# 2ndspos(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
(mark# plus(X1, X2) -> mark# X1, mark# square X -> a__square# mark X)
(mark# plus(X1, X2) -> mark# X1, mark# square X -> mark# X)
(mark# plus(X1, X2) -> mark# X1, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# plus(X1, X2) -> mark# X1, mark# times(X1, X2) -> mark# X2)
(mark# plus(X1, X2) -> mark# X1, mark# times(X1, X2) -> mark# X1)
(mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
(mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
(mark# plus(X1, X2) -> mark# X1, mark# pi X -> a__pi# mark X)
(mark# plus(X1, X2) -> mark# X1, mark# pi X -> mark# X)
(mark# plus(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# plus(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# plus(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# plus(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# plus(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# plus(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# plus(X1, X2) -> mark# X1, mark# negrecip X -> mark# X)
(mark# plus(X1, X2) -> mark# X1, mark# posrecip X -> mark# X)
(mark# plus(X1, X2) -> mark# X1, mark# rcons(X1, X2) -> mark# X2)
(mark# plus(X1, X2) -> mark# X1, mark# rcons(X1, X2) -> mark# X1)
(mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X)
(mark# plus(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
(mark# plus(X1, X2) -> mark# X1, mark# from X -> mark# X)
(mark# plus(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
(mark# from X -> mark# X, mark# square X -> a__square# mark X)
(mark# from X -> mark# X, mark# square X -> mark# X)
(mark# from X -> mark# X, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# from X -> mark# X, mark# times(X1, X2) -> mark# X2)
(mark# from X -> mark# X, mark# times(X1, X2) -> mark# X1)
(mark# from X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# from X -> mark# X, mark# plus(X1, X2) -> mark# X2)
(mark# from X -> mark# X, mark# plus(X1, X2) -> mark# X1)
(mark# from X -> mark# X, mark# pi X -> a__pi# mark X)
(mark# from X -> mark# X, mark# pi X -> mark# X)
(mark# from X -> mark# X, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# from X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# from X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# from X -> mark# X, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# from X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# from X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# from X -> mark# X, mark# negrecip X -> mark# X)
(mark# from X -> mark# X, mark# posrecip X -> mark# X)
(mark# from X -> mark# X, mark# rcons(X1, X2) -> mark# X2)
(mark# from X -> mark# X, mark# rcons(X1, X2) -> mark# X1)
(mark# from X -> mark# X, mark# s X -> mark# X)
(mark# from X -> mark# X, mark# from X -> a__from# mark X)
(mark# from X -> mark# X, mark# from X -> mark# X)
(mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
(mark# posrecip X -> mark# X, mark# square X -> a__square# mark X)
(mark# posrecip X -> mark# X, mark# square X -> mark# X)
(mark# posrecip X -> mark# X, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# posrecip X -> mark# X, mark# times(X1, X2) -> mark# X2)
(mark# posrecip X -> mark# X, mark# times(X1, X2) -> mark# X1)
(mark# posrecip X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# posrecip X -> mark# X, mark# plus(X1, X2) -> mark# X2)
(mark# posrecip X -> mark# X, mark# plus(X1, X2) -> mark# X1)
(mark# posrecip X -> mark# X, mark# pi X -> a__pi# mark X)
(mark# posrecip X -> mark# X, mark# pi X -> mark# X)
(mark# posrecip X -> mark# X, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# posrecip X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# posrecip X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# posrecip X -> mark# X, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# posrecip X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# posrecip X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# posrecip X -> mark# X, mark# negrecip X -> mark# X)
(mark# posrecip X -> mark# X, mark# posrecip X -> mark# X)
(mark# posrecip X -> mark# X, mark# rcons(X1, X2) -> mark# X2)
(mark# posrecip X -> mark# X, mark# rcons(X1, X2) -> mark# X1)
(mark# posrecip X -> mark# X, mark# s X -> mark# X)
(mark# posrecip X -> mark# X, mark# from X -> a__from# mark X)
(mark# posrecip X -> mark# X, mark# from X -> mark# X)
(mark# posrecip X -> mark# X, mark# cons(X1, X2) -> mark# X1)
(mark# pi X -> mark# X, mark# square X -> a__square# mark X)
(mark# pi X -> mark# X, mark# square X -> mark# X)
(mark# pi X -> mark# X, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# pi X -> mark# X, mark# times(X1, X2) -> mark# X2)
(mark# pi X -> mark# X, mark# times(X1, X2) -> mark# X1)
(mark# pi X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# pi X -> mark# X, mark# plus(X1, X2) -> mark# X2)
(mark# pi X -> mark# X, mark# plus(X1, X2) -> mark# X1)
(mark# pi X -> mark# X, mark# pi X -> a__pi# mark X)
(mark# pi X -> mark# X, mark# pi X -> mark# X)
(mark# pi X -> mark# X, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# pi X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# pi X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# pi X -> mark# X, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# pi X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# pi X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# pi X -> mark# X, mark# negrecip X -> mark# X)
(mark# pi X -> mark# X, mark# posrecip X -> mark# X)
(mark# pi X -> mark# X, mark# rcons(X1, X2) -> mark# X2)
(mark# pi X -> mark# X, mark# rcons(X1, X2) -> mark# X1)
(mark# pi X -> mark# X, mark# s X -> mark# X)
(mark# pi X -> mark# X, mark# from X -> a__from# mark X)
(mark# pi X -> mark# X, mark# from X -> mark# X)
(mark# pi X -> mark# X, mark# cons(X1, X2) -> mark# X1)
(a__from# X -> mark# X, mark# square X -> a__square# mark X)
(a__from# X -> mark# X, mark# square X -> mark# X)
(a__from# X -> mark# X, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(a__from# X -> mark# X, mark# times(X1, X2) -> mark# X2)
(a__from# X -> mark# X, mark# times(X1, X2) -> mark# X1)
(a__from# X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(a__from# X -> mark# X, mark# plus(X1, X2) -> mark# X2)
(a__from# X -> mark# X, mark# plus(X1, X2) -> mark# X1)
(a__from# X -> mark# X, mark# pi X -> a__pi# mark X)
(a__from# X -> mark# X, mark# pi X -> mark# X)
(a__from# X -> mark# X, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(a__from# X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X2)
(a__from# X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X1)
(a__from# X -> mark# X, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(a__from# X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X2)
(a__from# X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X1)
(a__from# X -> mark# X, mark# negrecip X -> mark# X)
(a__from# X -> mark# X, mark# posrecip X -> mark# X)
(a__from# X -> mark# X, mark# rcons(X1, X2) -> mark# X2)
(a__from# X -> mark# X, mark# rcons(X1, X2) -> mark# X1)
(a__from# X -> mark# X, mark# s X -> mark# X)
(a__from# X -> mark# X, mark# from X -> a__from# mark X)
(a__from# X -> mark# X, mark# from X -> mark# X)
(a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1)
(a__plus#(s X, Y) -> mark# X, mark# square X -> a__square# mark X)
(a__plus#(s X, Y) -> mark# X, mark# square X -> mark# X)
(a__plus#(s X, Y) -> mark# X, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(a__plus#(s X, Y) -> mark# X, mark# times(X1, X2) -> mark# X2)
(a__plus#(s X, Y) -> mark# X, mark# times(X1, X2) -> mark# X1)
(a__plus#(s X, Y) -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(a__plus#(s X, Y) -> mark# X, mark# plus(X1, X2) -> mark# X2)
(a__plus#(s X, Y) -> mark# X, mark# plus(X1, X2) -> mark# X1)
(a__plus#(s X, Y) -> mark# X, mark# pi X -> a__pi# mark X)
(a__plus#(s X, Y) -> mark# X, mark# pi X -> mark# X)
(a__plus#(s X, Y) -> mark# X, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(a__plus#(s X, Y) -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X2)
(a__plus#(s X, Y) -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X1)
(a__plus#(s X, Y) -> mark# X, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(a__plus#(s X, Y) -> mark# X, mark# 2ndspos(X1, X2) -> mark# X2)
(a__plus#(s X, Y) -> mark# X, mark# 2ndspos(X1, X2) -> mark# X1)
(a__plus#(s X, Y) -> mark# X, mark# negrecip X -> mark# X)
(a__plus#(s X, Y) -> mark# X, mark# posrecip X -> mark# X)
(a__plus#(s X, Y) -> mark# X, mark# rcons(X1, X2) -> mark# X2)
(a__plus#(s X, Y) -> mark# X, mark# rcons(X1, X2) -> mark# X1)
(a__plus#(s X, Y) -> mark# X, mark# s X -> mark# X)
(a__plus#(s X, Y) -> mark# X, mark# from X -> a__from# mark X)
(a__plus#(s X, Y) -> mark# X, mark# from X -> mark# X)
(a__plus#(s X, Y) -> mark# X, mark# cons(X1, X2) -> mark# X1)
(a__square# X -> mark# X, mark# square X -> a__square# mark X)
(a__square# X -> mark# X, mark# square X -> mark# X)
(a__square# X -> mark# X, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(a__square# X -> mark# X, mark# times(X1, X2) -> mark# X2)
(a__square# X -> mark# X, mark# times(X1, X2) -> mark# X1)
(a__square# X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(a__square# X -> mark# X, mark# plus(X1, X2) -> mark# X2)
(a__square# X -> mark# X, mark# plus(X1, X2) -> mark# X1)
(a__square# X -> mark# X, mark# pi X -> a__pi# mark X)
(a__square# X -> mark# X, mark# pi X -> mark# X)
(a__square# X -> mark# X, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(a__square# X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X2)
(a__square# X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X1)
(a__square# X -> mark# X, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(a__square# X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X2)
(a__square# X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X1)
(a__square# X -> mark# X, mark# negrecip X -> mark# X)
(a__square# X -> mark# X, mark# posrecip X -> mark# X)
(a__square# X -> mark# X, mark# rcons(X1, X2) -> mark# X2)
(a__square# X -> mark# X, mark# rcons(X1, X2) -> mark# X1)
(a__square# X -> mark# X, mark# s X -> mark# X)
(a__square# X -> mark# X, mark# from X -> a__from# mark X)
(a__square# X -> mark# X, mark# from X -> mark# X)
(a__square# X -> mark# X, mark# cons(X1, X2) -> mark# X1)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# square X -> a__square# mark X)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# square X -> mark# X)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# 2ndspos(X1, X2) -> mark# X2, mark# times(X1, X2) -> mark# X2)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# times(X1, X2) -> mark# X1)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# 2ndspos(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# pi X -> a__pi# mark X)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# pi X -> mark# X)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# 2ndspos(X1, X2) -> mark# X2, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# 2ndspos(X1, X2) -> mark# X2, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# negrecip X -> mark# X)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# posrecip X -> mark# X)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# rcons(X1, X2) -> mark# X2)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# rcons(X1, X2) -> mark# X1)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# s X -> mark# X)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# from X -> mark# X)
(mark# 2ndspos(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
(mark# plus(X1, X2) -> mark# X2, mark# square X -> a__square# mark X)
(mark# plus(X1, X2) -> mark# X2, mark# square X -> mark# X)
(mark# plus(X1, X2) -> mark# X2, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# plus(X1, X2) -> mark# X2, mark# times(X1, X2) -> mark# X2)
(mark# plus(X1, X2) -> mark# X2, mark# times(X1, X2) -> mark# X1)
(mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2)
(mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1)
(mark# plus(X1, X2) -> mark# X2, mark# pi X -> a__pi# mark X)
(mark# plus(X1, X2) -> mark# X2, mark# pi X -> mark# X)
(mark# plus(X1, X2) -> mark# X2, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# plus(X1, X2) -> mark# X2, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# plus(X1, X2) -> mark# X2, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# plus(X1, X2) -> mark# X2, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# plus(X1, X2) -> mark# X2, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# plus(X1, X2) -> mark# X2, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# plus(X1, X2) -> mark# X2, mark# negrecip X -> mark# X)
(mark# plus(X1, X2) -> mark# X2, mark# posrecip X -> mark# X)
(mark# plus(X1, X2) -> mark# X2, mark# rcons(X1, X2) -> mark# X2)
(mark# plus(X1, X2) -> mark# X2, mark# rcons(X1, X2) -> mark# X1)
(mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X)
(mark# plus(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
(mark# plus(X1, X2) -> mark# X2, mark# from X -> mark# X)
(mark# plus(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# square X -> a__square# mark X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# square X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# times(X1, X2) -> mark# X2)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# times(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# plus(X1, X2) -> mark# X2)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# plus(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# pi X -> a__pi# mark X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# pi X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# 2ndsneg(X1, X2) -> mark# X2)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# 2ndsneg(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# 2ndspos(X1, X2) -> mark# X2)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# 2ndspos(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# negrecip X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# posrecip X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# rcons(X1, X2) -> mark# X2)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# rcons(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# s X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# from X -> a__from# mark X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# from X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# cons(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# square X -> a__square# mark X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# square X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# times(X1, X2) -> mark# X2)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# times(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# plus(X1, X2) -> mark# X2)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# plus(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# pi X -> a__pi# mark X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# pi X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# 2ndsneg(X1, X2) -> mark# X2)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# 2ndsneg(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# 2ndspos(X1, X2) -> mark# X2)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# 2ndspos(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# negrecip X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# posrecip X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# rcons(X1, X2) -> mark# X2)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# rcons(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# s X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# from X -> a__from# mark X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# from X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# cons(X1, X2) -> mark# X1)
(a__plus#(0(), Y) -> mark# Y, mark# square X -> a__square# mark X)
(a__plus#(0(), Y) -> mark# Y, mark# square X -> mark# X)
(a__plus#(0(), Y) -> mark# Y, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(a__plus#(0(), Y) -> mark# Y, mark# times(X1, X2) -> mark# X2)
(a__plus#(0(), Y) -> mark# Y, mark# times(X1, X2) -> mark# X1)
(a__plus#(0(), Y) -> mark# Y, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(a__plus#(0(), Y) -> mark# Y, mark# plus(X1, X2) -> mark# X2)
(a__plus#(0(), Y) -> mark# Y, mark# plus(X1, X2) -> mark# X1)
(a__plus#(0(), Y) -> mark# Y, mark# pi X -> a__pi# mark X)
(a__plus#(0(), Y) -> mark# Y, mark# pi X -> mark# X)
(a__plus#(0(), Y) -> mark# Y, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(a__plus#(0(), Y) -> mark# Y, mark# 2ndsneg(X1, X2) -> mark# X2)
(a__plus#(0(), Y) -> mark# Y, mark# 2ndsneg(X1, X2) -> mark# X1)
(a__plus#(0(), Y) -> mark# Y, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(a__plus#(0(), Y) -> mark# Y, mark# 2ndspos(X1, X2) -> mark# X2)
(a__plus#(0(), Y) -> mark# Y, mark# 2ndspos(X1, X2) -> mark# X1)
(a__plus#(0(), Y) -> mark# Y, mark# negrecip X -> mark# X)
(a__plus#(0(), Y) -> mark# Y, mark# posrecip X -> mark# X)
(a__plus#(0(), Y) -> mark# Y, mark# rcons(X1, X2) -> mark# X2)
(a__plus#(0(), Y) -> mark# Y, mark# rcons(X1, X2) -> mark# X1)
(a__plus#(0(), Y) -> mark# Y, mark# s X -> mark# X)
(a__plus#(0(), Y) -> mark# Y, mark# from X -> a__from# mark X)
(a__plus#(0(), Y) -> mark# Y, mark# from X -> mark# X)
(a__plus#(0(), Y) -> mark# Y, mark# cons(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# square X -> a__square# mark X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# square X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# times(X1, X2) -> mark# X2)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# times(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# plus(X1, X2) -> mark# X2)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# plus(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# pi X -> a__pi# mark X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# pi X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# 2ndsneg(X1, X2) -> mark# X2)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# 2ndsneg(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# 2ndspos(X1, X2) -> mark# X2)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# 2ndspos(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# negrecip X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# posrecip X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# rcons(X1, X2) -> mark# X2)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# rcons(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# s X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# from X -> a__from# mark X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# from X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# cons(X1, X2) -> mark# X1)
(a__times#(s X, Y) -> a__plus#(mark Y, a__times(mark X, mark Y)), a__plus#(0(), Y) -> mark# Y)
(a__times#(s X, Y) -> a__plus#(mark Y, a__times(mark X, mark Y)), a__plus#(s X, Y) -> a__plus#(mark X, mark Y))
(a__times#(s X, Y) -> a__plus#(mark Y, a__times(mark X, mark Y)), a__plus#(s X, Y) -> mark# Y)
(a__times#(s X, Y) -> a__plus#(mark Y, a__times(mark X, mark Y)), a__plus#(s X, Y) -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# cons(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# from X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# from X -> a__from# mark X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# s X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# rcons(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# rcons(X1, X2) -> mark# X2)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# posrecip X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# negrecip X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# 2ndspos(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# 2ndspos(X1, X2) -> mark# X2)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# 2ndsneg(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# 2ndsneg(X1, X2) -> mark# X2)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# pi X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# pi X -> a__pi# mark X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# plus(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# plus(X1, X2) -> mark# X2)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# times(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# times(X1, X2) -> mark# X2)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# square X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N, mark# square X -> a__square# mark X)
(a__times#(s X, Y) -> mark# Y, mark# cons(X1, X2) -> mark# X1)
(a__times#(s X, Y) -> mark# Y, mark# from X -> mark# X)
(a__times#(s X, Y) -> mark# Y, mark# from X -> a__from# mark X)
(a__times#(s X, Y) -> mark# Y, mark# s X -> mark# X)
(a__times#(s X, Y) -> mark# Y, mark# rcons(X1, X2) -> mark# X1)
(a__times#(s X, Y) -> mark# Y, mark# rcons(X1, X2) -> mark# X2)
(a__times#(s X, Y) -> mark# Y, mark# posrecip X -> mark# X)
(a__times#(s X, Y) -> mark# Y, mark# negrecip X -> mark# X)
(a__times#(s X, Y) -> mark# Y, mark# 2ndspos(X1, X2) -> mark# X1)
(a__times#(s X, Y) -> mark# Y, mark# 2ndspos(X1, X2) -> mark# X2)
(a__times#(s X, Y) -> mark# Y, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(a__times#(s X, Y) -> mark# Y, mark# 2ndsneg(X1, X2) -> mark# X1)
(a__times#(s X, Y) -> mark# Y, mark# 2ndsneg(X1, X2) -> mark# X2)
(a__times#(s X, Y) -> mark# Y, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(a__times#(s X, Y) -> mark# Y, mark# pi X -> mark# X)
(a__times#(s X, Y) -> mark# Y, mark# pi X -> a__pi# mark X)
(a__times#(s X, Y) -> mark# Y, mark# plus(X1, X2) -> mark# X1)
(a__times#(s X, Y) -> mark# Y, mark# plus(X1, X2) -> mark# X2)
(a__times#(s X, Y) -> mark# Y, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(a__times#(s X, Y) -> mark# Y, mark# times(X1, X2) -> mark# X1)
(a__times#(s X, Y) -> mark# Y, mark# times(X1, X2) -> mark# X2)
(a__times#(s X, Y) -> mark# Y, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(a__times#(s X, Y) -> mark# Y, mark# square X -> mark# X)
(a__times#(s X, Y) -> mark# Y, mark# square X -> a__square# mark X)
(a__plus#(s X, Y) -> mark# Y, mark# cons(X1, X2) -> mark# X1)
(a__plus#(s X, Y) -> mark# Y, mark# from X -> mark# X)
(a__plus#(s X, Y) -> mark# Y, mark# from X -> a__from# mark X)
(a__plus#(s X, Y) -> mark# Y, mark# s X -> mark# X)
(a__plus#(s X, Y) -> mark# Y, mark# rcons(X1, X2) -> mark# X1)
(a__plus#(s X, Y) -> mark# Y, mark# rcons(X1, X2) -> mark# X2)
(a__plus#(s X, Y) -> mark# Y, mark# posrecip X -> mark# X)
(a__plus#(s X, Y) -> mark# Y, mark# negrecip X -> mark# X)
(a__plus#(s X, Y) -> mark# Y, mark# 2ndspos(X1, X2) -> mark# X1)
(a__plus#(s X, Y) -> mark# Y, mark# 2ndspos(X1, X2) -> mark# X2)
(a__plus#(s X, Y) -> mark# Y, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(a__plus#(s X, Y) -> mark# Y, mark# 2ndsneg(X1, X2) -> mark# X1)
(a__plus#(s X, Y) -> mark# Y, mark# 2ndsneg(X1, X2) -> mark# X2)
(a__plus#(s X, Y) -> mark# Y, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(a__plus#(s X, Y) -> mark# Y, mark# pi X -> mark# X)
(a__plus#(s X, Y) -> mark# Y, mark# pi X -> a__pi# mark X)
(a__plus#(s X, Y) -> mark# Y, mark# plus(X1, X2) -> mark# X1)
(a__plus#(s X, Y) -> mark# Y, mark# plus(X1, X2) -> mark# X2)
(a__plus#(s X, Y) -> mark# Y, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(a__plus#(s X, Y) -> mark# Y, mark# times(X1, X2) -> mark# X1)
(a__plus#(s X, Y) -> mark# Y, mark# times(X1, X2) -> mark# X2)
(a__plus#(s X, Y) -> mark# Y, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(a__plus#(s X, Y) -> mark# Y, mark# square X -> mark# X)
(a__plus#(s X, Y) -> mark# Y, mark# square X -> a__square# mark X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# cons(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# from X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# from X -> a__from# mark X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# s X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# rcons(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# rcons(X1, X2) -> mark# X2)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# posrecip X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# negrecip X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# 2ndspos(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# 2ndspos(X1, X2) -> mark# X2)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# 2ndsneg(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# 2ndsneg(X1, X2) -> mark# X2)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# pi X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# pi X -> a__pi# mark X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# plus(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# plus(X1, X2) -> mark# X2)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# times(X1, X2) -> mark# X1)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# times(X1, X2) -> mark# X2)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# square X -> mark# X)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y, mark# square X -> a__square# mark X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# cons(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# from X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# from X -> a__from# mark X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# s X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# rcons(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# rcons(X1, X2) -> mark# X2)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# posrecip X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# negrecip X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# 2ndspos(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# 2ndspos(X1, X2) -> mark# X2)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# 2ndsneg(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# 2ndsneg(X1, X2) -> mark# X2)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# pi X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# pi X -> a__pi# mark X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# plus(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# plus(X1, X2) -> mark# X2)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# times(X1, X2) -> mark# X1)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# times(X1, X2) -> mark# X2)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# square X -> mark# X)
(a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z, mark# square X -> a__square# mark X)
(mark# times(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
(mark# times(X1, X2) -> mark# X2, mark# from X -> mark# X)
(mark# times(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
(mark# times(X1, X2) -> mark# X2, mark# s X -> mark# X)
(mark# times(X1, X2) -> mark# X2, mark# rcons(X1, X2) -> mark# X1)
(mark# times(X1, X2) -> mark# X2, mark# rcons(X1, X2) -> mark# X2)
(mark# times(X1, X2) -> mark# X2, mark# posrecip X -> mark# X)
(mark# times(X1, X2) -> mark# X2, mark# negrecip X -> mark# X)
(mark# times(X1, X2) -> mark# X2, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# times(X1, X2) -> mark# X2, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# times(X1, X2) -> mark# X2, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# times(X1, X2) -> mark# X2, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# times(X1, X2) -> mark# X2, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# times(X1, X2) -> mark# X2, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# times(X1, X2) -> mark# X2, mark# pi X -> mark# X)
(mark# times(X1, X2) -> mark# X2, mark# pi X -> a__pi# mark X)
(mark# times(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1)
(mark# times(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2)
(mark# times(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# times(X1, X2) -> mark# X2, mark# times(X1, X2) -> mark# X1)
(mark# times(X1, X2) -> mark# X2, mark# times(X1, X2) -> mark# X2)
(mark# times(X1, X2) -> mark# X2, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# times(X1, X2) -> mark# X2, mark# square X -> mark# X)
(mark# times(X1, X2) -> mark# X2, mark# square X -> a__square# mark X)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# from X -> mark# X)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# s X -> mark# X)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# rcons(X1, X2) -> mark# X1)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# rcons(X1, X2) -> mark# X2)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# posrecip X -> mark# X)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# negrecip X -> mark# X)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# pi X -> mark# X)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# pi X -> a__pi# mark X)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# times(X1, X2) -> mark# X1)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# times(X1, X2) -> mark# X2)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# square X -> mark# X)
(mark# 2ndsneg(X1, X2) -> mark# X2, mark# square X -> a__square# mark X)
(mark# rcons(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
(mark# rcons(X1, X2) -> mark# X2, mark# from X -> mark# X)
(mark# rcons(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
(mark# rcons(X1, X2) -> mark# X2, mark# s X -> mark# X)
(mark# rcons(X1, X2) -> mark# X2, mark# rcons(X1, X2) -> mark# X1)
(mark# rcons(X1, X2) -> mark# X2, mark# rcons(X1, X2) -> mark# X2)
(mark# rcons(X1, X2) -> mark# X2, mark# posrecip X -> mark# X)
(mark# rcons(X1, X2) -> mark# X2, mark# negrecip X -> mark# X)
(mark# rcons(X1, X2) -> mark# X2, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# rcons(X1, X2) -> mark# X2, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# rcons(X1, X2) -> mark# X2, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# rcons(X1, X2) -> mark# X2, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# rcons(X1, X2) -> mark# X2, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# rcons(X1, X2) -> mark# X2, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# rcons(X1, X2) -> mark# X2, mark# pi X -> mark# X)
(mark# rcons(X1, X2) -> mark# X2, mark# pi X -> a__pi# mark X)
(mark# rcons(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1)
(mark# rcons(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2)
(mark# rcons(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# rcons(X1, X2) -> mark# X2, mark# times(X1, X2) -> mark# X1)
(mark# rcons(X1, X2) -> mark# X2, mark# times(X1, X2) -> mark# X2)
(mark# rcons(X1, X2) -> mark# X2, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# rcons(X1, X2) -> mark# X2, mark# square X -> mark# X)
(mark# rcons(X1, X2) -> mark# X2, mark# square X -> a__square# mark X)
(a__times#(s X, Y) -> mark# X, mark# cons(X1, X2) -> mark# X1)
(a__times#(s X, Y) -> mark# X, mark# from X -> mark# X)
(a__times#(s X, Y) -> mark# X, mark# from X -> a__from# mark X)
(a__times#(s X, Y) -> mark# X, mark# s X -> mark# X)
(a__times#(s X, Y) -> mark# X, mark# rcons(X1, X2) -> mark# X1)
(a__times#(s X, Y) -> mark# X, mark# rcons(X1, X2) -> mark# X2)
(a__times#(s X, Y) -> mark# X, mark# posrecip X -> mark# X)
(a__times#(s X, Y) -> mark# X, mark# negrecip X -> mark# X)
(a__times#(s X, Y) -> mark# X, mark# 2ndspos(X1, X2) -> mark# X1)
(a__times#(s X, Y) -> mark# X, mark# 2ndspos(X1, X2) -> mark# X2)
(a__times#(s X, Y) -> mark# X, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(a__times#(s X, Y) -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X1)
(a__times#(s X, Y) -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X2)
(a__times#(s X, Y) -> mark# X, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(a__times#(s X, Y) -> mark# X, mark# pi X -> mark# X)
(a__times#(s X, Y) -> mark# X, mark# pi X -> a__pi# mark X)
(a__times#(s X, Y) -> mark# X, mark# plus(X1, X2) -> mark# X1)
(a__times#(s X, Y) -> mark# X, mark# plus(X1, X2) -> mark# X2)
(a__times#(s X, Y) -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(a__times#(s X, Y) -> mark# X, mark# times(X1, X2) -> mark# X1)
(a__times#(s X, Y) -> mark# X, mark# times(X1, X2) -> mark# X2)
(a__times#(s X, Y) -> mark# X, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(a__times#(s X, Y) -> mark# X, mark# square X -> mark# X)
(a__times#(s X, Y) -> mark# X, mark# square X -> a__square# mark X)
(a__pi# X -> mark# X, mark# cons(X1, X2) -> mark# X1)
(a__pi# X -> mark# X, mark# from X -> mark# X)
(a__pi# X -> mark# X, mark# from X -> a__from# mark X)
(a__pi# X -> mark# X, mark# s X -> mark# X)
(a__pi# X -> mark# X, mark# rcons(X1, X2) -> mark# X1)
(a__pi# X -> mark# X, mark# rcons(X1, X2) -> mark# X2)
(a__pi# X -> mark# X, mark# posrecip X -> mark# X)
(a__pi# X -> mark# X, mark# negrecip X -> mark# X)
(a__pi# X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X1)
(a__pi# X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X2)
(a__pi# X -> mark# X, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(a__pi# X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X1)
(a__pi# X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X2)
(a__pi# X -> mark# X, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(a__pi# X -> mark# X, mark# pi X -> mark# X)
(a__pi# X -> mark# X, mark# pi X -> a__pi# mark X)
(a__pi# X -> mark# X, mark# plus(X1, X2) -> mark# X1)
(a__pi# X -> mark# X, mark# plus(X1, X2) -> mark# X2)
(a__pi# X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(a__pi# X -> mark# X, mark# times(X1, X2) -> mark# X1)
(a__pi# X -> mark# X, mark# times(X1, X2) -> mark# X2)
(a__pi# X -> mark# X, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(a__pi# X -> mark# X, mark# square X -> mark# X)
(a__pi# X -> mark# X, mark# square X -> a__square# mark X)
(mark# square X -> mark# X, mark# cons(X1, X2) -> mark# X1)
(mark# square X -> mark# X, mark# from X -> mark# X)
(mark# square X -> mark# X, mark# from X -> a__from# mark X)
(mark# square X -> mark# X, mark# s X -> mark# X)
(mark# square X -> mark# X, mark# rcons(X1, X2) -> mark# X1)
(mark# square X -> mark# X, mark# rcons(X1, X2) -> mark# X2)
(mark# square X -> mark# X, mark# posrecip X -> mark# X)
(mark# square X -> mark# X, mark# negrecip X -> mark# X)
(mark# square X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# square X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# square X -> mark# X, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# square X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# square X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# square X -> mark# X, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# square X -> mark# X, mark# pi X -> mark# X)
(mark# square X -> mark# X, mark# pi X -> a__pi# mark X)
(mark# square X -> mark# X, mark# plus(X1, X2) -> mark# X1)
(mark# square X -> mark# X, mark# plus(X1, X2) -> mark# X2)
(mark# square X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# square X -> mark# X, mark# times(X1, X2) -> mark# X1)
(mark# square X -> mark# X, mark# times(X1, X2) -> mark# X2)
(mark# square X -> mark# X, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# square X -> mark# X, mark# square X -> mark# X)
(mark# square X -> mark# X, mark# square X -> a__square# mark X)
(mark# negrecip X -> mark# X, mark# cons(X1, X2) -> mark# X1)
(mark# negrecip X -> mark# X, mark# from X -> mark# X)
(mark# negrecip X -> mark# X, mark# from X -> a__from# mark X)
(mark# negrecip X -> mark# X, mark# s X -> mark# X)
(mark# negrecip X -> mark# X, mark# rcons(X1, X2) -> mark# X1)
(mark# negrecip X -> mark# X, mark# rcons(X1, X2) -> mark# X2)
(mark# negrecip X -> mark# X, mark# posrecip X -> mark# X)
(mark# negrecip X -> mark# X, mark# negrecip X -> mark# X)
(mark# negrecip X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# negrecip X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# negrecip X -> mark# X, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# negrecip X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# negrecip X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# negrecip X -> mark# X, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# negrecip X -> mark# X, mark# pi X -> mark# X)
(mark# negrecip X -> mark# X, mark# pi X -> a__pi# mark X)
(mark# negrecip X -> mark# X, mark# plus(X1, X2) -> mark# X1)
(mark# negrecip X -> mark# X, mark# plus(X1, X2) -> mark# X2)
(mark# negrecip X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# negrecip X -> mark# X, mark# times(X1, X2) -> mark# X1)
(mark# negrecip X -> mark# X, mark# times(X1, X2) -> mark# X2)
(mark# negrecip X -> mark# X, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# negrecip X -> mark# X, mark# square X -> mark# X)
(mark# negrecip X -> mark# X, mark# square X -> a__square# mark X)
(mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
(mark# s X -> mark# X, mark# from X -> mark# X)
(mark# s X -> mark# X, mark# from X -> a__from# mark X)
(mark# s X -> mark# X, mark# s X -> mark# X)
(mark# s X -> mark# X, mark# rcons(X1, X2) -> mark# X1)
(mark# s X -> mark# X, mark# rcons(X1, X2) -> mark# X2)
(mark# s X -> mark# X, mark# posrecip X -> mark# X)
(mark# s X -> mark# X, mark# negrecip X -> mark# X)
(mark# s X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# s X -> mark# X, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# s X -> mark# X, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# s X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# s X -> mark# X, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# s X -> mark# X, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# s X -> mark# X, mark# pi X -> mark# X)
(mark# s X -> mark# X, mark# pi X -> a__pi# mark X)
(mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1)
(mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X2)
(mark# s X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# s X -> mark# X, mark# times(X1, X2) -> mark# X1)
(mark# s X -> mark# X, mark# times(X1, X2) -> mark# X2)
(mark# s X -> mark# X, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# s X -> mark# X, mark# square X -> mark# X)
(mark# s X -> mark# X, mark# square X -> a__square# mark X)
(mark# times(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
(mark# times(X1, X2) -> mark# X1, mark# from X -> mark# X)
(mark# times(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
(mark# times(X1, X2) -> mark# X1, mark# s X -> mark# X)
(mark# times(X1, X2) -> mark# X1, mark# rcons(X1, X2) -> mark# X1)
(mark# times(X1, X2) -> mark# X1, mark# rcons(X1, X2) -> mark# X2)
(mark# times(X1, X2) -> mark# X1, mark# posrecip X -> mark# X)
(mark# times(X1, X2) -> mark# X1, mark# negrecip X -> mark# X)
(mark# times(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# times(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# times(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# times(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# times(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# times(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# times(X1, X2) -> mark# X1, mark# pi X -> mark# X)
(mark# times(X1, X2) -> mark# X1, mark# pi X -> a__pi# mark X)
(mark# times(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
(mark# times(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
(mark# times(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# times(X1, X2) -> mark# X1, mark# times(X1, X2) -> mark# X1)
(mark# times(X1, X2) -> mark# X1, mark# times(X1, X2) -> mark# X2)
(mark# times(X1, X2) -> mark# X1, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# times(X1, X2) -> mark# X1, mark# square X -> mark# X)
(mark# times(X1, X2) -> mark# X1, mark# square X -> a__square# mark X)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# from X -> mark# X)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# s X -> mark# X)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# rcons(X1, X2) -> mark# X1)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# rcons(X1, X2) -> mark# X2)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# posrecip X -> mark# X)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# negrecip X -> mark# X)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# pi X -> mark# X)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# pi X -> a__pi# mark X)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# times(X1, X2) -> mark# X1)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# times(X1, X2) -> mark# X2)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# square X -> mark# X)
(mark# 2ndsneg(X1, X2) -> mark# X1, mark# square X -> a__square# mark X)
(mark# rcons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
(mark# rcons(X1, X2) -> mark# X1, mark# from X -> mark# X)
(mark# rcons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
(mark# rcons(X1, X2) -> mark# X1, mark# s X -> mark# X)
(mark# rcons(X1, X2) -> mark# X1, mark# rcons(X1, X2) -> mark# X1)
(mark# rcons(X1, X2) -> mark# X1, mark# rcons(X1, X2) -> mark# X2)
(mark# rcons(X1, X2) -> mark# X1, mark# posrecip X -> mark# X)
(mark# rcons(X1, X2) -> mark# X1, mark# negrecip X -> mark# X)
(mark# rcons(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> mark# X1)
(mark# rcons(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> mark# X2)
(mark# rcons(X1, X2) -> mark# X1, mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2))
(mark# rcons(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> mark# X1)
(mark# rcons(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> mark# X2)
(mark# rcons(X1, X2) -> mark# X1, mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2))
(mark# rcons(X1, X2) -> mark# X1, mark# pi X -> mark# X)
(mark# rcons(X1, X2) -> mark# X1, mark# pi X -> a__pi# mark X)
(mark# rcons(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
(mark# rcons(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
(mark# rcons(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
(mark# rcons(X1, X2) -> mark# X1, mark# times(X1, X2) -> mark# X1)
(mark# rcons(X1, X2) -> mark# X1, mark# times(X1, X2) -> mark# X2)
(mark# rcons(X1, X2) -> mark# X1, mark# times(X1, X2) -> a__times#(mark X1, mark X2))
(mark# rcons(X1, X2) -> mark# X1, mark# square X -> mark# X)
(mark# rcons(X1, X2) -> mark# X1, mark# square X -> a__square# mark X)
(a__square# X -> a__times#(mark X, mark X), a__times#(s X, Y) -> mark# X)
(a__square# X -> a__times#(mark X, mark X), a__times#(s X, Y) -> mark# Y)
(a__square# X -> a__times#(mark X, mark X), a__times#(s X, Y) -> a__plus#(mark Y, a__times(mark X, mark Y)))
(a__square# X -> a__times#(mark X, mark X), a__times#(s X, Y) -> a__times#(mark X, mark Y))
(a__plus#(s X, Y) -> a__plus#(mark X, mark Y), a__plus#(s X, Y) -> mark# X)
(a__plus#(s X, Y) -> a__plus#(mark X, mark Y), a__plus#(s X, Y) -> mark# Y)
(a__plus#(s X, Y) -> a__plus#(mark X, mark Y), a__plus#(s X, Y) -> a__plus#(mark X, mark Y))
(a__plus#(s X, Y) -> a__plus#(mark X, mark Y), a__plus#(0(), Y) -> mark# Y)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> a__2ndsneg#(mark N, mark Z), a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> a__2ndsneg#(mark N, mark Z), a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> a__2ndsneg#(mark N, mark Z), a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N)
(a__2ndspos#(s N, cons(X, cons(Y, Z))) -> a__2ndsneg#(mark N, mark Z), a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> a__2ndspos#(mark N, mark Z))
(mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(s X, Y) -> mark# X)
(mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(s X, Y) -> mark# Y)
(mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(s X, Y) -> a__plus#(mark X, mark Y))
(mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(0(), Y) -> mark# Y)
(mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2), a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z)
(mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2), a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y)
(mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2), a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N)
(mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2), a__2ndspos#(s N, cons(X, cons(Y, Z))) -> a__2ndsneg#(mark N, mark Z))
(mark# pi X -> a__pi# mark X, a__pi# X -> mark# X)
(mark# pi X -> a__pi# mark X, a__pi# X -> a__from# 0())
(mark# pi X -> a__pi# mark X, a__pi# X -> a__2ndspos#(mark X, a__from 0()))
(a__pi# X -> a__from# 0(), a__from# X -> mark# X)
}
STATUS:
arrows: 0.626181
SCCS (1):
Scc:
{ mark# cons(X1, X2) -> mark# X1,
mark# from X -> mark# X,
mark# from X -> a__from# mark X,
mark# s X -> mark# X,
mark# rcons(X1, X2) -> mark# X1,
mark# rcons(X1, X2) -> mark# X2,
mark# posrecip X -> mark# X,
mark# negrecip X -> mark# X,
mark# 2ndspos(X1, X2) -> mark# X1,
mark# 2ndspos(X1, X2) -> mark# X2,
mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2),
mark# 2ndsneg(X1, X2) -> mark# X1,
mark# 2ndsneg(X1, X2) -> mark# X2,
mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2),
mark# pi X -> mark# X,
mark# pi X -> a__pi# mark X,
mark# plus(X1, X2) -> mark# X1,
mark# plus(X1, X2) -> mark# X2,
mark# plus(X1, X2) -> a__plus#(mark X1, mark X2),
mark# times(X1, X2) -> mark# X1,
mark# times(X1, X2) -> mark# X2,
mark# times(X1, X2) -> a__times#(mark X1, mark X2),
mark# square X -> mark# X,
mark# square X -> a__square# mark X,
a__from# X -> mark# X,
a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z,
a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y,
a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N,
a__2ndspos#(s N, cons(X, cons(Y, Z))) -> a__2ndsneg#(mark N, mark Z),
a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z,
a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y,
a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N,
a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> a__2ndspos#(mark N, mark Z),
a__pi# X -> mark# X,
a__pi# X -> a__from# 0(),
a__plus#(s X, Y) -> mark# X,
a__plus#(s X, Y) -> mark# Y,
a__plus#(s X, Y) -> a__plus#(mark X, mark Y),
a__plus#(0(), Y) -> mark# Y,
a__times#(s X, Y) -> mark# X,
a__times#(s X, Y) -> mark# Y,
a__times#(s X, Y) -> a__plus#(mark Y, a__times(mark X, mark Y)),
a__times#(s X, Y) -> a__times#(mark X, mark Y),
a__square# X -> mark# X,
a__square# X -> a__times#(mark X, mark X)}
SCC (45):
Strict:
{ mark# cons(X1, X2) -> mark# X1,
mark# from X -> mark# X,
mark# from X -> a__from# mark X,
mark# s X -> mark# X,
mark# rcons(X1, X2) -> mark# X1,
mark# rcons(X1, X2) -> mark# X2,
mark# posrecip X -> mark# X,
mark# negrecip X -> mark# X,
mark# 2ndspos(X1, X2) -> mark# X1,
mark# 2ndspos(X1, X2) -> mark# X2,
mark# 2ndspos(X1, X2) -> a__2ndspos#(mark X1, mark X2),
mark# 2ndsneg(X1, X2) -> mark# X1,
mark# 2ndsneg(X1, X2) -> mark# X2,
mark# 2ndsneg(X1, X2) -> a__2ndsneg#(mark X1, mark X2),
mark# pi X -> mark# X,
mark# pi X -> a__pi# mark X,
mark# plus(X1, X2) -> mark# X1,
mark# plus(X1, X2) -> mark# X2,
mark# plus(X1, X2) -> a__plus#(mark X1, mark X2),
mark# times(X1, X2) -> mark# X1,
mark# times(X1, X2) -> mark# X2,
mark# times(X1, X2) -> a__times#(mark X1, mark X2),
mark# square X -> mark# X,
mark# square X -> a__square# mark X,
a__from# X -> mark# X,
a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z,
a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y,
a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N,
a__2ndspos#(s N, cons(X, cons(Y, Z))) -> a__2ndsneg#(mark N, mark Z),
a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Z,
a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# Y,
a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> mark# N,
a__2ndsneg#(s N, cons(X, cons(Y, Z))) -> a__2ndspos#(mark N, mark Z),
a__pi# X -> mark# X,
a__pi# X -> a__from# 0(),
a__plus#(s X, Y) -> mark# X,
a__plus#(s X, Y) -> mark# Y,
a__plus#(s X, Y) -> a__plus#(mark X, mark Y),
a__plus#(0(), Y) -> mark# Y,
a__times#(s X, Y) -> mark# X,
a__times#(s X, Y) -> mark# Y,
a__times#(s X, Y) -> a__plus#(mark Y, a__times(mark X, mark Y)),
a__times#(s X, Y) -> a__times#(mark X, mark Y),
a__square# X -> mark# X,
a__square# X -> a__times#(mark X, mark X)}
Weak:
{ mark cons(X1, X2) -> cons(mark X1, X2),
mark from X -> a__from mark X,
mark s X -> s mark X,
mark rnil() -> rnil(),
mark 0() -> 0(),
mark rcons(X1, X2) -> rcons(mark X1, mark X2),
mark posrecip X -> posrecip mark X,
mark negrecip X -> negrecip mark X,
mark 2ndspos(X1, X2) -> a__2ndspos(mark X1, mark X2),
mark 2ndsneg(X1, X2) -> a__2ndsneg(mark X1, mark X2),
mark pi X -> a__pi mark X,
mark plus(X1, X2) -> a__plus(mark X1, mark X2),
mark times(X1, X2) -> a__times(mark X1, mark X2),
mark square X -> a__square mark X,
mark nil() -> nil(),
a__from X -> cons(mark X, from s X),
a__from X -> from X,
a__2ndspos(X1, X2) -> 2ndspos(X1, X2),
a__2ndspos(s N, cons(X, cons(Y, Z))) -> rcons(posrecip mark Y, a__2ndsneg(mark N, mark Z)),
a__2ndspos(0(), Z) -> rnil(),
a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2),
a__2ndsneg(s N, cons(X, cons(Y, Z))) -> rcons(negrecip mark Y, a__2ndspos(mark N, mark Z)),
a__2ndsneg(0(), Z) -> rnil(),
a__pi X -> a__2ndspos(mark X, a__from 0()),
a__pi X -> pi X,
a__plus(X1, X2) -> plus(X1, X2),
a__plus(s X, Y) -> s a__plus(mark X, mark Y),
a__plus(0(), Y) -> mark Y,
a__times(X1, X2) -> times(X1, X2),
a__times(s X, Y) -> a__plus(mark Y, a__times(mark X, mark Y)),
a__times(0(), Y) -> 0(),
a__square X -> a__times(mark X, mark X),
a__square X -> square X}
Open