We consider the system h16.

  Alphabet:

    0 : [] --> R 
    1 : [] --> R 
    cos : [] --> R -> R 
    d : [] --> (R -> R) -> R -> R 
    minus : [] --> R -> R 
    mul : [] --> R -> R -> R 
    pls : [] --> R -> R -> R 
    sin : [] --> R -> R 

  Rules:

    d (/\x.y) z => 0 
    d (/\x.x) y => 1 
    d (/\x.minus (f x)) y => minus (d (/\z.f z) y) 
    d (/\x.pls (f x) (g x)) y => pls (d (/\z.f z) y) (d (/\u.g u) y) 
    d (/\x.mul (f x) (g x)) y => pls (mul (d (/\z.f z) y) (g y)) (mul (f y) (d (/\u.g u) y)) 
    d (/\x.sin (f x)) y => mul (cos y) (d (/\z.f z) y) 
    d (/\x.cos (f x)) y => mul (minus (sin y)) (d (/\z.f z) y) 
    minus 0 => 0 
    mul 0 x => 0 
    mul x 0 => 0 
    pls 0 x => x 

Using the transformations described in [Kop11], this system can be brought in a form without leading free variables in the left-hand side, and where the left-hand side of a variable is always a functional term or application headed by a functional term.

We now transform the resulting AFS into an AFSM by replacing all free variables by meta-variables (with arity 0).  This leads to the following AFSM:

  Alphabet:

    0 : [] --> R 
    1 : [] --> R 
    cos : [R] --> R 
    d : [R -> R * R] --> R 
    minus : [R] --> R 
    mul : [R * R] --> R 
    pls : [R * R] --> R 
    sin : [R] --> R 
    ~AP1 : [R -> R * R] --> R 

  Rules:

    d(/\x.X, Y) => 0 
    d(/\x.x, X) => 1 
    d(/\x.minus(~AP1(F, x)), X) => minus(d(/\y.~AP1(F, y), X)) 
    d(/\x.pls(~AP1(F, x), ~AP1(G, x)), X) => pls(d(/\y.~AP1(F, y), X), d(/\z.~AP1(G, z), X)) 
    d(/\x.mul(~AP1(F, x), ~AP1(G, x)), X) => pls(mul(d(/\y.~AP1(F, y), X), ~AP1(G, X)), mul(~AP1(F, X), d(/\z.~AP1(G, z), X))) 
    d(/\x.sin(~AP1(F, x)), X) => mul(cos(X), d(/\y.~AP1(F, y), X)) 
    d(/\x.cos(~AP1(F, x)), X) => mul(minus(sin(X)), d(/\y.~AP1(F, y), X)) 
    minus(0) => 0 
    mul(0, X) => 0 
    mul(X, 0) => 0 
    pls(0, X) => X 
    d(/\x.minus(cos(x)), X) => minus(d(/\y.cos(y), X)) 
    d(/\x.minus(d(F, x)), X) => minus(d(/\y.d(F, y), X)) 
    d(/\x.minus(minus(x)), X) => minus(d(/\y.minus(y), X)) 
    d(/\x.minus(mul(X, x)), Y) => minus(d(/\y.mul(X, y), Y)) 
    d(/\x.minus(pls(X, x)), Y) => minus(d(/\y.pls(X, y), Y)) 
    d(/\x.minus(sin(x)), X) => minus(d(/\y.sin(y), X)) 
    d(/\x.pls(cos(x), ~AP1(F, x)), X) => pls(d(/\y.cos(y), X), d(/\z.~AP1(F, z), X)) 
    d(/\x.pls(d(F, x), ~AP1(G, x)), X) => pls(d(/\y.d(F, y), X), d(/\z.~AP1(G, z), X)) 
    d(/\x.pls(minus(x), ~AP1(F, x)), X) => pls(d(/\y.minus(y), X), d(/\z.~AP1(F, z), X)) 
    d(/\x.pls(mul(X, x), ~AP1(F, x)), Y) => pls(d(/\y.mul(X, y), Y), d(/\z.~AP1(F, z), Y)) 
    d(/\x.pls(pls(X, x), ~AP1(F, x)), Y) => pls(d(/\y.pls(X, y), Y), d(/\z.~AP1(F, z), Y)) 
    d(/\x.pls(sin(x), ~AP1(F, x)), X) => pls(d(/\y.sin(y), X), d(/\z.~AP1(F, z), X)) 
    d(/\x.pls(~AP1(F, x), cos(x)), X) => pls(d(/\y.~AP1(F, y), X), d(/\z.cos(z), X)) 
    d(/\x.pls(~AP1(F, x), d(G, x)), X) => pls(d(/\y.~AP1(F, y), X), d(/\z.d(G, z), X)) 
    d(/\x.pls(~AP1(F, x), minus(x)), X) => pls(d(/\y.~AP1(F, y), X), d(/\z.minus(z), X)) 
    d(/\x.pls(~AP1(F, x), mul(X, x)), Y) => pls(d(/\y.~AP1(F, y), Y), d(/\z.mul(X, z), Y)) 
    d(/\x.pls(~AP1(F, x), pls(X, x)), Y) => pls(d(/\y.~AP1(F, y), Y), d(/\z.pls(X, z), Y)) 
    d(/\x.pls(~AP1(F, x), sin(x)), X) => pls(d(/\y.~AP1(F, y), X), d(/\z.sin(z), X)) 
    d(/\x.mul(cos(x), ~AP1(F, x)), X) => pls(mul(d(/\y.cos(y), X), ~AP1(F, X)), mul(cos(X), d(/\z.~AP1(F, z), X))) 
    d(/\x.mul(d(F, x), ~AP1(G, x)), X) => pls(mul(d(/\y.d(F, y), X), ~AP1(G, X)), mul(d(F, X), d(/\z.~AP1(G, z), X))) 
    d(/\x.mul(minus(x), ~AP1(F, x)), X) => pls(mul(d(/\y.minus(y), X), ~AP1(F, X)), mul(minus(X), d(/\z.~AP1(F, z), X))) 
    d(/\x.mul(mul(X, x), ~AP1(F, x)), Y) => pls(mul(d(/\y.mul(X, y), Y), ~AP1(F, Y)), mul(mul(X, Y), d(/\z.~AP1(F, z), Y))) 
    d(/\x.mul(pls(X, x), ~AP1(F, x)), Y) => pls(mul(d(/\y.pls(X, y), Y), ~AP1(F, Y)), mul(pls(X, Y), d(/\z.~AP1(F, z), Y))) 
    d(/\x.mul(sin(x), ~AP1(F, x)), X) => pls(mul(d(/\y.sin(y), X), ~AP1(F, X)), mul(sin(X), d(/\z.~AP1(F, z), X))) 
    d(/\x.mul(~AP1(F, x), cos(x)), X) => pls(mul(d(/\y.~AP1(F, y), X), cos(X)), mul(~AP1(F, X), d(/\z.cos(z), X))) 
    d(/\x.mul(~AP1(F, x), d(G, x)), X) => pls(mul(d(/\y.~AP1(F, y), X), d(G, X)), mul(~AP1(F, X), d(/\z.d(G, z), X))) 
    d(/\x.mul(~AP1(F, x), minus(x)), X) => pls(mul(d(/\y.~AP1(F, y), X), minus(X)), mul(~AP1(F, X), d(/\z.minus(z), X))) 
    d(/\x.mul(~AP1(F, x), mul(X, x)), Y) => pls(mul(d(/\y.~AP1(F, y), Y), mul(X, Y)), mul(~AP1(F, Y), d(/\z.mul(X, z), Y))) 
    d(/\x.mul(~AP1(F, x), pls(X, x)), Y) => pls(mul(d(/\y.~AP1(F, y), Y), pls(X, Y)), mul(~AP1(F, Y), d(/\z.pls(X, z), Y))) 
    d(/\x.mul(~AP1(F, x), sin(x)), X) => pls(mul(d(/\y.~AP1(F, y), X), sin(X)), mul(~AP1(F, X), d(/\z.sin(z), X))) 
    d(/\x.sin(cos(x)), X) => mul(cos(X), d(/\y.cos(y), X)) 
    d(/\x.sin(d(F, x)), X) => mul(cos(X), d(/\y.d(F, y), X)) 
    d(/\x.sin(minus(x)), X) => mul(cos(X), d(/\y.minus(y), X)) 
    d(/\x.sin(mul(X, x)), Y) => mul(cos(Y), d(/\y.mul(X, y), Y)) 
    d(/\x.sin(pls(X, x)), Y) => mul(cos(Y), d(/\y.pls(X, y), Y)) 
    d(/\x.sin(sin(x)), X) => mul(cos(X), d(/\y.sin(y), X)) 
    d(/\x.cos(cos(x)), X) => mul(minus(sin(X)), d(/\y.cos(y), X)) 
    d(/\x.cos(d(F, x)), X) => mul(minus(sin(X)), d(/\y.d(F, y), X)) 
    d(/\x.cos(minus(x)), X) => mul(minus(sin(X)), d(/\y.minus(y), X)) 
    d(/\x.cos(mul(X, x)), Y) => mul(minus(sin(Y)), d(/\y.mul(X, y), Y)) 
    d(/\x.cos(pls(X, x)), Y) => mul(minus(sin(Y)), d(/\y.pls(X, y), Y)) 
    d(/\x.cos(sin(x)), X) => mul(minus(sin(X)), d(/\y.sin(y), X)) 
    d(/\x.pls(cos(x), cos(x)), X) => pls(d(/\y.cos(y), X), d(/\z.cos(z), X)) 
    d(/\x.pls(cos(x), d(F, x)), X) => pls(d(/\y.cos(y), X), d(/\z.d(F, z), X)) 
    d(/\x.pls(cos(x), minus(x)), X) => pls(d(/\y.cos(y), X), d(/\z.minus(z), X)) 
    d(/\x.pls(cos(x), mul(X, x)), Y) => pls(d(/\y.cos(y), Y), d(/\z.mul(X, z), Y)) 
    d(/\x.pls(cos(x), pls(X, x)), Y) => pls(d(/\y.cos(y), Y), d(/\z.pls(X, z), Y)) 
    d(/\x.pls(cos(x), sin(x)), X) => pls(d(/\y.cos(y), X), d(/\z.sin(z), X)) 
    d(/\x.pls(d(F, x), cos(x)), X) => pls(d(/\y.d(F, y), X), d(/\z.cos(z), X)) 
    d(/\x.pls(d(F, x), d(G, x)), X) => pls(d(/\y.d(F, y), X), d(/\z.d(G, z), X)) 
    d(/\x.pls(d(F, x), minus(x)), X) => pls(d(/\y.d(F, y), X), d(/\z.minus(z), X)) 
    d(/\x.pls(d(F, x), mul(X, x)), Y) => pls(d(/\y.d(F, y), Y), d(/\z.mul(X, z), Y)) 
    d(/\x.pls(d(F, x), pls(X, x)), Y) => pls(d(/\y.d(F, y), Y), d(/\z.pls(X, z), Y)) 
    d(/\x.pls(d(F, x), sin(x)), X) => pls(d(/\y.d(F, y), X), d(/\z.sin(z), X)) 
    d(/\x.pls(minus(x), cos(x)), X) => pls(d(/\y.minus(y), X), d(/\z.cos(z), X)) 
    d(/\x.pls(minus(x), d(F, x)), X) => pls(d(/\y.minus(y), X), d(/\z.d(F, z), X)) 
    d(/\x.pls(minus(x), minus(x)), X) => pls(d(/\y.minus(y), X), d(/\z.minus(z), X)) 
    d(/\x.pls(minus(x), mul(X, x)), Y) => pls(d(/\y.minus(y), Y), d(/\z.mul(X, z), Y)) 
    d(/\x.pls(minus(x), pls(X, x)), Y) => pls(d(/\y.minus(y), Y), d(/\z.pls(X, z), Y)) 
    d(/\x.pls(minus(x), sin(x)), X) => pls(d(/\y.minus(y), X), d(/\z.sin(z), X)) 
    d(/\x.pls(mul(X, x), cos(x)), Y) => pls(d(/\y.mul(X, y), Y), d(/\z.cos(z), Y)) 
    d(/\x.pls(mul(X, x), d(F, x)), Y) => pls(d(/\y.mul(X, y), Y), d(/\z.d(F, z), Y)) 
    d(/\x.pls(mul(X, x), minus(x)), Y) => pls(d(/\y.mul(X, y), Y), d(/\z.minus(z), Y)) 
    d(/\x.pls(mul(X, x), mul(Y, x)), Z) => pls(d(/\y.mul(X, y), Z), d(/\z.mul(Y, z), Z)) 
    d(/\x.pls(mul(X, x), pls(Y, x)), Z) => pls(d(/\y.mul(X, y), Z), d(/\z.pls(Y, z), Z)) 
    d(/\x.pls(mul(X, x), sin(x)), Y) => pls(d(/\y.mul(X, y), Y), d(/\z.sin(z), Y)) 
    d(/\x.pls(pls(X, x), cos(x)), Y) => pls(d(/\y.pls(X, y), Y), d(/\z.cos(z), Y)) 
    d(/\x.pls(pls(X, x), d(F, x)), Y) => pls(d(/\y.pls(X, y), Y), d(/\z.d(F, z), Y)) 
    d(/\x.pls(pls(X, x), minus(x)), Y) => pls(d(/\y.pls(X, y), Y), d(/\z.minus(z), Y)) 
    d(/\x.pls(pls(X, x), mul(Y, x)), Z) => pls(d(/\y.pls(X, y), Z), d(/\z.mul(Y, z), Z)) 
    d(/\x.pls(pls(X, x), pls(Y, x)), Z) => pls(d(/\y.pls(X, y), Z), d(/\z.pls(Y, z), Z)) 
    d(/\x.pls(pls(X, x), sin(x)), Y) => pls(d(/\y.pls(X, y), Y), d(/\z.sin(z), Y)) 
    d(/\x.pls(sin(x), cos(x)), X) => pls(d(/\y.sin(y), X), d(/\z.cos(z), X)) 
    d(/\x.pls(sin(x), d(F, x)), X) => pls(d(/\y.sin(y), X), d(/\z.d(F, z), X)) 
    d(/\x.pls(sin(x), minus(x)), X) => pls(d(/\y.sin(y), X), d(/\z.minus(z), X)) 
    d(/\x.pls(sin(x), mul(X, x)), Y) => pls(d(/\y.sin(y), Y), d(/\z.mul(X, z), Y)) 
    d(/\x.pls(sin(x), pls(X, x)), Y) => pls(d(/\y.sin(y), Y), d(/\z.pls(X, z), Y)) 
    d(/\x.pls(sin(x), sin(x)), X) => pls(d(/\y.sin(y), X), d(/\z.sin(z), X)) 
    d(/\x.mul(cos(x), cos(x)), X) => pls(mul(d(/\y.cos(y), X), cos(X)), mul(cos(X), d(/\z.cos(z), X))) 
    d(/\x.mul(cos(x), d(F, x)), X) => pls(mul(d(/\y.cos(y), X), d(F, X)), mul(cos(X), d(/\z.d(F, z), X))) 
    d(/\x.mul(cos(x), minus(x)), X) => pls(mul(d(/\y.cos(y), X), minus(X)), mul(cos(X), d(/\z.minus(z), X))) 
    d(/\x.mul(cos(x), mul(X, x)), Y) => pls(mul(d(/\y.cos(y), Y), mul(X, Y)), mul(cos(Y), d(/\z.mul(X, z), Y))) 
    d(/\x.mul(cos(x), pls(X, x)), Y) => pls(mul(d(/\y.cos(y), Y), pls(X, Y)), mul(cos(Y), d(/\z.pls(X, z), Y))) 
    d(/\x.mul(cos(x), sin(x)), X) => pls(mul(d(/\y.cos(y), X), sin(X)), mul(cos(X), d(/\z.sin(z), X))) 
    d(/\x.mul(d(F, x), cos(x)), X) => pls(mul(d(/\y.d(F, y), X), cos(X)), mul(d(F, X), d(/\z.cos(z), X))) 
    d(/\x.mul(d(F, x), d(G, x)), X) => pls(mul(d(/\y.d(F, y), X), d(G, X)), mul(d(F, X), d(/\z.d(G, z), X))) 
    d(/\x.mul(d(F, x), minus(x)), X) => pls(mul(d(/\y.d(F, y), X), minus(X)), mul(d(F, X), d(/\z.minus(z), X))) 
    d(/\x.mul(d(F, x), mul(X, x)), Y) => pls(mul(d(/\y.d(F, y), Y), mul(X, Y)), mul(d(F, Y), d(/\z.mul(X, z), Y))) 
    d(/\x.mul(d(F, x), pls(X, x)), Y) => pls(mul(d(/\y.d(F, y), Y), pls(X, Y)), mul(d(F, Y), d(/\z.pls(X, z), Y))) 
    d(/\x.mul(d(F, x), sin(x)), X) => pls(mul(d(/\y.d(F, y), X), sin(X)), mul(d(F, X), d(/\z.sin(z), X))) 
    d(/\x.mul(minus(x), cos(x)), X) => pls(mul(d(/\y.minus(y), X), cos(X)), mul(minus(X), d(/\z.cos(z), X))) 
    d(/\x.mul(minus(x), d(F, x)), X) => pls(mul(d(/\y.minus(y), X), d(F, X)), mul(minus(X), d(/\z.d(F, z), X))) 
    d(/\x.mul(minus(x), minus(x)), X) => pls(mul(d(/\y.minus(y), X), minus(X)), mul(minus(X), d(/\z.minus(z), X))) 
    d(/\x.mul(minus(x), mul(X, x)), Y) => pls(mul(d(/\y.minus(y), Y), mul(X, Y)), mul(minus(Y), d(/\z.mul(X, z), Y))) 
    d(/\x.mul(minus(x), pls(X, x)), Y) => pls(mul(d(/\y.minus(y), Y), pls(X, Y)), mul(minus(Y), d(/\z.pls(X, z), Y))) 
    d(/\x.mul(minus(x), sin(x)), X) => pls(mul(d(/\y.minus(y), X), sin(X)), mul(minus(X), d(/\z.sin(z), X))) 
    d(/\x.mul(mul(X, x), cos(x)), Y) => pls(mul(d(/\y.mul(X, y), Y), cos(Y)), mul(mul(X, Y), d(/\z.cos(z), Y))) 
    d(/\x.mul(mul(X, x), d(F, x)), Y) => pls(mul(d(/\y.mul(X, y), Y), d(F, Y)), mul(mul(X, Y), d(/\z.d(F, z), Y))) 
    d(/\x.mul(mul(X, x), minus(x)), Y) => pls(mul(d(/\y.mul(X, y), Y), minus(Y)), mul(mul(X, Y), d(/\z.minus(z), Y))) 
    d(/\x.mul(mul(X, x), mul(Y, x)), Z) => pls(mul(d(/\y.mul(X, y), Z), mul(Y, Z)), mul(mul(X, Z), d(/\z.mul(Y, z), Z))) 
    d(/\x.mul(mul(X, x), pls(Y, x)), Z) => pls(mul(d(/\y.mul(X, y), Z), pls(Y, Z)), mul(mul(X, Z), d(/\z.pls(Y, z), Z))) 
    d(/\x.mul(mul(X, x), sin(x)), Y) => pls(mul(d(/\y.mul(X, y), Y), sin(Y)), mul(mul(X, Y), d(/\z.sin(z), Y))) 
    d(/\x.mul(pls(X, x), cos(x)), Y) => pls(mul(d(/\y.pls(X, y), Y), cos(Y)), mul(pls(X, Y), d(/\z.cos(z), Y))) 
    d(/\x.mul(pls(X, x), d(F, x)), Y) => pls(mul(d(/\y.pls(X, y), Y), d(F, Y)), mul(pls(X, Y), d(/\z.d(F, z), Y))) 
    d(/\x.mul(pls(X, x), minus(x)), Y) => pls(mul(d(/\y.pls(X, y), Y), minus(Y)), mul(pls(X, Y), d(/\z.minus(z), Y))) 
    d(/\x.mul(pls(X, x), mul(Y, x)), Z) => pls(mul(d(/\y.pls(X, y), Z), mul(Y, Z)), mul(pls(X, Z), d(/\z.mul(Y, z), Z))) 
    d(/\x.mul(pls(X, x), pls(Y, x)), Z) => pls(mul(d(/\y.pls(X, y), Z), pls(Y, Z)), mul(pls(X, Z), d(/\z.pls(Y, z), Z))) 
    d(/\x.mul(pls(X, x), sin(x)), Y) => pls(mul(d(/\y.pls(X, y), Y), sin(Y)), mul(pls(X, Y), d(/\z.sin(z), Y))) 
    d(/\x.mul(sin(x), cos(x)), X) => pls(mul(d(/\y.sin(y), X), cos(X)), mul(sin(X), d(/\z.cos(z), X))) 
    d(/\x.mul(sin(x), d(F, x)), X) => pls(mul(d(/\y.sin(y), X), d(F, X)), mul(sin(X), d(/\z.d(F, z), X))) 
    d(/\x.mul(sin(x), minus(x)), X) => pls(mul(d(/\y.sin(y), X), minus(X)), mul(sin(X), d(/\z.minus(z), X))) 
    d(/\x.mul(sin(x), mul(X, x)), Y) => pls(mul(d(/\y.sin(y), Y), mul(X, Y)), mul(sin(Y), d(/\z.mul(X, z), Y))) 
    d(/\x.mul(sin(x), pls(X, x)), Y) => pls(mul(d(/\y.sin(y), Y), pls(X, Y)), mul(sin(Y), d(/\z.pls(X, z), Y))) 
    d(/\x.mul(sin(x), sin(x)), X) => pls(mul(d(/\y.sin(y), X), sin(X)), mul(sin(X), d(/\z.sin(z), X))) 
    ~AP1(F, X) => F X 

