MAYBE Time: 36.304328 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__pi# X -> a__2ndspos#(mark X, a__from 0()), a__2ndspos#(s N, cons(X, cons(Y, Z))) -> a__2ndsneg#(mark N, mark Z)) (a__pi# X -> a__2ndspos#(mark X, a__from 0()), a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# N) (a__pi# X -> a__2ndspos#(mark X, a__from 0()), a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Y) (a__pi# X -> a__2ndspos#(mark X, a__from 0()), a__2ndspos#(s N, cons(X, cons(Y, Z))) -> mark# Z) (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.624291 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__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)} SCC (46): 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__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)} 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