Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

intersect'ii'in#( Xs , cons( X0 , Ys ) ) → u'1'1#( intersect'ii'in( Xs , Ys ) )

intersect'ii'in#( Xs , cons( X0 , Ys ) ) → intersect'ii'in#( Xs , Ys )

intersect'ii'in#( cons( X0 , Xs ) , Ys ) → u'2'1#( intersect'ii'in( Xs , Ys ) )

intersect'ii'in#( cons( X0 , Xs ) , Ys ) → intersect'ii'in#( Xs , Ys )

reduce'ii'in#( sequent( cons( if( A , B ) , Fs ) , Gs ) , NF ) → u'3'1#( reduce'ii'in( sequent( cons( x'2b( x'2d( B ) , A ) , Fs ) , Gs ) , NF ) )

reduce'ii'in#( sequent( cons( if( A , B ) , Fs ) , Gs ) , NF ) → reduce'ii'in#( sequent( cons( x'2b( x'2d( B ) , A ) , Fs ) , Gs ) , NF )

reduce'ii'in#( sequent( cons( iff( A , B ) , Fs ) , Gs ) , NF ) → u'4'1#( reduce'ii'in( sequent( cons( x'2a( if( A , B ) , if( B , A ) ) , Fs ) , Gs ) , NF ) )

reduce'ii'in#( sequent( cons( iff( A , B ) , Fs ) , Gs ) , NF ) → reduce'ii'in#( sequent( cons( x'2a( if( A , B ) , if( B , A ) ) , Fs ) , Gs ) , NF )

reduce'ii'in#( sequent( cons( x'2a( F1 , F2 ) , Fs ) , Gs ) , NF ) → u'5'1#( reduce'ii'in( sequent( cons( F1 , cons( F2 , Fs ) ) , Gs ) , NF ) )

reduce'ii'in#( sequent( cons( x'2a( F1 , F2 ) , Fs ) , Gs ) , NF ) → reduce'ii'in#( sequent( cons( F1 , cons( F2 , Fs ) ) , Gs ) , NF )

reduce'ii'in#( sequent( cons( x'2b( F1 , F2 ) , Fs ) , Gs ) , NF ) → u'6'1#( reduce'ii'in( sequent( cons( F1 , Fs ) , Gs ) , NF ) , F2 , Fs , Gs , NF )

reduce'ii'in#( sequent( cons( x'2b( F1 , F2 ) , Fs ) , Gs ) , NF ) → reduce'ii'in#( sequent( cons( F1 , Fs ) , Gs ) , NF )

u'6'1#( reduce'ii'out , F2 , Fs , Gs , NF ) → u'6'2#( reduce'ii'in( sequent( cons( F2 , Fs ) , Gs ) , NF ) )

u'6'1#( reduce'ii'out , F2 , Fs , Gs , NF ) → reduce'ii'in#( sequent( cons( F2 , Fs ) , Gs ) , NF )

reduce'ii'in#( sequent( cons( x'2d( F1 ) , Fs ) , Gs ) , NF ) → u'7'1#( reduce'ii'in( sequent( Fs , cons( F1 , Gs ) ) , NF ) )

reduce'ii'in#( sequent( cons( x'2d( F1 ) , Fs ) , Gs ) , NF ) → reduce'ii'in#( sequent( Fs , cons( F1 , Gs ) ) , NF )

reduce'ii'in#( sequent( Fs , cons( if( A , B ) , Gs ) ) , NF ) → u'8'1#( reduce'ii'in( sequent( Fs , cons( x'2b( x'2d( B ) , A ) , Gs ) ) , NF ) )

reduce'ii'in#( sequent( Fs , cons( if( A , B ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( Fs , cons( x'2b( x'2d( B ) , A ) , Gs ) ) , NF )

reduce'ii'in#( sequent( Fs , cons( iff( A , B ) , Gs ) ) , NF ) → u'9'1#( reduce'ii'in( sequent( Fs , cons( x'2a( if( A , B ) , if( B , A ) ) , Gs ) ) , NF ) )

reduce'ii'in#( sequent( Fs , cons( iff( A , B ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( Fs , cons( x'2a( if( A , B ) , if( B , A ) ) , Gs ) ) , NF )