Symbol ~AP1 is an encoding for application that is only used in innocuous ways.  We can simplify the program (without losing non-termination) by removing it.  Additionally, we can remove some (now-)redundant rules.  This gives:

  Alphabet:

    0 : [] --> R 
    1 : [] --> R 
    cos : [R] --> R 
    d : [R -> R * R] --> R 
    minus : [R] --> R 
    mul : [R * R] --> R 
    pls : [R * R] --> R 
    sin : [R] --> R 

  Rules:

    d(/\x.X, Y) => 0 
    d(/\x.x, X) => 1 
    d(/\x.minus(X(x)), Y) => minus(d(/\y.X(y), Y)) 
    d(/\x.pls(X(x), Y(x)), Z) => pls(d(/\y.X(y), Z), d(/\z.Y(z), Z)) 
    d(/\x.mul(X(x), Y(x)), Z) => pls(mul(d(/\y.X(y), Z), Y(Z)), mul(X(Z), d(/\z.Y(z), Z))) 
    d(/\x.sin(X(x)), Y) => mul(cos(Y), d(/\y.X(y), Y)) 
    d(/\x.cos(X(x)), Y) => mul(minus(sin(Y)), d(/\y.X(y), Y)) 
    minus(0) => 0 
    mul(0, X) => 0 
    mul(X, 0) => 0 
    pls(0, X) => X 

