Termination proof

1: switching to dependency pairs

din#( der( plus( X , Y ) ) )	→	u21#( din( der( X ) ) , X , Y )
din#( der( plus( X , Y ) ) )	→	din#( der( X ) )
u21#( dout( DX ) , X , Y )	→	u22#( din( der( Y ) ) , X , Y , DX )
u21#( dout( DX ) , X , Y )	→	din#( der( Y ) )
din#( der( times( X , Y ) ) )	→	u31#( din( der( X ) ) , X , Y )
din#( der( times( X , Y ) ) )	→	din#( der( X ) )
u31#( dout( DX ) , X , Y )	→	u32#( din( der( Y ) ) , X , Y , DX )
u31#( dout( DX ) , X , Y )	→	din#( der( Y ) )
din#( der( der( X ) ) )	→	u41#( din( der( X ) ) , X )
din#( der( der( X ) ) )	→	din#( der( X ) )
u41#( dout( DX ) , X )	→	u42#( din( der( DX ) ) , X , DX )
u41#( dout( DX ) , X )	→	din#( der( DX ) )

1.1: dependency graph processor

The dependency pairs are split into 1 component(s).

• The 1st component contains the pair(s)

  u21#( dout( DX ) , X , Y )	→	din#( der( Y ) )
  din#( der( plus( X , Y ) ) )	→	u21#( din( der( X ) ) , X , Y )
  din#( der( plus( X , Y ) ) )	→	din#( der( X ) )
  din#( der( times( X , Y ) ) )	→	u31#( din( der( X ) ) , X , Y )
  u31#( dout( DX ) , X , Y )	→	din#( der( Y ) )
  din#( der( times( X , Y ) ) )	→	din#( der( X ) )
  din#( der( der( X ) ) )	→	u41#( din( der( X ) ) , X )
  u41#( dout( DX ) , X )	→	din#( der( DX ) )
  din#( der( der( X ) ) )	→	din#( der( X ) )

  1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [u31# (x1, x2, x3) ]	=	0
  [u41 (x1, x2) ]	=	2 x1
  [u41# (x1, x2) ]	=	0
  [u21# (x1, x2, x3) ]	=	2 x1
  [u31 (x1, x2, x3) ]	=	2 x1
  [u32 (x1, ..., x4) ]	=	x1
  [times (x1, x2) ]	=	0
  [u42 (x1, x2, x3) ]	=	3 x1 + 3
  [u21 (x1, x2, x3) ]	=	2 x1
  [u22 (x1, ..., x4) ]	=	3 x1 + 3
  [plus (x1, x2) ]	=	0
  [din (x1) ]	=	0
  [din# (x1) ]	=	0
  [dout (x1) ]	=	2
  [der (x1) ]	=	0
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  din#( der( plus( X , Y ) ) )	→	u21#( din( der( X ) ) , X , Y )
  din#( der( plus( X , Y ) ) )	→	din#( der( X ) )
  din#( der( times( X , Y ) ) )	→	u31#( din( der( X ) ) , X , Y )
  u31#( dout( DX ) , X , Y )	→	din#( der( Y ) )
  din#( der( times( X , Y ) ) )	→	din#( der( X ) )
  din#( der( der( X ) ) )	→	u41#( din( der( X ) ) , X )
  u41#( dout( DX ) , X )	→	din#( der( DX ) )
  din#( der( der( X ) ) )	→	din#( der( X ) )

  1.1.1.1: dependency graph processor

  The dependency pairs are split into 1 component(s).

  • The 1st component contains the pair(s)

    din#( der( times( X , Y ) ) )	→	u31#( din( der( X ) ) , X , Y )
    u31#( dout( DX ) , X , Y )	→	din#( der( Y ) )
    din#( der( plus( X , Y ) ) )	→	din#( der( X ) )
    din#( der( times( X , Y ) ) )	→	din#( der( X ) )
    din#( der( der( X ) ) )	→	u41#( din( der( X ) ) , X )
    u41#( dout( DX ) , X )	→	din#( der( DX ) )
    din#( der( der( X ) ) )	→	din#( der( X ) )

    1.1.1.1.1: reduction pair processor

    Using the following reduction pair

    Linear polynomial interpretation over the naturals

    [u31# (x1, x2, x3) ]	=	x1
    [u41 (x1, x2) ]	=	2 x1
    [u41# (x1, x2) ]	=	0
    [u31 (x1, x2, x3) ]	=	3 x1
    [u32 (x1, ..., x4) ]	=	3 x1 + 3 x2
    [times (x1, x2) ]	=	0
    [u42 (x1, x2, x3) ]	=	2 x1 + x2 + 1
    [u21 (x1, x2, x3) ]	=	2 x1
    [u22 (x1, ..., x4) ]	=	3 x1 + x2 + 2
    [din (x1) ]	=	0
    [plus (x1, x2) ]	=	3
    [din# (x1) ]	=	0
    [dout (x1) ]	=	x1 + 2
    [der (x1) ]	=	0
    [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

    one remains with the following pair(s).

    din#( der( times( X , Y ) ) )	→	u31#( din( der( X ) ) , X , Y )
    din#( der( plus( X , Y ) ) )	→	din#( der( X ) )
    din#( der( times( X , Y ) ) )	→	din#( der( X ) )
    din#( der( der( X ) ) )	→	u41#( din( der( X ) ) , X )
    u41#( dout( DX ) , X )	→	din#( der( DX ) )
    din#( der( der( X ) ) )	→	din#( der( X ) )

    1.1.1.1.1.1: dependency graph processor

    The dependency pairs are split into 1 component(s).

    • The 1st component contains the pair(s)

      din#( der( times( X , Y ) ) )	→	din#( der( X ) )
      din#( der( plus( X , Y ) ) )	→	din#( der( X ) )
      din#( der( der( X ) ) )	→	u41#( din( der( X ) ) , X )
      u41#( dout( DX ) , X )	→	din#( der( DX ) )
      din#( der( der( X ) ) )	→	din#( der( X ) )

      1.1.1.1.1.1.1: reduction pair processor

      Using the following reduction pair

      Linear polynomial interpretation over the naturals

      [u41 (x1, x2) ]	=	0
      [u41# (x1, x2) ]	=	2 x1
      [u31 (x1, x2, x3) ]	=	0
      [u32 (x1, ..., x4) ]	=	3 x1
      [times (x1, x2) ]	=	0
      [u42 (x1, x2, x3) ]	=	x1
      [u21 (x1, x2, x3) ]	=	3 x1
      [u22 (x1, ..., x4) ]	=	2 x1 + 2
      [plus (x1, x2) ]	=	0
      [din (x1) ]	=	0
      [din# (x1) ]	=	0
      [dout (x1) ]	=	3
      [der (x1) ]	=	0
      [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

      one remains with the following pair(s).

      din#( der( times( X , Y ) ) )	→	din#( der( X ) )
      din#( der( plus( X , Y ) ) )	→	din#( der( X ) )
      din#( der( der( X ) ) )	→	u41#( din( der( X ) ) , X )
      din#( der( der( X ) ) )	→	din#( der( X ) )

      1.1.1.1.1.1.1.1: dependency graph processor

      The dependency pairs are split into 1 component(s).

      • The 1st component contains the pair(s)

        din#( der( plus( X , Y ) ) )	→	din#( der( X ) )
        din#( der( times( X , Y ) ) )	→	din#( der( X ) )
        din#( der( der( X ) ) )	→	din#( der( X ) )

        1.1.1.1.1.1.1.1.1: reduction pair processor

        Using the following reduction pair

        Linear polynomial interpretation over the naturals

        [u21 (x1, x2, x3) ]	=	0
        [u41 (x1, x2) ]	=	0
        [u22 (x1, ..., x4) ]	=	0
        [plus (x1, x2) ]	=	x1 + 3
        [din (x1) ]	=	2
        [din# (x1) ]	=	2 x1
        [u31 (x1, x2, x3) ]	=	1
        [u32 (x1, ..., x4) ]	=	0
        [times (x1, x2) ]	=	x1 + 3
        [dout (x1) ]	=	0
        [der (x1) ]	=	2 x1
        [u42 (x1, x2, x3) ]	=	0
        [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

        one remains with the following pair(s).

        din#( der( der( X ) ) )

        →

        din#( der( X ) )

        1.1.1.1.1.1.1.1.1.1: reduction pair processor

        Using the following reduction pair

        Linear polynomial interpretation over the naturals

        [u21 (x1, x2, x3) ]	=	2
        [u41 (x1, x2) ]	=	2
        [u22 (x1, ..., x4) ]	=	0
        [din (x1) ]	=	2
        [plus (x1, x2) ]	=	0
        [din# (x1) ]	=	x1
        [u31 (x1, x2, x3) ]	=	x1
        [u32 (x1, ..., x4) ]	=	0
        [dout (x1) ]	=	x1
        [times (x1, x2) ]	=	0
        [der (x1) ]	=	x1 + 1
        [u42 (x1, x2, x3) ]	=	x1
        [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

        one remains with the following pair(s).

        none

        1.1.1.1.1.1.1.1.1.1.1: P is empty

        All dependency pairs have been removed.