reduce'ii'in#( sequent( cons( p( V ) , Fs ) , Gs ) , sequent( Left , Right ) ) → u'10'1#( reduce'ii'in( sequent( Fs , Gs ) , sequent( cons( p( V ) , Left ) , Right ) ) )

reduce'ii'in#( sequent( cons( p( V ) , Fs ) , Gs ) , sequent( Left , Right ) ) → reduce'ii'in#( sequent( Fs , Gs ) , sequent( cons( p( V ) , Left ) , Right ) )

reduce'ii'in#( sequent( Fs , cons( x'2b( G1 , G2 ) , Gs ) ) , NF ) → u'11'1#( reduce'ii'in( sequent( Fs , cons( G1 , cons( G2 , Gs ) ) ) , NF ) )

reduce'ii'in#( sequent( Fs , cons( x'2b( G1 , G2 ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( Fs , cons( G1 , cons( G2 , Gs ) ) ) , NF )

reduce'ii'in#( sequent( Fs , cons( x'2a( G1 , G2 ) , Gs ) ) , NF ) → u'12'1#( reduce'ii'in( sequent( Fs , cons( G1 , Gs ) ) , NF ) , Fs , G2 , Gs , NF )

reduce'ii'in#( sequent( Fs , cons( x'2a( G1 , G2 ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( Fs , cons( G1 , Gs ) ) , NF )

u'12'1#( reduce'ii'out , Fs , G2 , Gs , NF ) → u'12'2#( reduce'ii'in( sequent( Fs , cons( G2 , Gs ) ) , NF ) )

u'12'1#( reduce'ii'out , Fs , G2 , Gs , NF ) → reduce'ii'in#( sequent( Fs , cons( G2 , Gs ) ) , NF )

reduce'ii'in#( sequent( Fs , cons( x'2d( G1 ) , Gs ) ) , NF ) → u'13'1#( reduce'ii'in( sequent( cons( G1 , Fs ) , Gs ) , NF ) )

reduce'ii'in#( sequent( Fs , cons( x'2d( G1 ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( cons( G1 , Fs ) , Gs ) , NF )

reduce'ii'in#( sequent( nil , cons( p( V ) , Gs ) ) , sequent( Left , Right ) ) → u'14'1#( reduce'ii'in( sequent( nil , Gs ) , sequent( Left , cons( p( V ) , Right ) ) ) )

reduce'ii'in#( sequent( nil , cons( p( V ) , Gs ) ) , sequent( Left , Right ) ) → reduce'ii'in#( sequent( nil , Gs ) , sequent( Left , cons( p( V ) , Right ) ) )

reduce'ii'in#( sequent( nil , nil ) , sequent( F1 , F2 ) ) → u'15'1#( intersect'ii'in( F1 , F2 ) )

reduce'ii'in#( sequent( nil , nil ) , sequent( F1 , F2 ) ) → intersect'ii'in#( F1 , F2 )

tautology'i'in#( F ) → u'16'1#( reduce'ii'in( sequent( nil , cons( F , nil ) ) , sequent( nil , nil ) ) )

tautology'i'in#( F ) → reduce'ii'in#( sequent( nil , cons( F , nil ) ) , sequent( nil , nil ) )

1.1: dependency graph processor

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

The 1st component contains the pair(s)

reduce'ii'in#( sequent( cons( x'2b( F1 , F2 ) , Fs ) , Gs ) , NF ) → u'6'1#( reduce'ii'in( sequent( cons( F1 , Fs ) , Gs ) , NF ) , F2 , Fs , Gs , NF )

u'6'1#( reduce'ii'out , F2 , Fs , Gs , NF ) → reduce'ii'in#( sequent( cons( F2 , Fs ) , Gs ) , NF )

reduce'ii'in#( sequent( cons( if( A , B ) , Fs ) , Gs ) , NF ) → reduce'ii'in#( sequent( cons( x'2b( x'2d( B ) , A ) , Fs ) , Gs ) , NF )

reduce'ii'in#( sequent( cons( x'2b( F1 , F2 ) , Fs ) , Gs ) , NF ) → reduce'ii'in#( sequent( cons( F1 , Fs ) , Gs ) , NF )

reduce'ii'in#( sequent( cons( iff( A , B ) , Fs ) , Gs ) , NF ) → reduce'ii'in#( sequent( cons( x'2a( if( A , B ) , if( B , A ) ) , Fs ) , Gs ) , NF )