We observe that the rules contain a first-order subset:

  minus(0) => 0 
  mul(0, X) => 0 
  mul(X, 0) => 0 
  pls(0, X) => X 

Moreover, the system is finitely branching.  Thus, by [Kop12, Thm. 7.55], we may omit all first-order dependency pairs from the dependency pair problem (DP(R), R) if this first-order part is Ce-terminating when seen as a many-sorted first-order TRS.

According to the external first-order termination prover, this system is indeed Ce-terminating:

 || proof of resources/system.trs
 || # AProVE Commit ID: d84c10301d352dfd14de2104819581f4682260f5 fuhs 20130616
 || 
 || 
 || Termination w.r.t. Q of the given QTRS could be proven:
 || 
 || (0) QTRS
 || (1) QTRSRRRProof [EQUIVALENT]
 || (2) QTRS
 || (3) RisEmptyProof [EQUIVALENT]
 || (4) YES
 || 
 || 
 || ----------------------------------------
 || 
 || (0)
 || Obligation:
 || Q restricted rewrite system:
 || The TRS R consists of the following rules:
 || 
 ||    minus(0) -> 0
 ||    mul(0, %X) -> 0
 ||    mul(%X, 0) -> 0
 ||    pls(0, %X) -> %X
 ||    ~PAIR(%X, %Y) -> %X
 ||    ~PAIR(%X, %Y) -> %Y
 || 
 || Q is empty.
 || 
 || ----------------------------------------
 || 
 || (1) QTRSRRRProof (EQUIVALENT)
 || Used ordering:
 || Polynomial interpretation [POLO]:
 || 
 ||    POL(0) = 1
 ||    POL(minus(x_1)) = 2 + 2*x_1
 ||    POL(mul(x_1, x_2)) = 2 + 2*x_1 + 2*x_2
 ||    POL(pls(x_1, x_2)) = 2 + x_1 + x_2
 ||    POL(~PAIR(x_1, x_2)) = 2 + x_1 + x_2
 || With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
 || 
 ||    minus(0) -> 0
 ||    mul(0, %X) -> 0
 ||    mul(%X, 0) -> 0
 ||    pls(0, %X) -> %X
 ||    ~PAIR(%X, %Y) -> %X
 ||    ~PAIR(%X, %Y) -> %Y
 || 
 || 
 || 
 || 
 || ----------------------------------------
 || 
 || (2)
 || Obligation:
 || Q restricted rewrite system:
 || R is empty.
 || Q is empty.
 || 
 || ----------------------------------------
 || 
 || (3) RisEmptyProof (EQUIVALENT)
 || The TRS R is empty. Hence, termination is trivially proven.
 || ----------------------------------------
 || 
 || (4)
 || YES
 || 
We use the dependency pair framework as described in [Kop12, Ch. 6/7], with dynamic dependency pairs.

We thus obtain the following dependency pair problem (P_0, R_0, minimal, all):

  Dependency Pairs P_0:

    0] d#(/\x.minus(X(x)), Y) =#> minus#(d(/\y.X(y), Y))   
    1] d#(/\x.minus(X(x)), Y) =#> d#(/\y.X(y), Y)   
    2] d#(/\x.minus(X(x)), Y) =#> X(y)   
    3] d#(/\x.pls(X(x), Y(x)), Z) =#> pls#(d(/\y.X(y), Z), d(/\z.Y(z), Z))   
    4] d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z)   
    5] d#(/\x.pls(X(x), Y(x)), Z) =#> X(y)   
    6] d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z)   
    7] d#(/\x.pls(X(x), Y(x)), Z) =#> Y(y)   
    8] d#(/\x.mul(X(x), Y(x)), Z) =#> pls#(mul(d(/\y.X(y), Z), Y(Z)), mul(X(Z), d(/\z.Y(z), Z)))   
    9] d#(/\x.mul(X(x), Y(x)), Z) =#> mul#(d(/\y.X(y), Z), Y(Z))   
    10] d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z)   
    11] d#(/\x.mul(X(x), Y(x)), Z) =#> X(y)   
    12] d#(/\x.mul(X(x), Y(x)), Z) =#> Y(Z)   
    13] d#(/\x.mul(X(x), Y(x)), Z) =#> mul#(X(Z), d(/\y.Y(y), Z))   
    14] d#(/\x.mul(X(x), Y(x)), Z) =#> X(Z)   
    15] d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z)   
    16] d#(/\x.mul(X(x), Y(x)), Z) =#> Y(y)   
    17] d#(/\x.sin(X(x)), Y) =#> mul#(cos(Y), d(/\y.X(y), Y))   
    18] d#(/\x.sin(X(x)), Y) =#> d#(/\y.X(y), Y)   
    19] d#(/\x.sin(X(x)), Y) =#> X(y)   
    20] d#(/\x.cos(X(x)), Y) =#> mul#(minus(sin(Y)), d(/\y.X(y), Y))   
    21] d#(/\x.cos(X(x)), Y) =#> minus#(sin(Y))   
    22] d#(/\x.cos(X(x)), Y) =#> d#(/\y.X(y), Y)   
    23] d#(/\x.cos(X(x)), Y) =#> X(y)   

  Rules R_0:

    d(/\x.X, Y) => 0 
    d(/\x.x, X) => 1 
    d(/\x.minus(X(x)), Y) => minus(d(/\y.X(y), Y)) 
    d(/\x.pls(X(x), Y(x)), Z) => pls(d(/\y.X(y), Z), d(/\z.Y(z), Z)) 
    d(/\x.mul(X(x), Y(x)), Z) => pls(mul(d(/\y.X(y), Z), Y(Z)), mul(X(Z), d(/\z.Y(z), Z))) 
    d(/\x.sin(X(x)), Y) => mul(cos(Y), d(/\y.X(y), Y)) 
    d(/\x.cos(X(x)), Y) => mul(minus(sin(Y)), d(/\y.X(y), Y)) 
    minus(0) => 0 
    mul(0, X) => 0 
    mul(X, 0) => 0 
    pls(0, X) => X 

Thus, the original system is terminating if (P_0, R_0, minimal, all) is finite.

We consider the dependency pair problem (P_0, R_0, minimal, all).

We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows:

    * 0 :  
    * 1 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 2 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 3 :  
    * 4 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 5 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 6 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 7 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 8 :  
    * 9 :  
    * 10 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 11 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 12 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 13 :  
    * 14 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 15 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 16 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 17 :  
    * 18 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 19 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 20 :  
    * 21 :  
    * 22 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 23 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 

This graph has the following strongly connected components:

  P_1:

    d#(/\x.minus(X(x)), Y) =#> d#(/\y.X(y), Y)   
    d#(/\x.minus(X(x)), Y) =#> X(y)   
    d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z)   
    d#(/\x.pls(X(x), Y(x)), Z) =#> X(y)   
    d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z)   
    d#(/\x.pls(X(x), Y(x)), Z) =#> Y(y)   
    d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z)   
    d#(/\x.mul(X(x), Y(x)), Z) =#> X(y)   
    d#(/\x.mul(X(x), Y(x)), Z) =#> Y(Z)   
    d#(/\x.mul(X(x), Y(x)), Z) =#> X(Z)   
    d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z)   
    d#(/\x.mul(X(x), Y(x)), Z) =#> Y(y)   
    d#(/\x.sin(X(x)), Y) =#> d#(/\y.X(y), Y)   
    d#(/\x.sin(X(x)), Y) =#> X(y)   
    d#(/\x.cos(X(x)), Y) =#> d#(/\y.X(y), Y)   
    d#(/\x.cos(X(x)), Y) =#> X(y)   

By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_0, R_0, m, f) by (P_1, R_0, m, f).

Thus, the original system is terminating if (P_1, R_0, minimal, all) is finite.

We consider the dependency pair problem (P_1, R_0, minimal, all).

We will use the reduction pair processor [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  d#(/\x.minus(X(x)), Y) >? d#(/\y.X(y), Y) 
  d#(/\x.minus(X(x)), Y) >? X(~c0) 
  d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) 
  d#(/\x.pls(X(x), Y(x)), Z) >? X(~c1) 
  d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) 
  d#(/\x.pls(X(x), Y(x)), Z) >? Y(~c2) 
  d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >? X(~c3) 
  d#(/\x.mul(X(x), Y(x)), Z) >? Y(Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >? X(Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >? Y(~c4) 
  d#(/\x.sin(X(x)), Y) >? d#(/\y.X(y), Y) 
  d#(/\x.sin(X(x)), Y) >? X(~c5) 
  d#(/\x.cos(X(x)), Y) >? d#(/\y.X(y), Y) 
  d#(/\x.cos(X(x)), Y) >? X(~c6) 
  d(/\x.X, Y) >= 0 
  d(/\x.x, X) >= 1 
  d(/\x.minus(X(x)), Y) >= minus(d(/\y.X(y), Y)) 
  d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\y.X(y), Z), d(/\z.Y(z), Z)) 
  d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\y.X(y), Z), Y(Z)), mul(X(Z), d(/\z.Y(z), Z))) 
  d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\y.X(y), Y)) 
  d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\y.X(y), Y)) 
  minus(0) >= 0 
  mul(0, X) >= 0 
  mul(X, 0) >= 0 
  pls(0, X) >= X 
  d(F, X) >= d#(F, X) 

Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.)

We use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[0]] = _|_ 
  [[1]] = _|_ 
  [[minus(x_1)]] = x_1 
  [[~c0]] = _|_ 
  [[~c1]] = _|_ 
  [[~c2]] = _|_ 
  [[~c3]] = _|_ 
  [[~c4]] = _|_ 
  [[~c5]] = _|_ 
  [[~c6]] = _|_ 

We choose Lex = {} and Mul = {cos, d, d#, mul, pls, sin}, and the following precedence: d > cos > d# > pls > sin > mul

Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows:

  d#(/\x.X(x), Y) >= d#(/\x.X(x), Y) 
  d#(/\x.X(x), Y) >= X(_|_) 
  d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) 
  d#(/\x.pls(X(x), Y(x)), Z) >= X(_|_) 
  d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) 
  d#(/\x.pls(X(x), Y(x)), Z) >= Y(_|_) 
  d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >= X(_|_) 
  d#(/\x.mul(X(x), Y(x)), Z) >= Y(Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >= X(Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >= Y(_|_) 
  d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) 
  d#(/\x.sin(X(x)), Y) > X(_|_) 
  d#(/\x.cos(X(x)), Y) >= d#(/\x.X(x), Y) 
  d#(/\x.cos(X(x)), Y) >= X(_|_) 
  d(/\x.X, Y) >= _|_ 
  d(/\x.x, X) >= _|_ 
  d(/\x.X(x), Y) >= d(/\x.X(x), Y) 
  d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) 
  d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) 
  d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) 
  d(/\x.cos(X(x)), Y) >= mul(sin(Y), d(/\x.X(x), Y)) 
  _|_ >= _|_ 
  mul(_|_, X) >= _|_ 
  mul(X, _|_) >= _|_ 
  pls(_|_, X) >= X 
  d(F, X) >= d#(F, X) 

With these choices, we have:

  1] d#(/\x.X(x), Y) >= d#(/\x.X(x), Y)  because d# in Mul, [2] and [5], by (Fun) 
  2] /\y.X(y) >= /\y.X(y)  because [3], by (Abs) 
  3] X(x) >= X(x)  because [4], by (Meta) 
  4] x >= x  by (Var) 
  5] Y >= Y  by (Meta) 

  6] d#(/\x.X(x), Y) >= X(_|_)  because [7], by (Star) 
  7] d#*(/\x.X(x), Y) >= X(_|_)  because [8], by (Select) 
  8] X(d#*(/\x.X(x), Y)) >= X(_|_)  because [9], by (Meta) 
  9] d#*(/\x.X(x), Y) >= _|_  by (Bot) 

  10] d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.X(x), Z)  because d# in Mul, [11] and [16], by (Fun) 
  11] /\y.pls(X(y), Y(y)) >= /\y.X(y)  because [12], by (Abs) 
  12] pls(X(x), Y(x)) >= X(x)  because [13], by (Star) 
  13] pls*(X(x), Y(x)) >= X(x)  because [14], by (Select) 
  14] X(x) >= X(x)  because [15], by (Meta) 
  15] x >= x  by (Var) 
  16] Z >= Z  by (Meta) 

  17] d#(/\x.pls(X(x), Y(x)), Z) >= X(_|_)  because [18], by (Star) 
  18] d#*(/\x.pls(X(x), Y(x)), Z) >= X(_|_)  because [19], by (Select) 
  19] pls(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= X(_|_)  because [20], by (Star) 
  20] pls*(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= X(_|_)  because [21], by (Select) 
  21] X(d#*(/\x.pls(X(x), Y(x)), Z)) >= X(_|_)  because [22], by (Meta) 
  22] d#*(/\x.pls(X(x), Y(x)), Z) >= _|_  by (Bot) 

  23] d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z)  because d# in Mul, [24] and [16], by (Fun) 
  24] /\y.pls(X(y), Y(y)) >= /\y.Y(y)  because [25], by (Abs) 
  25] pls(X(x), Y(x)) >= Y(x)  because [26], by (Star) 
  26] pls*(X(x), Y(x)) >= Y(x)  because [27], by (Select) 
  27] Y(x) >= Y(x)  because [28], by (Meta) 
  28] x >= x  by (Var) 

  29] d#(/\x.pls(X(x), Y(x)), Z) >= Y(_|_)  because [30], by (Star) 
  30] d#*(/\x.pls(X(x), Y(x)), Z) >= Y(_|_)  because [31], by (Select) 
  31] pls(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= Y(_|_)  because [32], by (Star) 
  32] pls*(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= Y(_|_)  because [33], by (Select) 
  33] Y(d#*(/\x.pls(X(x), Y(x)), Z)) >= Y(_|_)  because [34], by (Meta) 
  34] d#*(/\x.pls(X(x), Y(x)), Z) >= _|_  by (Bot) 

  35] d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z)  because d# in Mul, [36] and [41], by (Fun) 
  36] /\y.mul(X(y), Y(y)) >= /\y.X(y)  because [37], by (Abs) 
  37] mul(X(x), Y(x)) >= X(x)  because [38], by (Star) 
  38] mul*(X(x), Y(x)) >= X(x)  because [39], by (Select) 
  39] X(x) >= X(x)  because [40], by (Meta) 
  40] x >= x  by (Var) 
  41] Z >= Z  by (Meta) 

  42] d#(/\x.mul(X(x), Y(x)), Z) >= X(_|_)  because [43], by (Star) 
  43] d#*(/\x.mul(X(x), Y(x)), Z) >= X(_|_)  because [44], by (Select) 
  44] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(_|_)  because [45], by (Star) 
  45] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(_|_)  because [46], by (Select) 
  46] X(d#*(/\x.mul(X(x), Y(x)), Z)) >= X(_|_)  because [47], by (Meta) 
  47] d#*(/\x.mul(X(x), Y(x)), Z) >= _|_  by (Bot) 

  48] d#(/\x.mul(X(x), Y(x)), Z) >= Y(Z)  because [49], by (Star) 
  49] d#*(/\x.mul(X(x), Y(x)), Z) >= Y(Z)  because [50], by (Select) 
  50] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z)  because [51], by (Star) 
  51] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z)  because [52], by (Select) 
  52] Y(d#*(/\x.mul(X(x), Y(x)), Z)) >= Y(Z)  because [53], by (Meta) 
  53] d#*(/\x.mul(X(x), Y(x)), Z) >= Z  because [41], by (Select) 

  54] d#(/\x.mul(X(x), Y(x)), Z) >= X(Z)  because [55], by (Star) 
  55] d#*(/\x.mul(X(x), Y(x)), Z) >= X(Z)  because [56], by (Select) 
  56] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z)  because [57], by (Star) 
  57] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z)  because [58], by (Select) 
  58] X(d#*(/\x.mul(X(x), Y(x)), Z)) >= X(Z)  because [53], by (Meta) 

  59] d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z)  because d# in Mul, [60] and [41], by (Fun) 
  60] /\y.mul(X(y), Y(y)) >= /\y.Y(y)  because [61], by (Abs) 
  61] mul(X(x), Y(x)) >= Y(x)  because [62], by (Star) 
  62] mul*(X(x), Y(x)) >= Y(x)  because [63], by (Select) 
  63] Y(x) >= Y(x)  because [64], by (Meta) 
  64] x >= x  by (Var) 

  65] d#(/\x.mul(X(x), Y(x)), Z) >= Y(_|_)  because [66], by (Star) 
  66] d#*(/\x.mul(X(x), Y(x)), Z) >= Y(_|_)  because [67], by (Select) 
  67] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(_|_)  because [68], by (Star) 
  68] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(_|_)  because [69], by (Select) 
  69] Y(d#*(/\x.mul(X(x), Y(x)), Z)) >= Y(_|_)  because [70], by (Meta) 
  70] d#*(/\x.mul(X(x), Y(x)), Z) >= _|_  by (Bot) 

  71] d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y)  because [72], by (Star) 
  72] d#*(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y)  because d# in Mul, [73] and [78], by (Stat) 
  73] /\x.sin(X(x)) > /\x.X(x)  because [74], by definition 
  74] /\y.sin*(X(y)) >= /\y.X(y)  because [75], by (Abs) 
  75] sin*(X(x)) >= X(x)  because [76], by (Select) 
  76] X(x) >= X(x)  because [77], by (Meta) 
  77] x >= x  by (Var) 
  78] Y >= Y  by (Meta) 

  79] d#(/\x.sin(X(x)), Y) > X(_|_)  because [80], by definition 
  80] d#*(/\x.sin(X(x)), Y) >= X(_|_)  because [81], by (Select) 
  81] sin(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_)  because [82], by (Star) 
  82] sin*(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_)  because [83], by (Select) 
  83] X(d#*(/\x.sin(X(x)), Y)) >= X(_|_)  because [84], by (Meta) 
  84] d#*(/\x.sin(X(x)), Y) >= _|_  by (Bot) 

  85] d#(/\x.cos(X(x)), Y) >= d#(/\x.X(x), Y)  because [86], by (Star) 
  86] d#*(/\x.cos(X(x)), Y) >= d#(/\x.X(x), Y)  because d# in Mul, [87] and [92], by (Stat) 
  87] /\x.cos(X(x)) > /\x.X(x)  because [88], by definition 
  88] /\y.cos*(X(y)) >= /\y.X(y)  because [89], by (Abs) 
  89] cos*(X(x)) >= X(x)  because [90], by (Select) 
  90] X(x) >= X(x)  because [91], by (Meta) 
  91] x >= x  by (Var) 
  92] Y >= Y  by (Meta) 

  93] d#(/\x.cos(X(x)), Y) >= X(_|_)  because [94], by (Star) 
  94] d#*(/\x.cos(X(x)), Y) >= X(_|_)  because [95], by (Select) 
  95] cos(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_)  because [96], by (Star) 
  96] cos*(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_)  because [97], by (Select) 
  97] X(d#*(/\x.cos(X(x)), Y)) >= X(_|_)  because [98], by (Meta) 
  98] d#*(/\x.cos(X(x)), Y) >= _|_  by (Bot) 

  99] d(/\x.X, Y) >= _|_  by (Bot) 

  100] d(/\x.x, X) >= _|_  by (Bot) 

  101] d(/\x.X(x), Y) >= d(/\x.X(x), Y)  because d in Mul, [2] and [5], by (Fun) 

  102] d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z))  because [103], by (Star) 
  103] d*(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z))  because d > pls, [104] and [110], by (Copy) 
  104] d*(/\x.pls(X(x), Y(x)), Z) >= d(/\x.X(x), Z)  because d in Mul, [105] and [16], by (Stat) 
  105] /\x.pls(X(x), Y(x)) > /\x.X(x)  because [106], by definition 
  106] /\y.pls*(X(y), Y(y)) >= /\y.X(y)  because [107], by (Abs) 
  107] pls*(X(x), Y(x)) >= X(x)  because [108], by (Select) 
  108] X(x) >= X(x)  because [109], by (Meta) 
  109] x >= x  by (Var) 
  110] d*(/\y.pls(X(y), Y(y)), Z) >= d(/\y.Y(y), Z)  because d in Mul, [111] and [16], by (Stat) 
  111] /\y.pls(X(y), Y(y)) > /\y.Y(y)  because [112], by definition 
  112] /\z.pls*(X(z), Y(z)) >= /\z.Y(z)  because [113], by (Abs) 
  113] pls*(X(y), Y(y)) >= Y(y)  because [114], by (Select) 
  114] Y(y) >= Y(y)  because [115], by (Meta) 
  115] y >= y  by (Var) 

  116] d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z)))  because [117], by (Star) 
  117] d*(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z)))  because d > pls, [118] and [130], by (Copy) 
  118] d*(/\x.mul(X(x), Y(x)), Z) >= mul(d(/\x.X(x), Z), Y(Z))  because d > mul, [119] and [125], by (Copy) 
  119] d*(/\x.mul(X(x), Y(x)), Z) >= d(/\x.X(x), Z)  because d in Mul, [120] and [41], by (Stat) 
  120] /\x.mul(X(x), Y(x)) > /\x.X(x)  because [121], by definition 
  121] /\y.mul*(X(y), Y(y)) >= /\y.X(y)  because [122], by (Abs) 
  122] mul*(X(x), Y(x)) >= X(x)  because [123], by (Select) 
  123] X(x) >= X(x)  because [124], by (Meta) 
  124] x >= x  by (Var) 
  125] d*(/\y.mul(X(y), Y(y)), Z) >= Y(Z)  because [126], by (Select) 
  126] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z)  because [127], by (Star) 
  127] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z)  because [128], by (Select) 
  128] Y(d*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z)  because [129], by (Meta) 
  129] d*(/\y.mul(X(y), Y(y)), Z) >= Z  because [41], by (Select) 
  130] d*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), d(/\y.Y(y), Z))  because d > mul, [131] and [135], by (Copy) 
  131] d*(/\y.mul(X(y), Y(y)), Z) >= X(Z)  because [132], by (Select) 
  132] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z)  because [133], by (Star) 
  133] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z)  because [134], by (Select) 
  134] X(d*(/\y.mul(X(y), Y(y)), Z)) >= X(Z)  because [129], by (Meta) 
  135] d*(/\y.mul(X(y), Y(y)), Z) >= d(/\y.Y(y), Z)  because d in Mul, [136] and [41], by (Stat) 
  136] /\y.mul(X(y), Y(y)) > /\y.Y(y)  because [137], by definition 
  137] /\z.mul*(X(z), Y(z)) >= /\z.Y(z)  because [138], by (Abs) 
  138] mul*(X(y), Y(y)) >= Y(y)  because [139], by (Select) 
  139] Y(y) >= Y(y)  because [140], by (Meta) 
  140] y >= y  by (Var) 

  141] d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y))  because [142], by (Star) 
  142] d*(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y))  because d > mul, [143] and [145], by (Copy) 
  143] d*(/\x.sin(X(x)), Y) >= cos(Y)  because d > cos and [144], by (Copy) 
  144] d*(/\x.sin(X(x)), Y) >= Y  because [78], by (Select) 
  145] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y)  because d in Mul, [73] and [78], by (Stat) 

  146] d(/\x.cos(X(x)), Y) >= mul(sin(Y), d(/\x.X(x), Y))  because [147], by (Star) 
  147] d*(/\x.cos(X(x)), Y) >= mul(sin(Y), d(/\x.X(x), Y))  because d > mul, [148] and [150], by (Copy) 
  148] d*(/\x.cos(X(x)), Y) >= sin(Y)  because d > sin and [149], by (Copy) 
  149] d*(/\x.cos(X(x)), Y) >= Y  because [92], by (Select) 
  150] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y)  because d in Mul, [87] and [92], by (Stat) 

  151] _|_ >= _|_  by (Bot) 

  152] mul(_|_, X) >= _|_  by (Bot) 

  153] mul(X, _|_) >= _|_  by (Bot) 

  154] pls(_|_, X) >= X  because [155], by (Star) 
  155] pls*(_|_, X) >= X  because [156], by (Select) 
  156] X >= X  by (Meta) 

  157] d(F, X) >= d#(F, X)  because [158], by (Star) 
  158] d*(F, X) >= d#(F, X)  because d > d#, [159] and [161], by (Copy) 
  159] d*(F, X) >= F  because [160], by (Select) 
  160] F >= F  by (Meta) 
  161] d*(F, X) >= X  because [162], by (Select) 
  162] X >= X  by (Meta) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_1, R_0, minimal, all) by (P_2, R_0, minimal, all), where P_2 consists of:

  d#(/\x.minus(X(x)), Y) =#> d#(/\y.X(y), Y)   
  d#(/\x.minus(X(x)), Y) =#> X(y)   
  d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z)   
  d#(/\x.pls(X(x), Y(x)), Z) =#> X(y)   
  d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z)   
  d#(/\x.pls(X(x), Y(x)), Z) =#> Y(y)   
  d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z)   
  d#(/\x.mul(X(x), Y(x)), Z) =#> X(y)   
  d#(/\x.mul(X(x), Y(x)), Z) =#> Y(Z)   
  d#(/\x.mul(X(x), Y(x)), Z) =#> X(Z)   
  d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z)   
  d#(/\x.mul(X(x), Y(x)), Z) =#> Y(y)   
  d#(/\x.sin(X(x)), Y) =#> d#(/\y.X(y), Y)   
  d#(/\x.cos(X(x)), Y) =#> d#(/\y.X(y), Y)   
  d#(/\x.cos(X(x)), Y) =#> X(y)   