reduce'ii'in#( sequent( cons( x'2a( F1 , F2 ) , Fs ) , Gs ) , NF ) → reduce'ii'in#( sequent( cons( F1 , cons( F2 , Fs ) ) , Gs ) , NF )

reduce'ii'in#( sequent( cons( x'2d( F1 ) , Fs ) , Gs ) , NF ) → reduce'ii'in#( sequent( Fs , cons( F1 , Gs ) ) , NF )

reduce'ii'in#( sequent( Fs , cons( if( A , B ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( Fs , cons( x'2b( x'2d( B ) , A ) , Gs ) ) , NF )

reduce'ii'in#( sequent( cons( p( V ) , Fs ) , Gs ) , sequent( Left , Right ) ) → reduce'ii'in#( sequent( Fs , Gs ) , sequent( cons( p( V ) , Left ) , Right ) )

reduce'ii'in#( sequent( Fs , cons( iff( A , B ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( Fs , cons( x'2a( if( A , B ) , if( B , A ) ) , Gs ) ) , NF )

reduce'ii'in#( sequent( Fs , cons( x'2a( G1 , G2 ) , Gs ) ) , NF ) → u'12'1#( reduce'ii'in( sequent( Fs , cons( G1 , Gs ) ) , NF ) , Fs , G2 , Gs , NF )

u'12'1#( reduce'ii'out , Fs , G2 , Gs , NF ) → reduce'ii'in#( sequent( Fs , cons( G2 , Gs ) ) , NF )

reduce'ii'in#( sequent( Fs , cons( x'2b( G1 , G2 ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( Fs , cons( G1 , cons( G2 , Gs ) ) ) , NF )

reduce'ii'in#( sequent( Fs , cons( x'2a( G1 , G2 ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( Fs , cons( G1 , Gs ) ) , NF )

reduce'ii'in#( sequent( Fs , cons( x'2d( G1 ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( cons( G1 , Fs ) , Gs ) , NF )

reduce'ii'in#( sequent( nil , cons( p( V ) , Gs ) ) , sequent( Left , Right ) ) → reduce'ii'in#( sequent( nil , Gs ) , sequent( Left , cons( p( V ) , Right ) ) )

1.1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals

[u'13'1 (x₁) ] = 0

[u'6'2 (x₁) ] = 0

[u'7'1 (x₁) ] = 0

[reduce'ii'in# (x₁, x₂) ] = 2 x₁ + x₂

[u'15'1 (x₁) ] = 0

[u'5'1 (x₁) ] = 0

[intersect'ii'in (x₁, x₂) ] = 0

[x'2a (x₁, x₂) ] = x₁ + x₂

[u'12'1# (x₁, ..., x₅) ] = 2 x₁ + 2 x₂ + 2 x₃ + x₄

[u'11'1 (x₁) ] = 0

[u'6'1 (x₁, ..., x₅) ] = 0

[u'1'1 (x₁) ] = 0

[cons (x₁, x₂) ] = x₁ + x₂

[u'12'2 (x₁) ] = 0

[u'12'1 (x₁, ..., x₅) ] = 0

[iff (x₁, x₂) ] = 3 x₁ + 3 x₂ + 3

[if (x₁, x₂) ] = x₁ + 2 x₂

[u'8'1 (x₁) ] = 0

[x'2d (x₁) ] = 2 x₁

[sequent (x₁, x₂) ] = x₁ + x₂

[u'4'1 (x₁) ] = 0

[u'10'1 (x₁) ] = 0

[intersect'ii'out] = 0

[u'3'1 (x₁) ] = 0

[p (x₁) ] = 3

[tautology'i'in (x₁) ] = x₁ + 2

[u'2'1 (x₁) ] = 0

[nil] = 0

[reduce'ii'in (x₁, x₂) ] = 0

[reduce'ii'out] = 0

[tautology'i'out] = 0

[x'2b (x₁, x₂) ] = x₁ + x₂

[u'6'1# (x₁, ..., x₅) ] = 2 x₁ + 2 x₂ + 2 x₃ + x₄

[u'14'1 (x₁) ] = 0

[u'16'1 (x₁) ] = 1

[u'9'1 (x₁) ] = 0

[f(x₁, ..., x_n)] = x₁ + ... + x_n + 1 for all other symbols f of arity n

one remains with the following pair(s).

reduce'ii'in#( sequent( cons( x'2b( F1 , F2 ) , Fs ) , Gs ) , NF ) → u'6'1#( reduce'ii'in( sequent( cons( F1 , Fs ) , Gs ) , NF ) , F2 , Fs , Gs , NF )

u'6'1#( reduce'ii'out , F2 , Fs , Gs , NF ) → reduce'ii'in#( sequent( cons( F2 , Fs ) , Gs ) , NF )

reduce'ii'in#( sequent( cons( if( A , B ) , Fs ) , Gs ) , NF ) → reduce'ii'in#( sequent( cons( x'2b( x'2d( B ) , A ) , Fs ) , Gs ) , NF )

reduce'ii'in#( sequent( cons( x'2b( F1 , F2 ) , Fs ) , Gs ) , NF ) → reduce'ii'in#( sequent( cons( F1 , Fs ) , Gs ) , NF )

reduce'ii'in#( sequent( cons( x'2a( F1 , F2 ) , Fs ) , Gs ) , NF ) → reduce'ii'in#( sequent( cons( F1 , cons( F2 , Fs ) ) , Gs ) , NF )

reduce'ii'in#( sequent( cons( x'2d( F1 ) , Fs ) , Gs ) , NF ) → reduce'ii'in#( sequent( Fs , cons( F1 , Gs ) ) , NF )

reduce'ii'in#( sequent( Fs , cons( if( A , B ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( Fs , cons( x'2b( x'2d( B ) , A ) , Gs ) ) , NF )

reduce'ii'in#( sequent( Fs , cons( x'2a( G1 , G2 ) , Gs ) ) , NF ) → u'12'1#( reduce'ii'in( sequent( Fs , cons( G1 , Gs ) ) , NF ) , Fs , G2 , Gs , NF )

u'12'1#( reduce'ii'out , Fs , G2 , Gs , NF ) → reduce'ii'in#( sequent( Fs , cons( G2 , Gs ) ) , NF )

reduce'ii'in#( sequent( Fs , cons( x'2b( G1 , G2 ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( Fs , cons( G1 , cons( G2 , Gs ) ) ) , NF )

reduce'ii'in#( sequent( Fs , cons( x'2a( G1 , G2 ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( Fs , cons( G1 , Gs ) ) , NF )

reduce'ii'in#( sequent( Fs , cons( x'2d( G1 ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( cons( G1 , Fs ) , Gs ) , NF )

1.1.1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals

[u'13'1 (x₁) ] = 0

[u'6'2 (x₁) ] = 0

[u'7'1 (x₁) ] = 0

[reduce'ii'in# (x₁, x₂) ] = 2 x₁

[u'15'1 (x₁) ] = 0

[u'5'1 (x₁) ] = 0

[x'2a (x₁, x₂) ] = x₁ + x₂ + 3

[u'12'1# (x₁, ..., x₅) ] = 2 x₁ + 2 x₂ + 2 x₃

[intersect'ii'in (x₁, x₂) ] = 0

[u'11'1 (x₁) ] = 0

[u'6'1 (x₁, ..., x₅) ] = 0

[u'1'1 (x₁) ] = 0

[cons (x₁, x₂) ] = x₁ + x₂

[u'12'2 (x₁) ] = 0

[u'12'1 (x₁, ..., x₅) ] = 0

[iff (x₁, x₂) ] = 0

[if (x₁, x₂) ] = 2 x₁ + 2 x₂ + 2

[u'8'1 (x₁) ] = 0

[x'2d (x₁) ] = x₁ + 1

[sequent (x₁, x₂) ] = x₁ + x₂

[u'4'1 (x₁) ] = 0

[u'10'1 (x₁) ] = 0

[intersect'ii'out] = 0

[u'3'1 (x₁) ] = 0

[p (x₁) ] = 0

[tautology'i'in (x₁) ] = 2 x₁

[u'2'1 (x₁) ] = 0

[reduce'ii'in (x₁, x₂) ] = 0

[nil] = 0

[reduce'ii'out] = 0

[tautology'i'out] = 0

[x'2b (x₁, x₂) ] = x₁ + 2 x₂

[u'6'1# (x₁, ..., x₅) ] = 3 x₁ + 2 x₂ + 2 x₃

[u'14'1 (x₁) ] = 0

[u'16'1 (x₁) ] = 0

[u'9'1 (x₁) ] = 0

[f(x₁, ..., x_n)] = x₁ + ... + x_n + 1 for all other symbols f of arity n

one remains with the following pair(s).

1.1.1.1.1: dependency graph processor

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

The 1st component contains the pair(s)

u'6'1#( reduce'ii'out , F2 , Fs , Gs , NF ) → reduce'ii'in#( sequent( cons( F2 , Fs ) , Gs ) , NF )

reduce'ii'in#( sequent( cons( x'2b( F1 , F2 ) , Fs ) , Gs ) , NF ) → u'6'1#( reduce'ii'in( sequent( cons( F1 , Fs ) , Gs ) , NF ) , F2 , Fs , Gs , NF )

reduce'ii'in#( sequent( cons( x'2b( F1 , F2 ) , Fs ) , Gs ) , NF ) → reduce'ii'in#( sequent( cons( F1 , Fs ) , Gs ) , NF )

reduce'ii'in#( sequent( Fs , cons( x'2b( G1 , G2 ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( Fs , cons( G1 , cons( G2 , Gs ) ) ) , NF )

1.1.1.1.1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals

[u'13'1 (x₁) ] = 0

[u'6'2 (x₁) ] = 0

[u'7'1 (x₁) ] = 0

[reduce'ii'in# (x₁, x₂) ] = 2 x₁ + x₂

[u'15'1 (x₁) ] = 0

[u'5'1 (x₁) ] = 0

[x'2a (x₁, x₂) ] = 0

[intersect'ii'in (x₁, x₂) ] = 0

[u'11'1 (x₁) ] = 0

[u'6'1 (x₁, ..., x₅) ] = 0

[u'1'1 (x₁) ] = 0

[cons (x₁, x₂) ] = x₁

[u'12'2 (x₁) ] = 0

[u'12'1 (x₁, ..., x₅) ] = 0

[iff (x₁, x₂) ] = 0

[if (x₁, x₂) ] = 0

[u'8'1 (x₁) ] = 0

[sequent (x₁, x₂) ] = x₁

[x'2d (x₁) ] = 0

[u'4'1 (x₁) ] = 0

[u'10'1 (x₁) ] = 0

[intersect'ii'out] = 0

[u'3'1 (x₁) ] = 0

[p (x₁) ] = 0

[tautology'i'in (x₁) ] = 3 x₁ + 3

[u'2'1 (x₁) ] = 0

[reduce'ii'in (x₁, x₂) ] = 0

[nil] = 0

[reduce'ii'out] = 0

[tautology'i'out] = 0

[u'6'1# (x₁, ..., x₅) ] = 3 x₁ + x₂ + 2

[x'2b (x₁, x₂) ] = x₁ + 2 x₂ + 2

[u'14'1 (x₁) ] = 0

[u'16'1 (x₁) ] = 0

[u'9'1 (x₁) ] = 0

[f(x₁, ..., x_n)] = x₁ + ... + x_n + 1 for all other symbols f of arity n

one remains with the following pair(s).

reduce'ii'in#( sequent( Fs , cons( x'2b( G1 , G2 ) , Gs ) ) , NF ) → reduce'ii'in#( sequent( Fs , cons( G1 , cons( G2 , Gs ) ) ) , NF )

1.1.1.1.1.1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals

[u'13'1 (x₁) ] = 0

[u'6'2 (x₁) ] = 0

[u'7'1 (x₁) ] = x₁

[reduce'ii'in# (x₁, x₂) ] = 2 x₁

[u'15'1 (x₁) ] = 0

[u'11'1 (x₁) ] = x₁

[u'5'1 (x₁) ] = 0

[x'2a (x₁, x₂) ] = 0

[intersect'ii'in (x₁, x₂) ] = 1

[u'6'1 (x₁, ..., x₅) ] = x₁

[u'1'1 (x₁) ] = x₁

[cons (x₁, x₂) ] = 2 x₁

[u'12'2 (x₁) ] = 0

[u'12'1 (x₁, ..., x₅) ] = x₁

[iff (x₁, x₂) ] = 0

[if (x₁, x₂) ] = 0

[u'8'1 (x₁) ] = x₁

[x'2d (x₁) ] = 0

[sequent (x₁, x₂) ] = 2 x₁

[u'4'1 (x₁) ] = x₁

[u'10'1 (x₁) ] = x₁

[intersect'ii'out] = 0

[u'3'1 (x₁) ] = 0

[p (x₁) ] = 0

[tautology'i'in (x₁) ] = 3 x₁ + 2

[u'2'1 (x₁) ] = 0

[reduce'ii'in (x₁, x₂) ] = x₁

[nil] = 0

[reduce'ii'out] = 0

[tautology'i'out] = 1

[x'2b (x₁, x₂) ] = 2 x₁ + 2

[u'14'1 (x₁) ] = 0

[u'16'1 (x₁) ] = 1

[u'9'1 (x₁) ] = x₁

[f(x₁, ..., x_n)] = x₁ + ... + x_n + 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: P is empty

All dependency pairs have been removed.

The 2nd component contains the pair(s)

intersect'ii'in#( cons( X0 , Xs ) , Ys ) → intersect'ii'in#( Xs , Ys )

intersect'ii'in#( Xs , cons( X0 , Ys ) ) → intersect'ii'in#( Xs , Ys )

1.1.2: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals

[u'13'1 (x₁) ] = 1

[u'6'2 (x₁) ] = 1

[u'7'1 (x₁) ] = 1

[u'15'1 (x₁) ] = 0

[u'11'1 (x₁) ] = 2

[u'5'1 (x₁) ] = 0

[x'2a (x₁, x₂) ] = x₁

[intersect'ii'in (x₁, x₂) ] = x₁

[u'6'1 (x₁, ..., x₅) ] = 2 x₁ + x₂ + 1

[u'1'1 (x₁) ] = 1

[cons (x₁, x₂) ] = x₁ + 2 x₂ + 1

[u'12'2 (x₁) ] = 0

[u'12'1 (x₁, ..., x₅) ] = x₁ + x₂

[iff (x₁, x₂) ] = 0

[if (x₁, x₂) ] = 0

[u'8'1 (x₁) ] = 2

[x'2d (x₁) ] = 0

[sequent (x₁, x₂) ] = x₁ + 2 x₂

[u'4'1 (x₁) ] = 1

[u'10'1 (x₁) ] = 0

[intersect'ii'out] = 0

[u'3'1 (x₁) ] = 0

[p (x₁) ] = x₁ + 3

[tautology'i'in (x₁) ] = 2

[u'2'1 (x₁) ] = x₁

[reduce'ii'in (x₁, x₂) ] = x₁

[nil] = 0

[reduce'ii'out] = 0

[tautology'i'out] = 0

[x'2b (x₁, x₂) ] = 0

[u'14'1 (x₁) ] = 3

[u'16'1 (x₁) ] = 1

[u'9'1 (x₁) ] = 0

[intersect'ii'in# (x₁, x₂) ] = x₁ + x₂

[f(x₁, ..., x_n)] = x₁ + ... + x_n + 1 for all other symbols f of arity n

one remains with the following pair(s).

none

1.1.2.1: P is empty

All dependency pairs have been removed.

intersect'ii'in#( Xs , cons( X0 , Ys ) )	→	u'1'1#( intersect'ii'in( Xs , Ys ) )
intersect'ii'in#( Xs , cons( X0 , Ys ) )	→	intersect'ii'in#( Xs , Ys )
intersect'ii'in#( cons( X0 , Xs ) , Ys )	→	u'2'1#( intersect'ii'in( Xs , Ys ) )
intersect'ii'in#( cons( X0 , Xs ) , Ys )	→	intersect'ii'in#( Xs , Ys )
reduce'ii'in#( sequent( cons( if( A , B ) , Fs ) , Gs ) , NF )	→	u'3'1#( reduce'ii'in( sequent( cons( x'2b( x'2d( B ) , A ) , Fs ) , Gs ) , NF ) )
reduce'ii'in#( sequent( cons( if( A , B ) , Fs ) , Gs ) , NF )	→	reduce'ii'in#( sequent( cons( x'2b( x'2d( B ) , A ) , Fs ) , Gs ) , NF )
reduce'ii'in#( sequent( cons( iff( A , B ) , Fs ) , Gs ) , NF )	→	u'4'1#( reduce'ii'in( sequent( cons( x'2a( if( A , B ) , if( B , A ) ) , Fs ) , Gs ) , NF ) )
reduce'ii'in#( sequent( cons( iff( A , B ) , Fs ) , Gs ) , NF )	→	reduce'ii'in#( sequent( cons( x'2a( if( A , B ) , if( B , A ) ) , Fs ) , Gs ) , NF )
reduce'ii'in#( sequent( cons( x'2a( F1 , F2 ) , Fs ) , Gs ) , NF )	→	u'5'1#( reduce'ii'in( sequent( cons( F1 , cons( F2 , Fs ) ) , Gs ) , NF ) )
reduce'ii'in#( sequent( cons( x'2a( F1 , F2 ) , Fs ) , Gs ) , NF )	→	reduce'ii'in#( sequent( cons( F1 , cons( F2 , Fs ) ) , Gs ) , NF )
reduce'ii'in#( sequent( cons( x'2b( F1 , F2 ) , Fs ) , Gs ) , NF )	→	u'6'1#( reduce'ii'in( sequent( cons( F1 , Fs ) , Gs ) , NF ) , F2 , Fs , Gs , NF )
reduce'ii'in#( sequent( cons( x'2b( F1 , F2 ) , Fs ) , Gs ) , NF )	→	reduce'ii'in#( sequent( cons( F1 , Fs ) , Gs ) , NF )
u'6'1#( reduce'ii'out , F2 , Fs , Gs , NF )	→	u'6'2#( reduce'ii'in( sequent( cons( F2 , Fs ) , Gs ) , NF ) )
u'6'1#( reduce'ii'out , F2 , Fs , Gs , NF )	→	reduce'ii'in#( sequent( cons( F2 , Fs ) , Gs ) , NF )
reduce'ii'in#( sequent( cons( x'2d( F1 ) , Fs ) , Gs ) , NF )	→	u'7'1#( reduce'ii'in( sequent( Fs , cons( F1 , Gs ) ) , NF ) )
reduce'ii'in#( sequent( cons( x'2d( F1 ) , Fs ) , Gs ) , NF )	→	reduce'ii'in#( sequent( Fs , cons( F1 , Gs ) ) , NF )
reduce'ii'in#( sequent( Fs , cons( if( A , B ) , Gs ) ) , NF )	→	u'8'1#( reduce'ii'in( sequent( Fs , cons( x'2b( x'2d( B ) , A ) , Gs ) ) , NF ) )
reduce'ii'in#( sequent( Fs , cons( if( A , B ) , Gs ) ) , NF )	→	reduce'ii'in#( sequent( Fs , cons( x'2b( x'2d( B ) , A ) , Gs ) ) , NF )
reduce'ii'in#( sequent( Fs , cons( iff( A , B ) , Gs ) ) , NF )	→	u'9'1#( reduce'ii'in( sequent( Fs , cons( x'2a( if( A , B ) , if( B , A ) ) , Gs ) ) , NF ) )
reduce'ii'in#( sequent( Fs , cons( iff( A , B ) , Gs ) ) , NF )	→	reduce'ii'in#( sequent( Fs , cons( x'2a( if( A , B ) , if( B , A ) ) , Gs ) ) , NF )
reduce'ii'in#( sequent( cons( p( V ) , Fs ) , Gs ) , sequent( Left , Right ) )	→	u'10'1#( reduce'ii'in( sequent( Fs , Gs ) , sequent( cons( p( V ) , Left ) , Right ) ) )
reduce'ii'in#( sequent( cons( p( V ) , Fs ) , Gs ) , sequent( Left , Right ) )	→	reduce'ii'in#( sequent( Fs , Gs ) , sequent( cons( p( V ) , Left ) , Right ) )
reduce'ii'in#( sequent( Fs , cons( x'2b( G1 , G2 ) , Gs ) ) , NF )	→	u'11'1#( reduce'ii'in( sequent( Fs , cons( G1 , cons( G2 , Gs ) ) ) , NF ) )
reduce'ii'in#( sequent( Fs , cons( x'2b( G1 , G2 ) , Gs ) ) , NF )	→	reduce'ii'in#( sequent( Fs , cons( G1 , cons( G2 , Gs ) ) ) , NF )
reduce'ii'in#( sequent( Fs , cons( x'2a( G1 , G2 ) , Gs ) ) , NF )	→	u'12'1#( reduce'ii'in( sequent( Fs , cons( G1 , Gs ) ) , NF ) , Fs , G2 , Gs , NF )
reduce'ii'in#( sequent( Fs , cons( x'2a( G1 , G2 ) , Gs ) ) , NF )	→	reduce'ii'in#( sequent( Fs , cons( G1 , Gs ) ) , NF )
u'12'1#( reduce'ii'out , Fs , G2 , Gs , NF )	→	u'12'2#( reduce'ii'in( sequent( Fs , cons( G2 , Gs ) ) , NF ) )
u'12'1#( reduce'ii'out , Fs , G2 , Gs , NF )	→	reduce'ii'in#( sequent( Fs , cons( G2 , Gs ) ) , NF )
reduce'ii'in#( sequent( Fs , cons( x'2d( G1 ) , Gs ) ) , NF )	→	u'13'1#( reduce'ii'in( sequent( cons( G1 , Fs ) , Gs ) , NF ) )
reduce'ii'in#( sequent( Fs , cons( x'2d( G1 ) , Gs ) ) , NF )	→	reduce'ii'in#( sequent( cons( G1 , Fs ) , Gs ) , NF )
reduce'ii'in#( sequent( nil , cons( p( V ) , Gs ) ) , sequent( Left , Right ) )	→	u'14'1#( reduce'ii'in( sequent( nil , Gs ) , sequent( Left , cons( p( V ) , Right ) ) ) )
reduce'ii'in#( sequent( nil , cons( p( V ) , Gs ) ) , sequent( Left , Right ) )	→	reduce'ii'in#( sequent( nil , Gs ) , sequent( Left , cons( p( V ) , Right ) ) )
reduce'ii'in#( sequent( nil , nil ) , sequent( F1 , F2 ) )	→	u'15'1#( intersect'ii'in( F1 , F2 ) )
reduce'ii'in#( sequent( nil , nil ) , sequent( F1 , F2 ) )	→	intersect'ii'in#( F1 , F2 )
tautology'i'in#( F )	→	u'16'1#( reduce'ii'in( sequent( nil , cons( F , nil ) ) , sequent( nil , nil ) ) )
tautology'i'in#( F )	→	reduce'ii'in#( sequent( nil , cons( F , nil ) ) , sequent( nil , nil ) )

[u'13'1 (x₁) ]	=	0
[u'6'2 (x₁) ]	=	0
[u'7'1 (x₁) ]	=	0
[reduce'ii'in# (x₁, x₂) ]	=	2 x₁ + x₂
[u'15'1 (x₁) ]	=	0
[u'5'1 (x₁) ]	=	0
[intersect'ii'in (x₁, x₂) ]	=	0
[x'2a (x₁, x₂) ]	=	x₁ + x₂
[u'12'1# (x₁, ..., x₅) ]	=	2 x₁ + 2 x₂ + 2 x₃ + x₄
[u'11'1 (x₁) ]	=	0
[u'6'1 (x₁, ..., x₅) ]	=	0
[u'1'1 (x₁) ]	=	0
[cons (x₁, x₂) ]	=	x₁ + x₂
[u'12'2 (x₁) ]	=	0
[u'12'1 (x₁, ..., x₅) ]	=	0
[iff (x₁, x₂) ]	=	3 x₁ + 3 x₂ + 3
[if (x₁, x₂) ]	=	x₁ + 2 x₂
[u'8'1 (x₁) ]	=	0
[x'2d (x₁) ]	=	2 x₁
[sequent (x₁, x₂) ]	=	x₁ + x₂
[u'4'1 (x₁) ]	=	0
[u'10'1 (x₁) ]	=	0
[intersect'ii'out]	=	0
[u'3'1 (x₁) ]	=	0
[p (x₁) ]	=	3
[tautology'i'in (x₁) ]	=	x₁ + 2
[u'2'1 (x₁) ]	=	0
[nil]	=	0
[reduce'ii'in (x₁, x₂) ]	=	0
[reduce'ii'out]	=	0
[tautology'i'out]	=	0
[x'2b (x₁, x₂) ]	=	x₁ + x₂
[u'6'1# (x₁, ..., x₅) ]	=	2 x₁ + 2 x₂ + 2 x₃ + x₄
[u'14'1 (x₁) ]	=	0
[u'16'1 (x₁) ]	=	1
[u'9'1 (x₁) ]	=	0
[f(x₁, ..., x_n)]	=	x₁ + ... + x_n + 1	for all other symbols f of arity n