Thus, the original system is terminating if (P_2, R_0, minimal, all) is finite.

We consider the dependency pair problem (P_2, R_0, minimal, all).

We will use the reduction pair processor [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  d#(/\x.minus(X(x)), Y) >? d#(/\y.X(y), Y) 
  d#(/\x.minus(X(x)), Y) >? X(~c0) 
  d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) 
  d#(/\x.pls(X(x), Y(x)), Z) >? X(~c1) 
  d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) 
  d#(/\x.pls(X(x), Y(x)), Z) >? Y(~c2) 
  d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >? X(~c3) 
  d#(/\x.mul(X(x), Y(x)), Z) >? Y(Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >? X(Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >? Y(~c4) 
  d#(/\x.sin(X(x)), Y) >? d#(/\y.X(y), Y) 
  d#(/\x.cos(X(x)), Y) >? d#(/\y.X(y), Y) 
  d#(/\x.cos(X(x)), Y) >? X(~c5) 
  d(/\x.X, Y) >= 0 
  d(/\x.x, X) >= 1 
  d(/\x.minus(X(x)), Y) >= minus(d(/\y.X(y), Y)) 
  d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\y.X(y), Z), d(/\z.Y(z), Z)) 
  d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\y.X(y), Z), Y(Z)), mul(X(Z), d(/\z.Y(z), Z))) 
  d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\y.X(y), Y)) 
  d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\y.X(y), Y)) 
  minus(0) >= 0 
  mul(0, X) >= 0 
  mul(X, 0) >= 0 
  pls(0, X) >= X 
  d(F, X) >= d#(F, X) 

Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.)

We use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[0]] = _|_ 
  [[1]] = _|_ 
  [[~c0]] = _|_ 
  [[~c1]] = _|_ 
  [[~c2]] = _|_ 
  [[~c3]] = _|_ 
  [[~c4]] = _|_ 
  [[~c5]] = _|_ 

We choose Lex = {} and Mul = {cos, d, d#, minus, mul, pls, sin}, and the following precedence: d > d# > minus > cos > mul > pls > sin

Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows:

  d#(/\x.minus(X(x)), Y) >= d#(/\x.X(x), Y) 
  d#(/\x.minus(X(x)), Y) > X(_|_) 
  d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) 
  d#(/\x.pls(X(x), Y(x)), Z) >= X(_|_) 
  d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) 
  d#(/\x.pls(X(x), Y(x)), Z) > Y(_|_) 
  d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) > X(_|_) 
  d#(/\x.mul(X(x), Y(x)), Z) >= Y(Z) 
  d#(/\x.mul(X(x), Y(x)), Z) > X(Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >= Y(_|_) 
  d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) 
  d#(/\x.cos(X(x)), Y) >= d#(/\x.X(x), Y) 
  d#(/\x.cos(X(x)), Y) >= X(_|_) 
  d(/\x.X, Y) >= _|_ 
  d(/\x.x, X) >= _|_ 
  d(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) 
  d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) 
  d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) 
  d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) 
  d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) 
  minus(_|_) >= _|_ 
  mul(_|_, X) >= _|_ 
  mul(X, _|_) >= _|_ 
  pls(_|_, X) >= X 
  d(F, X) >= d#(F, X) 

With these choices, we have:

  1] d#(/\x.minus(X(x)), Y) >= d#(/\x.X(x), Y)  because d# in Mul, [2] and [7], by (Fun) 
  2] /\y.minus(X(y)) >= /\y.X(y)  because [3], by (Abs) 
  3] minus(X(x)) >= X(x)  because [4], by (Star) 
  4] minus*(X(x)) >= X(x)  because [5], by (Select) 
  5] X(x) >= X(x)  because [6], by (Meta) 
  6] x >= x  by (Var) 
  7] Y >= Y  by (Meta) 

  8] d#(/\x.minus(X(x)), Y) > X(_|_)  because [9], by definition 
  9] d#*(/\x.minus(X(x)), Y) >= X(_|_)  because [10], by (Select) 
  10] minus(X(d#*(/\x.minus(X(x)), Y))) >= X(_|_)  because [11], by (Star) 
  11] minus*(X(d#*(/\x.minus(X(x)), Y))) >= X(_|_)  because [12], by (Select) 
  12] X(d#*(/\x.minus(X(x)), Y)) >= X(_|_)  because [13], by (Meta) 
  13] d#*(/\x.minus(X(x)), Y) >= _|_  by (Bot) 

  14] d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.X(x), Z)  because d# in Mul, [15] and [20], by (Fun) 
  15] /\y.pls(X(y), Y(y)) >= /\y.X(y)  because [16], by (Abs) 
  16] pls(X(x), Y(x)) >= X(x)  because [17], by (Star) 
  17] pls*(X(x), Y(x)) >= X(x)  because [18], by (Select) 
  18] X(x) >= X(x)  because [19], by (Meta) 
  19] x >= x  by (Var) 
  20] Z >= Z  by (Meta) 

  21] d#(/\x.pls(X(x), Y(x)), Z) >= X(_|_)  because [22], by (Star) 
  22] d#*(/\x.pls(X(x), Y(x)), Z) >= X(_|_)  because [23], by (Select) 
  23] pls(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= X(_|_)  because [24], by (Star) 
  24] pls*(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= X(_|_)  because [25], by (Select) 
  25] X(d#*(/\x.pls(X(x), Y(x)), Z)) >= X(_|_)  because [26], by (Meta) 
  26] d#*(/\x.pls(X(x), Y(x)), Z) >= _|_  by (Bot) 

  27] d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z)  because d# in Mul, [28] and [20], by (Fun) 
  28] /\y.pls(X(y), Y(y)) >= /\y.Y(y)  because [29], by (Abs) 
  29] pls(X(x), Y(x)) >= Y(x)  because [30], by (Star) 
  30] pls*(X(x), Y(x)) >= Y(x)  because [31], by (Select) 
  31] Y(x) >= Y(x)  because [32], by (Meta) 
  32] x >= x  by (Var) 

  33] d#(/\x.pls(X(x), Y(x)), Z) > Y(_|_)  because [34], by definition 
  34] d#*(/\x.pls(X(x), Y(x)), Z) >= Y(_|_)  because [35], by (Select) 
  35] pls(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= Y(_|_)  because [36], by (Star) 
  36] pls*(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= Y(_|_)  because [37], by (Select) 
  37] Y(d#*(/\x.pls(X(x), Y(x)), Z)) >= Y(_|_)  because [38], by (Meta) 
  38] d#*(/\x.pls(X(x), Y(x)), Z) >= _|_  by (Bot) 

  39] d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z)  because d# in Mul, [40] and [45], by (Fun) 
  40] /\y.mul(X(y), Y(y)) >= /\y.X(y)  because [41], by (Abs) 
  41] mul(X(x), Y(x)) >= X(x)  because [42], by (Star) 
  42] mul*(X(x), Y(x)) >= X(x)  because [43], by (Select) 
  43] X(x) >= X(x)  because [44], by (Meta) 
  44] x >= x  by (Var) 
  45] Z >= Z  by (Meta) 

  46] d#(/\x.mul(X(x), Y(x)), Z) > X(_|_)  because [47], by definition 
  47] d#*(/\x.mul(X(x), Y(x)), Z) >= X(_|_)  because [48], by (Select) 
  48] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(_|_)  because [49], by (Star) 
  49] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(_|_)  because [50], by (Select) 
  50] X(d#*(/\x.mul(X(x), Y(x)), Z)) >= X(_|_)  because [51], by (Meta) 
  51] d#*(/\x.mul(X(x), Y(x)), Z) >= _|_  by (Bot) 

  52] d#(/\x.mul(X(x), Y(x)), Z) >= Y(Z)  because [53], by (Star) 
  53] d#*(/\x.mul(X(x), Y(x)), Z) >= Y(Z)  because [54], by (Select) 
  54] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z)  because [55], by (Star) 
  55] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z)  because [56], by (Select) 
  56] Y(d#*(/\x.mul(X(x), Y(x)), Z)) >= Y(Z)  because [57], by (Meta) 
  57] d#*(/\x.mul(X(x), Y(x)), Z) >= Z  because [45], by (Select) 

  58] d#(/\x.mul(X(x), Y(x)), Z) > X(Z)  because [59], by definition 
  59] d#*(/\x.mul(X(x), Y(x)), Z) >= X(Z)  because [60], by (Select) 
  60] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z)  because [61], by (Star) 
  61] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z)  because [62], by (Select) 
  62] X(d#*(/\x.mul(X(x), Y(x)), Z)) >= X(Z)  because [57], by (Meta) 

  63] d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z)  because d# in Mul, [64] and [45], by (Fun) 
  64] /\y.mul(X(y), Y(y)) >= /\y.Y(y)  because [65], by (Abs) 
  65] mul(X(x), Y(x)) >= Y(x)  because [66], by (Star) 
  66] mul*(X(x), Y(x)) >= Y(x)  because [67], by (Select) 
  67] Y(x) >= Y(x)  because [68], by (Meta) 
  68] x >= x  by (Var) 

  69] d#(/\x.mul(X(x), Y(x)), Z) >= Y(_|_)  because [70], by (Star) 
  70] d#*(/\x.mul(X(x), Y(x)), Z) >= Y(_|_)  because [71], by (Select) 
  71] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(_|_)  because [72], by (Star) 
  72] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(_|_)  because [73], by (Select) 
  73] Y(d#*(/\x.mul(X(x), Y(x)), Z)) >= Y(_|_)  because [74], by (Meta) 
  74] d#*(/\x.mul(X(x), Y(x)), Z) >= _|_  by (Bot) 

  75] d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y)  because d# in Mul, [76] and [81], by (Fun) 
  76] /\y.sin(X(y)) >= /\y.X(y)  because [77], by (Abs) 
  77] sin(X(x)) >= X(x)  because [78], by (Star) 
  78] sin*(X(x)) >= X(x)  because [79], by (Select) 
  79] X(x) >= X(x)  because [80], by (Meta) 
  80] x >= x  by (Var) 
  81] Y >= Y  by (Meta) 

  82] d#(/\x.cos(X(x)), Y) >= d#(/\x.X(x), Y)  because [83], by (Star) 
  83] d#*(/\x.cos(X(x)), Y) >= d#(/\x.X(x), Y)  because d# in Mul, [84] and [89], by (Stat) 
  84] /\x.cos(X(x)) > /\x.X(x)  because [85], by definition 
  85] /\y.cos*(X(y)) >= /\y.X(y)  because [86], by (Abs) 
  86] cos*(X(x)) >= X(x)  because [87], by (Select) 
  87] X(x) >= X(x)  because [88], by (Meta) 
  88] x >= x  by (Var) 
  89] Y >= Y  by (Meta) 

  90] d#(/\x.cos(X(x)), Y) >= X(_|_)  because [91], by (Star) 
  91] d#*(/\x.cos(X(x)), Y) >= X(_|_)  because [92], by (Select) 
  92] cos(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_)  because [93], by (Star) 
  93] cos*(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_)  because [94], by (Select) 
  94] X(d#*(/\x.cos(X(x)), Y)) >= X(_|_)  because [95], by (Meta) 
  95] d#*(/\x.cos(X(x)), Y) >= _|_  by (Bot) 

  96] d(/\x.X, Y) >= _|_  by (Bot) 

  97] d(/\x.x, X) >= _|_  by (Bot) 

  98] d(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y))  because [99], by (Star) 
  99] d*(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y))  because d > minus and [100], by (Copy) 
  100] d*(/\x.minus(X(x)), Y) >= d(/\x.X(x), Y)  because d in Mul, [101] and [7], by (Stat) 
  101] /\x.minus(X(x)) > /\x.X(x)  because [102], by definition 
  102] /\y.minus*(X(y)) >= /\y.X(y)  because [103], by (Abs) 
  103] minus*(X(x)) >= X(x)  because [104], by (Select) 
  104] X(x) >= X(x)  because [105], by (Meta) 
  105] x >= x  by (Var) 

  106] d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z))  because [107], by (Star) 
  107] d*(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z))  because d > pls, [108] and [114], by (Copy) 
  108] d*(/\x.pls(X(x), Y(x)), Z) >= d(/\x.X(x), Z)  because d in Mul, [109] and [20], by (Stat) 
  109] /\x.pls(X(x), Y(x)) > /\x.X(x)  because [110], by definition 
  110] /\y.pls*(X(y), Y(y)) >= /\y.X(y)  because [111], by (Abs) 
  111] pls*(X(x), Y(x)) >= X(x)  because [112], by (Select) 
  112] X(x) >= X(x)  because [113], by (Meta) 
  113] x >= x  by (Var) 
  114] d*(/\y.pls(X(y), Y(y)), Z) >= d(/\y.Y(y), Z)  because d in Mul, [115] and [20], by (Stat) 
  115] /\y.pls(X(y), Y(y)) > /\y.Y(y)  because [116], by definition 
  116] /\z.pls*(X(z), Y(z)) >= /\z.Y(z)  because [117], by (Abs) 
  117] pls*(X(y), Y(y)) >= Y(y)  because [118], by (Select) 
  118] Y(y) >= Y(y)  because [119], by (Meta) 
  119] y >= y  by (Var) 

  120] d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z)))  because [121], by (Star) 
  121] d*(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z)))  because d > pls, [122] and [134], by (Copy) 
  122] d*(/\x.mul(X(x), Y(x)), Z) >= mul(d(/\x.X(x), Z), Y(Z))  because d > mul, [123] and [129], by (Copy) 
  123] d*(/\x.mul(X(x), Y(x)), Z) >= d(/\x.X(x), Z)  because d in Mul, [124] and [45], by (Stat) 
  124] /\x.mul(X(x), Y(x)) > /\x.X(x)  because [125], by definition 
  125] /\y.mul*(X(y), Y(y)) >= /\y.X(y)  because [126], by (Abs) 
  126] mul*(X(x), Y(x)) >= X(x)  because [127], by (Select) 
  127] X(x) >= X(x)  because [128], by (Meta) 
  128] x >= x  by (Var) 
  129] d*(/\y.mul(X(y), Y(y)), Z) >= Y(Z)  because [130], by (Select) 
  130] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z)  because [131], by (Star) 
  131] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z)  because [132], by (Select) 
  132] Y(d*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z)  because [133], by (Meta) 
  133] d*(/\y.mul(X(y), Y(y)), Z) >= Z  because [45], by (Select) 
  134] d*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), d(/\y.Y(y), Z))  because d > mul, [135] and [139], by (Copy) 
  135] d*(/\y.mul(X(y), Y(y)), Z) >= X(Z)  because [136], by (Select) 
  136] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z)  because [137], by (Star) 
  137] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z)  because [138], by (Select) 
  138] X(d*(/\y.mul(X(y), Y(y)), Z)) >= X(Z)  because [133], by (Meta) 
  139] d*(/\y.mul(X(y), Y(y)), Z) >= d(/\y.Y(y), Z)  because d in Mul, [140] and [45], by (Stat) 
  140] /\y.mul(X(y), Y(y)) > /\y.Y(y)  because [141], by definition 
  141] /\z.mul*(X(z), Y(z)) >= /\z.Y(z)  because [142], by (Abs) 
  142] mul*(X(y), Y(y)) >= Y(y)  because [143], by (Select) 
  143] Y(y) >= Y(y)  because [144], by (Meta) 
  144] y >= y  by (Var) 

  145] d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y))  because [146], by (Star) 
  146] d*(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y))  because d > mul, [147] and [149], by (Copy) 
  147] d*(/\x.sin(X(x)), Y) >= cos(Y)  because d > cos and [148], by (Copy) 
  148] d*(/\x.sin(X(x)), Y) >= Y  because [81], by (Select) 
  149] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y)  because d in Mul, [150] and [81], by (Stat) 
  150] /\x.sin(X(x)) > /\x.X(x)  because [151], by definition 
  151] /\y.sin*(X(y)) >= /\y.X(y)  because [152], by (Abs) 
  152] sin*(X(x)) >= X(x)  because [153], by (Select) 
  153] X(x) >= X(x)  because [154], by (Meta) 
  154] x >= x  by (Var) 

  155] d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y))  because [156], by (Star) 
  156] d*(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y))  because d > mul, [157] and [160], by (Copy) 
  157] d*(/\x.cos(X(x)), Y) >= minus(sin(Y))  because d > minus and [158], by (Copy) 
  158] d*(/\x.cos(X(x)), Y) >= sin(Y)  because d > sin and [159], by (Copy) 
  159] d*(/\x.cos(X(x)), Y) >= Y  because [89], by (Select) 
  160] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y)  because d in Mul, [84] and [89], by (Stat) 

  161] minus(_|_) >= _|_  by (Bot) 

  162] mul(_|_, X) >= _|_  by (Bot) 

  163] mul(X, _|_) >= _|_  by (Bot) 

  164] pls(_|_, X) >= X  because [165], by (Star) 
  165] pls*(_|_, X) >= X  because [166], by (Select) 
  166] X >= X  by (Meta) 

  167] d(F, X) >= d#(F, X)  because [168], by (Star) 
  168] d*(F, X) >= d#(F, X)  because d > d#, [169] and [171], by (Copy) 
  169] d*(F, X) >= F  because [170], by (Select) 
  170] F >= F  by (Meta) 
  171] d*(F, X) >= X  because [172], by (Select) 
  172] X >= X  by (Meta) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_2, R_0, minimal, all) by (P_3, R_0, minimal, all), where P_3 consists of:

  d#(/\x.minus(X(x)), Y) =#> d#(/\y.X(y), Y)   
  d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z)   
  d#(/\x.pls(X(x), Y(x)), Z) =#> X(y)   
  d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z)   
  d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z)   
  d#(/\x.mul(X(x), Y(x)), Z) =#> Y(Z)   
  d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z)   
  d#(/\x.mul(X(x), Y(x)), Z) =#> Y(y)   
  d#(/\x.sin(X(x)), Y) =#> d#(/\y.X(y), Y)   
  d#(/\x.cos(X(x)), Y) =#> d#(/\y.X(y), Y)   
  d#(/\x.cos(X(x)), Y) =#> X(y)   

Thus, the original system is terminating if (P_3, R_0, minimal, all) is finite.

We consider the dependency pair problem (P_3, R_0, minimal, all).

We will use the reduction pair processor [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  d#(/\x.minus(X(x)), Y) >? d#(/\y.X(y), Y) 
  d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) 
  d#(/\x.pls(X(x), Y(x)), Z) >? X(~c0) 
  d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >? Y(Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >? Y(~c1) 
  d#(/\x.sin(X(x)), Y) >? d#(/\y.X(y), Y) 
  d#(/\x.cos(X(x)), Y) >? d#(/\y.X(y), Y) 
  d#(/\x.cos(X(x)), Y) >? X(~c2) 
  d(/\x.X, Y) >= 0 
  d(/\x.x, X) >= 1 
  d(/\x.minus(X(x)), Y) >= minus(d(/\y.X(y), Y)) 
  d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\y.X(y), Z), d(/\z.Y(z), Z)) 
  d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\y.X(y), Z), Y(Z)), mul(X(Z), d(/\z.Y(z), Z))) 
  d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\y.X(y), Y)) 
  d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\y.X(y), Y)) 
  minus(0) >= 0 
  mul(0, X) >= 0 
  mul(X, 0) >= 0 
  pls(0, X) >= X 
  d(F, X) >= d#(F, X) 

Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.)

We use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[0]] = _|_ 
  [[1]] = _|_ 
  [[~c0]] = _|_ 
  [[~c1]] = _|_ 
  [[~c2]] = _|_ 

We choose Lex = {} and Mul = {cos, d, d#, minus, mul, pls, sin}, and the following precedence: d > cos > d# > minus > mul > pls > sin

Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows:

  d#(/\x.minus(X(x)), Y) >= d#(/\x.X(x), Y) 
  d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) 
  d#(/\x.pls(X(x), Y(x)), Z) > X(_|_) 
  d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) > Y(Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) > Y(_|_) 
  d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) 
  d#(/\x.cos(X(x)), Y) > d#(/\x.X(x), Y) 
  d#(/\x.cos(X(x)), Y) > X(_|_) 
  d(/\x.X, Y) >= _|_ 
  d(/\x.x, X) >= _|_ 
  d(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) 
  d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) 
  d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) 
  d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) 
  d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) 
  minus(_|_) >= _|_ 
  mul(_|_, X) >= _|_ 
  mul(X, _|_) >= _|_ 
  pls(_|_, X) >= X 
  d(F, X) >= d#(F, X) 

With these choices, we have:

  1] d#(/\x.minus(X(x)), Y) >= d#(/\x.X(x), Y)  because d# in Mul, [2] and [7], by (Fun) 
  2] /\y.minus(X(y)) >= /\y.X(y)  because [3], by (Abs) 
  3] minus(X(x)) >= X(x)  because [4], by (Star) 
  4] minus*(X(x)) >= X(x)  because [5], by (Select) 
  5] X(x) >= X(x)  because [6], by (Meta) 
  6] x >= x  by (Var) 
  7] Y >= Y  by (Meta) 

  8] d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.X(x), Z)  because d# in Mul, [9] and [14], by (Fun) 
  9] /\y.pls(X(y), Y(y)) >= /\y.X(y)  because [10], by (Abs) 
  10] pls(X(x), Y(x)) >= X(x)  because [11], by (Star) 
  11] pls*(X(x), Y(x)) >= X(x)  because [12], by (Select) 
  12] X(x) >= X(x)  because [13], by (Meta) 
  13] x >= x  by (Var) 
  14] Z >= Z  by (Meta) 

  15] d#(/\x.pls(X(x), Y(x)), Z) > X(_|_)  because [16], by definition 
  16] d#*(/\x.pls(X(x), Y(x)), Z) >= X(_|_)  because [17], by (Select) 
  17] pls(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= X(_|_)  because [18], by (Star) 
  18] pls*(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= X(_|_)  because [19], by (Select) 
  19] X(d#*(/\x.pls(X(x), Y(x)), Z)) >= X(_|_)  because [20], by (Meta) 
  20] d#*(/\x.pls(X(x), Y(x)), Z) >= _|_  by (Bot) 

  21] d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z)  because d# in Mul, [22] and [14], by (Fun) 
  22] /\y.pls(X(y), Y(y)) >= /\y.Y(y)  because [23], by (Abs) 
  23] pls(X(x), Y(x)) >= Y(x)  because [24], by (Star) 
  24] pls*(X(x), Y(x)) >= Y(x)  because [25], by (Select) 
  25] Y(x) >= Y(x)  because [26], by (Meta) 
  26] x >= x  by (Var) 

  27] d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z)  because d# in Mul, [28] and [33], by (Fun) 
  28] /\y.mul(X(y), Y(y)) >= /\y.X(y)  because [29], by (Abs) 
  29] mul(X(x), Y(x)) >= X(x)  because [30], by (Star) 
  30] mul*(X(x), Y(x)) >= X(x)  because [31], by (Select) 
  31] X(x) >= X(x)  because [32], by (Meta) 
  32] x >= x  by (Var) 
  33] Z >= Z  by (Meta) 

  34] d#(/\x.mul(X(x), Y(x)), Z) > Y(Z)  because [35], by definition 
  35] d#*(/\x.mul(X(x), Y(x)), Z) >= Y(Z)  because [36], by (Select) 
  36] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z)  because [37], by (Star) 
  37] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z)  because [38], by (Select) 
  38] Y(d#*(/\x.mul(X(x), Y(x)), Z)) >= Y(Z)  because [39], by (Meta) 
  39] d#*(/\x.mul(X(x), Y(x)), Z) >= Z  because [33], by (Select) 

  40] d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z)  because d# in Mul, [41] and [33], by (Fun) 
  41] /\y.mul(X(y), Y(y)) >= /\y.Y(y)  because [42], by (Abs) 
  42] mul(X(x), Y(x)) >= Y(x)  because [43], by (Star) 
  43] mul*(X(x), Y(x)) >= Y(x)  because [44], by (Select) 
  44] Y(x) >= Y(x)  because [45], by (Meta) 
  45] x >= x  by (Var) 

  46] d#(/\x.mul(X(x), Y(x)), Z) > Y(_|_)  because [47], by definition 
  47] d#*(/\x.mul(X(x), Y(x)), Z) >= Y(_|_)  because [48], by (Select) 
  48] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(_|_)  because [49], by (Star) 
  49] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(_|_)  because [50], by (Select) 
  50] Y(d#*(/\x.mul(X(x), Y(x)), Z)) >= Y(_|_)  because [51], by (Meta) 
  51] d#*(/\x.mul(X(x), Y(x)), Z) >= _|_  by (Bot) 

  52] d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y)  because [53], by (Star) 
  53] d#*(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y)  because d# in Mul, [54] and [59], by (Stat) 
  54] /\x.sin(X(x)) > /\x.X(x)  because [55], by definition 
  55] /\y.sin*(X(y)) >= /\y.X(y)  because [56], by (Abs) 
  56] sin*(X(x)) >= X(x)  because [57], by (Select) 
  57] X(x) >= X(x)  because [58], by (Meta) 
  58] x >= x  by (Var) 
  59] Y >= Y  by (Meta) 

  60] d#(/\x.cos(X(x)), Y) > d#(/\x.X(x), Y)  because [61], by definition 
  61] d#*(/\x.cos(X(x)), Y) >= d#(/\x.X(x), Y)  because d# in Mul, [62] and [67], by (Stat) 
  62] /\x.cos(X(x)) > /\x.X(x)  because [63], by definition 
  63] /\y.cos*(X(y)) >= /\y.X(y)  because [64], by (Abs) 
  64] cos*(X(x)) >= X(x)  because [65], by (Select) 
  65] X(x) >= X(x)  because [66], by (Meta) 
  66] x >= x  by (Var) 
  67] Y >= Y  by (Meta) 

  68] d#(/\x.cos(X(x)), Y) > X(_|_)  because [69], by definition 
  69] d#*(/\x.cos(X(x)), Y) >= X(_|_)  because [70], by (Select) 
  70] cos(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_)  because [71], by (Star) 
  71] cos*(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_)  because [72], by (Select) 
  72] X(d#*(/\x.cos(X(x)), Y)) >= X(_|_)  because [73], by (Meta) 
  73] d#*(/\x.cos(X(x)), Y) >= _|_  by (Bot) 

  74] d(/\x.X, Y) >= _|_  by (Bot) 

  75] d(/\x.x, X) >= _|_  by (Bot) 

  76] d(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y))  because [77], by (Star) 
  77] d*(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y))  because d > minus and [78], by (Copy) 
  78] d*(/\x.minus(X(x)), Y) >= d(/\x.X(x), Y)  because d in Mul, [79] and [7], by (Stat) 
  79] /\x.minus(X(x)) > /\x.X(x)  because [80], by definition 
  80] /\y.minus*(X(y)) >= /\y.X(y)  because [81], by (Abs) 
  81] minus*(X(x)) >= X(x)  because [82], by (Select) 
  82] X(x) >= X(x)  because [83], by (Meta) 
  83] x >= x  by (Var) 

  84] d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z))  because [85], by (Star) 
  85] d*(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z))  because d > pls, [86] and [92], by (Copy) 
  86] d*(/\x.pls(X(x), Y(x)), Z) >= d(/\x.X(x), Z)  because d in Mul, [87] and [14], by (Stat) 
  87] /\x.pls(X(x), Y(x)) > /\x.X(x)  because [88], by definition 
  88] /\y.pls*(X(y), Y(y)) >= /\y.X(y)  because [89], by (Abs) 
  89] pls*(X(x), Y(x)) >= X(x)  because [90], by (Select) 
  90] X(x) >= X(x)  because [91], by (Meta) 
  91] x >= x  by (Var) 
  92] d*(/\y.pls(X(y), Y(y)), Z) >= d(/\y.Y(y), Z)  because d in Mul, [93] and [14], by (Stat) 
  93] /\y.pls(X(y), Y(y)) > /\y.Y(y)  because [94], by definition 
  94] /\z.pls*(X(z), Y(z)) >= /\z.Y(z)  because [95], by (Abs) 
  95] pls*(X(y), Y(y)) >= Y(y)  because [96], by (Select) 
  96] Y(y) >= Y(y)  because [97], by (Meta) 
  97] y >= y  by (Var) 

  98] d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z)))  because [99], by (Star) 
  99] d*(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z)))  because d > pls, [100] and [112], by (Copy) 
  100] d*(/\x.mul(X(x), Y(x)), Z) >= mul(d(/\x.X(x), Z), Y(Z))  because d > mul, [101] and [107], by (Copy) 
  101] d*(/\x.mul(X(x), Y(x)), Z) >= d(/\x.X(x), Z)  because d in Mul, [102] and [33], by (Stat) 
  102] /\x.mul(X(x), Y(x)) > /\x.X(x)  because [103], by definition 
  103] /\y.mul*(X(y), Y(y)) >= /\y.X(y)  because [104], by (Abs) 
  104] mul*(X(x), Y(x)) >= X(x)  because [105], by (Select) 
  105] X(x) >= X(x)  because [106], by (Meta) 
  106] x >= x  by (Var) 
  107] d*(/\y.mul(X(y), Y(y)), Z) >= Y(Z)  because [108], by (Select) 
  108] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z)  because [109], by (Star) 
  109] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z)  because [110], by (Select) 
  110] Y(d*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z)  because [111], by (Meta) 
  111] d*(/\y.mul(X(y), Y(y)), Z) >= Z  because [33], by (Select) 
  112] d*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), d(/\y.Y(y), Z))  because d > mul, [113] and [117], by (Copy) 
  113] d*(/\y.mul(X(y), Y(y)), Z) >= X(Z)  because [114], by (Select) 
  114] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z)  because [115], by (Star) 
  115] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z)  because [116], by (Select) 
  116] X(d*(/\y.mul(X(y), Y(y)), Z)) >= X(Z)  because [111], by (Meta) 
  117] d*(/\y.mul(X(y), Y(y)), Z) >= d(/\y.Y(y), Z)  because d in Mul, [118] and [33], by (Stat) 
  118] /\y.mul(X(y), Y(y)) > /\y.Y(y)  because [119], by definition 
  119] /\z.mul*(X(z), Y(z)) >= /\z.Y(z)  because [120], by (Abs) 
  120] mul*(X(y), Y(y)) >= Y(y)  because [121], by (Select) 
  121] Y(y) >= Y(y)  because [122], by (Meta) 
  122] y >= y  by (Var) 

  123] d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y))  because [124], by (Star) 
  124] d*(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y))  because d > mul, [125] and [127], by (Copy) 
  125] d*(/\x.sin(X(x)), Y) >= cos(Y)  because d > cos and [126], by (Copy) 
  126] d*(/\x.sin(X(x)), Y) >= Y  because [59], by (Select) 
  127] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y)  because d in Mul, [54] and [59], by (Stat) 

  128] d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y))  because [129], by (Star) 
  129] d*(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y))  because d > mul, [130] and [133], by (Copy) 
  130] d*(/\x.cos(X(x)), Y) >= minus(sin(Y))  because d > minus and [131], by (Copy) 
  131] d*(/\x.cos(X(x)), Y) >= sin(Y)  because d > sin and [132], by (Copy) 
  132] d*(/\x.cos(X(x)), Y) >= Y  because [67], by (Select) 
  133] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y)  because d in Mul, [62] and [67], by (Stat) 

  134] minus(_|_) >= _|_  by (Bot) 

  135] mul(_|_, X) >= _|_  by (Bot) 

  136] mul(X, _|_) >= _|_  by (Bot) 

  137] pls(_|_, X) >= X  because [138], by (Star) 
  138] pls*(_|_, X) >= X  because [139], by (Select) 
  139] X >= X  by (Meta) 

  140] d(F, X) >= d#(F, X)  because [141], by (Star) 
  141] d*(F, X) >= d#(F, X)  because d > d#, [142] and [144], by (Copy) 
  142] d*(F, X) >= F  because [143], by (Select) 
  143] F >= F  by (Meta) 
  144] d*(F, X) >= X  because [145], by (Select) 
  145] X >= X  by (Meta) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_3, R_0, minimal, all) by (P_4, R_0, minimal, all), where P_4 consists of:

  d#(/\x.minus(X(x)), Y) =#> d#(/\y.X(y), Y)   
  d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z)   
  d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z)   
  d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z)   
  d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z)   
  d#(/\x.sin(X(x)), Y) =#> d#(/\y.X(y), Y)   

Thus, the original system is terminating if (P_4, R_0, minimal, all) is finite.

We consider the dependency pair problem (P_4, R_0, minimal, all).

We will use the reduction pair processor with usable rules [Kop12, Thm. 7.44].  (P_4, R_0) has no usable rules.

It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  d#(/\x.minus(X(x)), Y) >? d#(/\y.X(y), Y) 
  d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) 
  d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) 
  d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) 
  d#(/\x.sin(X(x)), Y) >? d#(/\y.X(y), Y) 

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  d# = \G0y1.3G0(0) + 3G0(y1) + y1G0(y1) 
  minus = \y0.3 + 3y0 
  mul = \y0y1.3 + 2y0 + 3y1 
  pls = \y0y1.3 + y1 + 3y0 
  sin = \y0.3 + 3y0 

Using this interpretation, the requirements translate to:

  [[d#(/\x.minus(_x0(x)), _x1)]] = 18 + 3x1 + 3x1F0(x1) + 9F0(0) + 9F0(x1) > 3F0(0) + 3F0(x1) + x1F0(x1) = [[d#(/\x._x0(x), _x1)]] 
  [[d#(/\x.pls(_x0(x), _x1(x)), _x2)]] = 18 + 3x2 + 3x2F0(x2) + 3F1(0) + 3F1(x2) + 9F0(0) + 9F0(x2) + x2F1(x2) > 3F0(0) + 3F0(x2) + x2F0(x2) = [[d#(/\x._x0(x), _x2)]] 
  [[d#(/\x.pls(_x0(x), _x1(x)), _x2)]] = 18 + 3x2 + 3x2F0(x2) + 3F1(0) + 3F1(x2) + 9F0(0) + 9F0(x2) + x2F1(x2) > 3F1(0) + 3F1(x2) + x2F1(x2) = [[d#(/\x._x1(x), _x2)]] 
  [[d#(/\x.mul(_x0(x), _x1(x)), _x2)]] = 18 + 3x2 + 2x2F0(x2) + 3x2F1(x2) + 6F0(0) + 6F0(x2) + 9F1(0) + 9F1(x2) > 3F0(0) + 3F0(x2) + x2F0(x2) = [[d#(/\x._x0(x), _x2)]] 
  [[d#(/\x.mul(_x0(x), _x1(x)), _x2)]] = 18 + 3x2 + 2x2F0(x2) + 3x2F1(x2) + 6F0(0) + 6F0(x2) + 9F1(0) + 9F1(x2) > 3F1(0) + 3F1(x2) + x2F1(x2) = [[d#(/\x._x1(x), _x2)]] 
  [[d#(/\x.sin(_x0(x)), _x1)]] = 18 + 3x1 + 3x1F0(x1) + 9F0(0) + 9F0(x1) > 3F0(0) + 3F0(x1) + x1F0(x1) = [[d#(/\x._x0(x), _x1)]] 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_4, R_0) by ({}, R_0).  By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed.

As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination.


+++ Citations +++

[Kop11]  C. Kop.  Simplifying Algebraic Functional Systems.  In Proceedings of CAI 2011, volume 6742 of LNCS.  201--215, Springer, 2011.
[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.