Certification Problem

Input (TPDB TRS_Equational/Mixed_AC/RENAMED-BOOL_nokinds)

The rewrite relation of the following equational TRS is considered.

Associative symbols: _and_, _or_, _xor_

Commutative symbols: _and_, _or_, _xor_

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 AC Dependency Pair Transformation

The following set of (strict) dependency pairs is constructed for the TRS.

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

• The 1^st component contains the pair

  _or_#(_or_(x,y),z)	→	_or_#(y,z)	(59)
  _or_#(_or_(A,B),ext)	→	_or_#(U101(and(isBool(A),isBool(B)),A,B),ext)	(148)
  _or_#(x,y)	→	_or_#(y,x)	(53)
  _or_#(_or_(x,y),z)	→	_or_#(x,_or_(y,z))	(56)

  1.1.1 AC Reduction Pair Processor with Usable Rules

  Using the non-linear polynomial interpretation over the naturals

  [_or_#(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
  [_or_(x1, x2)]	=	2 + 3 · x2 + 3 · x1 + 3 · x1 · x2
  [U101(x1, x2, x3)]	=	2 + 2 · x3 + 2 · x2 + 1 · x2 · x3
  [and(x1, x2)]	=	0
  [isBool(x1)]	=	0
  [U31(x1)]	=	0
  [tt]	=	0
  [false]	=	0
  [true]	=	2
  [_xor_(x1, x2)]	=	1 + 1 · x2 + 1 · x1
  [not_(x1)]	=	0
  [_isEqualTo_(x1, x2)]	=	0
  [isUniversal(x1)]	=	0
  [_implies_(x1, x2)]	=	0
  [_isNotEqualTo_(x1, x2)]	=	0
  [_and_(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
  [U111(x1)]	=	0
  [U11(x1, x2)]	=	1 · x2
  [U121(x1, x2)]	=	1 + 1 · x2
  [U21(x1,...,x4)]	=	1 + 1 · x4 + 1 · x3 + 2 · x2 + 1 · x2 · x4 + 1 · x2 · x3
  [U41(x1, x2)]	=	2 · x2

  together with the usable rules

  _or_(A,B)	→	U101(and(isBool(A),isBool(B)),A,B)	(27)
  _or_(_or_(A,B),ext)	→	_or_(U101(and(isBool(A),isBool(B)),A,B),ext)	(163)
  U31(tt)	→	false	(10)
  U111(tt)	→	false	(3)
  U11(tt,A)	→	A	(2)
  _xor_(false,A)	→	U121(isBool(A),A)	(29)
  _xor_(A,A)	→	U111(isBool(A))	(28)
  _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(165)
  _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(164)
  _and_(false,A)	→	U31(isBool(A))	(20)
  _and_(A,_xor_(B,C))	→	U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)	(19)
  _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(162)
  _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(159)
  _and_(A,A)	→	U11(isBool(A),A)	(18)
  _and_(true,A)	→	U41(isBool(A),A)	(21)
  _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C),ext)	(160)
  _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(161)
  U21(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(9)
  U101(tt,A,B)	→	_xor_(_and_(A,B),_xor_(A,B))	(1)
  U41(tt,A)	→	A	(11)
  U121(tt,A)	→	A	(4)
  _or_(x,y)	→	_or_(y,x)	(47)
  _or_(_or_(x,y),z)	→	_or_(x,_or_(y,z))	(50)
  _xor_(x,y)	→	_xor_(y,x)	(48)
  _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(51)
  _and_(_and_(x,y),z)	→	_and_(x,_and_(y,z))	(49)
  _and_(x,y)	→	_and_(y,x)	(46)

  (w.r.t. the implicit argument filter of the reduction pair), the pair

  _or_#(_or_(x,y),z)

  →

  _or_#(y,z)

  (59)

  could be deleted.

  1.1.1.1 AC Reduction Pair Processor with Usable Rules

  Using the non-linear polynomial interpretation over the naturals

  [_or_#(x1, x2)]	=	2 · x2 + 2 · x1 + 2 · x1 · x2
  [_or_(x1, x2)]	=	2 + 3 · x2 + 3 · x1 + 3 · x1 · x2
  [U101(x1, x2, x3)]	=	1 + 2 · x3 + 2 · x2 + 1 · x1 + 2 · x2 · x3
  [and(x1, x2)]	=	1 · x2
  [isBool(x1)]	=	1 · x1
  [true]	=	1
  [tt]	=	1
  [false]	=	1
  [_xor_(x1, x2)]	=	1 + 1 · x2 + 1 · x1
  [not_(x1)]	=	2 · x1
  [_isEqualTo_(x1, x2)]	=	1 · x2
  [isUniversal(x1)]	=	0
  [_implies_(x1, x2)]	=	2 · x2
  [_isNotEqualTo_(x1, x2)]	=	0
  [_and_(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
  [U31(x1)]	=	1
  [U21(x1,...,x4)]	=	1 + 1 · x4 + 1 · x3 + 2 · x2 + 1 · x2 · x4 + 1 · x2 · x3
  [U41(x1, x2)]	=	1 · x2
  [U11(x1, x2)]	=	1 · x1 · x2
  [U121(x1, x2)]	=	1 · x2
  [U111(x1)]	=	1

  together with the usable rules

  isBool(true)	→	tt	(35)
  isBool(false)	→	tt	(34)
  isBool(_xor_(V1,V2))	→	and(isBool(V1),isBool(V2))	(41)
  isBool(not_(V1))	→	isBool(V1)	(42)
  isBool(_isEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(38)
  isBool(_implies_(V1,V2))	→	and(isBool(V1),isBool(V2))	(37)
  isBool(_isNotEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(39)
  isBool(_or_(V1,V2))	→	and(isBool(V1),isBool(V2))	(40)
  isBool(_and_(V1,V2))	→	and(isBool(V1),isBool(V2))	(36)
  _and_(false,A)	→	U31(isBool(A))	(20)
  _and_(A,_xor_(B,C))	→	U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)	(19)
  _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(162)
  _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(159)
  _and_(A,A)	→	U11(isBool(A),A)	(18)
  _and_(true,A)	→	U41(isBool(A),A)	(21)
  _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C),ext)	(160)
  _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(161)
  U11(tt,A)	→	A	(2)
  U31(tt)	→	false	(10)
  U121(tt,A)	→	A	(4)
  _xor_(false,A)	→	U121(isBool(A),A)	(29)
  _xor_(A,A)	→	U111(isBool(A))	(28)
  _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(165)
  _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(164)
  U21(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(9)
  U41(tt,A)	→	A	(11)
  _or_(A,B)	→	U101(and(isBool(A),isBool(B)),A,B)	(27)
  _or_(_or_(A,B),ext)	→	_or_(U101(and(isBool(A),isBool(B)),A,B),ext)	(163)
  U101(tt,A,B)	→	_xor_(_and_(A,B),_xor_(A,B))	(1)
  and(tt,X)	→	X	(30)
  U111(tt)	→	false	(3)
  _and_(_and_(x,y),z)	→	_and_(x,_and_(y,z))	(49)
  _and_(x,y)	→	_and_(y,x)	(46)
  _xor_(x,y)	→	_xor_(y,x)	(48)
  _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(51)
  _or_(x,y)	→	_or_(y,x)	(47)
  _or_(_or_(x,y),z)	→	_or_(x,_or_(y,z))	(50)

  (w.r.t. the implicit argument filter of the reduction pair), the pair

  _or_#(_or_(A,B),ext)

  →

  _or_#(U101(and(isBool(A),isBool(B)),A,B),ext)

  (148)

  could be deleted.

  1.1.1.1.1 AC Dependency Pair Problem is trivial

  There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.
• The 2^nd component contains the pair

  U21#(tt,A,B,C)	→	_and_#(A,B)	(69)
  _and_#(A,_xor_(B,C))	→	U21#(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)	(81)
  U21#(tt,A,B,C)	→	_and_#(A,C)	(70)
  _and_#(_and_(A,A),ext)	→	_and_#(U11(isBool(A),A),ext)	(132)
  _and_#(_and_(A,_xor_(B,C)),ext)	→	_and_#(U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C),ext)	(135)
  _and_#(_and_(A,_xor_(B,C)),ext)	→	U21#(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)	(136)
  _and_#(_and_(false,A),ext)	→	_and_#(U31(isBool(A)),ext)	(142)
  _and_#(_and_(true,A),ext)	→	_and_#(U41(isBool(A),A),ext)	(145)
  _and_#(_and_(x,y),z)	→	_and_#(y,z)	(58)
  _and_#(x,y)	→	_and_#(y,x)	(52)
  _and_#(_and_(x,y),z)	→	_and_#(x,_and_(y,z))	(55)

  1.1.2 AC Reduction Pair Processor with Usable Rules

  Using the non-linear polynomial interpretation over the naturals

  [_and_#(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
  [_and_(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
  [U11(x1, x2)]	=	1 · x1 · x2
  [isBool(x1)]	=	1
  [_xor_(x1, x2)]	=	1 + 1 · x2 + 1 · x1
  [U21(x1,...,x4)]	=	1 + 1 · x3 + 1 · x2 + 1 · x1 · x4 + 1 · x1 · x2 + 1 · x1 · x2 · x4 + 1 · x1 · x2 · x3
  [and(x1, x2)]	=	1 · x2
  [U21#(x1,...,x4)]	=	1 · x4 + 1 · x3 + 1 · x2 + 1 · x2 · x4 + 1 · x2 · x3
  [tt]	=	1
  [false]	=	0
  [U31(x1)]	=	0
  [true]	=	1
  [U41(x1, x2)]	=	1 · x2
  [not_(x1)]	=	1 + 1 · x1 + 1 · x1 · x1
  [_isEqualTo_(x1, x2)]	=	1 · x1 · x2
  [isUniversal(x1)]	=	0
  [_implies_(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
  [_isNotEqualTo_(x1, x2)]	=	1 · x1 · x2
  [_or_(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
  [U121(x1, x2)]	=	1 · x2
  [U111(x1)]	=	0

  together with the usable rules

  and(tt,X)	→	X	(30)
  isBool(true)	→	tt	(35)
  isBool(false)	→	tt	(34)
  isBool(_xor_(V1,V2))	→	and(isBool(V1),isBool(V2))	(41)
  isBool(not_(V1))	→	isBool(V1)	(42)
  isBool(_isEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(38)
  isBool(_implies_(V1,V2))	→	and(isBool(V1),isBool(V2))	(37)
  isBool(_isNotEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(39)
  isBool(_or_(V1,V2))	→	and(isBool(V1),isBool(V2))	(40)
  isBool(_and_(V1,V2))	→	and(isBool(V1),isBool(V2))	(36)
  U121(tt,A)	→	A	(4)
  U41(tt,A)	→	A	(11)
  _and_(false,A)	→	U31(isBool(A))	(20)
  _and_(A,_xor_(B,C))	→	U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)	(19)
  _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(162)
  _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(159)
  _and_(A,A)	→	U11(isBool(A),A)	(18)
  _and_(true,A)	→	U41(isBool(A),A)	(21)
  _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C),ext)	(160)
  _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(161)
  U11(tt,A)	→	A	(2)
  U21(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(9)
  U31(tt)	→	false	(10)
  _xor_(false,A)	→	U121(isBool(A),A)	(29)
  _xor_(A,A)	→	U111(isBool(A))	(28)
  _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(165)
  _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(164)
  U111(tt)	→	false	(3)
  _and_(_and_(x,y),z)	→	_and_(x,_and_(y,z))	(49)
  _and_(x,y)	→	_and_(y,x)	(46)
  _xor_(x,y)	→	_xor_(y,x)	(48)
  _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(51)

  (w.r.t. the implicit argument filter of the reduction pair), the pairs

  _and_#(_and_(true,A),ext)	→	_and_#(U41(isBool(A),A),ext)	(145)
  _and_#(_and_(A,_xor_(B,C)),ext)	→	U21#(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)	(136)
  _and_#(A,_xor_(B,C))	→	U21#(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)	(81)

  could be deleted.

  1.1.2.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    _and_#(_and_(A,_xor_(B,C)),ext)	→	_and_#(U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C),ext)	(135)
    _and_#(_and_(A,A),ext)	→	_and_#(U11(isBool(A),A),ext)	(132)
    _and_#(_and_(false,A),ext)	→	_and_#(U31(isBool(A)),ext)	(142)
    _and_#(_and_(x,y),z)	→	_and_#(y,z)	(58)
    _and_#(x,y)	→	_and_#(y,x)	(52)
    _and_#(_and_(x,y),z)	→	_and_#(x,_and_(y,z))	(55)

    1.1.2.1.1 AC Reduction Pair Processor with Usable Rules

    Using the non-linear polynomial interpretation over the naturals

    [_and_#(x1, x2)]	=	2 · x2 + 2 · x1 + 2 · x1 · x2
    [_and_(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
    [U11(x1, x2)]	=	1 · x2
    [isBool(x1)]	=	1 · x1
    [_xor_(x1, x2)]	=	1 + 1 · x2 + 1 · x1
    [U21(x1,...,x4)]	=	1 + 1 · x4 + 1 · x3 + 2 · x2 + 1 · x2 · x4 + 1 · x2 · x3
    [and(x1, x2)]	=	1 · x2
    [false]	=	2
    [U31(x1)]	=	2 · x1
    [true]	=	2
    [U41(x1, x2)]	=	1 · x2
    [U121(x1, x2)]	=	1 · x2
    [tt]	=	2
    [not_(x1)]	=	1 · x1
    [_isEqualTo_(x1, x2)]	=	2 + 3 · x2 + 3 · x1 + 3 · x1 · x2
    [isUniversal(x1)]	=	0
    [_implies_(x1, x2)]	=	2 + 3 · x2 + 3 · x1 + 3 · x1 · x2
    [_isNotEqualTo_(x1, x2)]	=	2 + 3 · x2 + 3 · x1 + 3 · x1 · x2
    [_or_(x1, x2)]	=	2 + 3 · x2 + 3 · x1
    [U111(x1)]	=	1 · x1

    together with the usable rules

    _and_(false,A)	→	U31(isBool(A))	(20)
    _and_(A,_xor_(B,C))	→	U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)	(19)
    _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(162)
    _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(159)
    _and_(A,A)	→	U11(isBool(A),A)	(18)
    _and_(true,A)	→	U41(isBool(A),A)	(21)
    _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C),ext)	(160)
    _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(161)
    U121(tt,A)	→	A	(4)
    U11(tt,A)	→	A	(2)
    isBool(true)	→	tt	(35)
    isBool(false)	→	tt	(34)
    isBool(_xor_(V1,V2))	→	and(isBool(V1),isBool(V2))	(41)
    isBool(not_(V1))	→	isBool(V1)	(42)
    isBool(_isEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(38)
    isBool(_implies_(V1,V2))	→	and(isBool(V1),isBool(V2))	(37)
    isBool(_isNotEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(39)
    isBool(_or_(V1,V2))	→	and(isBool(V1),isBool(V2))	(40)
    isBool(_and_(V1,V2))	→	and(isBool(V1),isBool(V2))	(36)
    _xor_(false,A)	→	U121(isBool(A),A)	(29)
    _xor_(A,A)	→	U111(isBool(A))	(28)
    _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(165)
    _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(164)
    U41(tt,A)	→	A	(11)
    U111(tt)	→	false	(3)
    U21(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(9)
    U31(tt)	→	false	(10)
    and(tt,X)	→	X	(30)
    _and_(_and_(x,y),z)	→	_and_(x,_and_(y,z))	(49)
    _and_(x,y)	→	_and_(y,x)	(46)
    _xor_(x,y)	→	_xor_(y,x)	(48)
    _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(51)

    (w.r.t. the implicit argument filter of the reduction pair), the pair

    _and_#(_and_(false,A),ext)

    →

    _and_#(U31(isBool(A)),ext)

    (142)

    could be deleted.

    1.1.2.1.1.1 AC Reduction Pair Processor with Usable Rules

    Using the non-linear polynomial interpretation over the naturals

    [_and_#(x1, x2)]	=	2 · x2 + 2 · x1 + 2 · x1 · x2
    [_and_(x1, x2)]	=	1 + 2 · x2 + 2 · x1 + 2 · x1 · x2
    [U11(x1, x2)]	=	1 + 1 · x2
    [isBool(x1)]	=	1
    [_xor_(x1, x2)]	=	1 + 1 · x2 + 1 · x1
    [U21(x1,...,x4)]	=	3 + 2 · x4 + 2 · x3 + 2 · x2 + 2 · x2 · x4 + 2 · x1 · x2 + 2 · x1 · x2 · x3
    [and(x1, x2)]	=	1 · x1 · x2
    [false]	=	1
    [U121(x1, x2)]	=	1 · x2
    [U111(x1)]	=	1
    [U31(x1)]	=	1
    [true]	=	0
    [U41(x1, x2)]	=	1 + 1 · x2
    [tt]	=	1
    [not_(x1)]	=	0
    [_isEqualTo_(x1, x2)]	=	0
    [isUniversal(x1)]	=	1
    [_implies_(x1, x2)]	=	0
    [_isNotEqualTo_(x1, x2)]	=	0
    [_or_(x1, x2)]	=	0

    together with the usable rules

    _xor_(false,A)	→	U121(isBool(A),A)	(29)
    _xor_(A,A)	→	U111(isBool(A))	(28)
    _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(165)
    _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(164)
    _and_(false,A)	→	U31(isBool(A))	(20)
    _and_(A,_xor_(B,C))	→	U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)	(19)
    _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(162)
    _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(159)
    _and_(A,A)	→	U11(isBool(A),A)	(18)
    _and_(true,A)	→	U41(isBool(A),A)	(21)
    _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C),ext)	(160)
    _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(161)
    U41(tt,A)	→	A	(11)
    U21(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(9)
    U111(tt)	→	false	(3)
    and(tt,X)	→	X	(30)
    U121(tt,A)	→	A	(4)
    isBool(true)	→	tt	(35)
    isBool(false)	→	tt	(34)
    isBool(_xor_(V1,V2))	→	and(isBool(V1),isBool(V2))	(41)
    isBool(not_(V1))	→	isBool(V1)	(42)
    isBool(_isEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(38)
    isBool(_implies_(V1,V2))	→	and(isBool(V1),isBool(V2))	(37)
    isBool(_isNotEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(39)
    isBool(_or_(V1,V2))	→	and(isBool(V1),isBool(V2))	(40)
    isBool(_and_(V1,V2))	→	and(isBool(V1),isBool(V2))	(36)
    U31(tt)	→	false	(10)
    U11(tt,A)	→	A	(2)
    _xor_(x,y)	→	_xor_(y,x)	(48)
    _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(51)
    _and_(_and_(x,y),z)	→	_and_(x,_and_(y,z))	(49)
    _and_(x,y)	→	_and_(y,x)	(46)

    (w.r.t. the implicit argument filter of the reduction pair), the pair

    _and_#(_and_(x,y),z)

    →

    _and_#(y,z)

    (58)

    could be deleted.

    1.1.2.1.1.1.1 AC Reduction Pair Processor with Usable Rules

    Using the non-linear polynomial interpretation over the naturals

    [_and_#(x1, x2)]	=	2 · x2 + 2 · x1 + 1 · x1 · x2
    [_and_(x1, x2)]	=	2 + 2 · x2 + 2 · x1 + 1 · x1 · x2
    [U11(x1, x2)]	=	2 · x2 + 1 · x1
    [isBool(x1)]	=	1
    [_xor_(x1, x2)]	=	2 + 1 · x2 + 1 · x1
    [U21(x1,...,x4)]	=	3 + 2 · x4 + 2 · x3 + 3 · x2 + 3 · x1 + 1 · x2 · x4 + 1 · x2 · x3 + 1 · x1 · x2
    [and(x1, x2)]	=	1 · x1 · x2
    [U121(x1, x2)]	=	2 + 1 · x2
    [tt]	=	1
    [U111(x1)]	=	0
    [false]	=	0
    [U41(x1, x2)]	=	1 · x2
    [U31(x1)]	=	0
    [true]	=	2
    [not_(x1)]	=	0
    [_isEqualTo_(x1, x2)]	=	0
    [isUniversal(x1)]	=	0
    [_implies_(x1, x2)]	=	0
    [_isNotEqualTo_(x1, x2)]	=	0
    [_or_(x1, x2)]	=	0

    together with the usable rules

    U121(tt,A)	→	A	(4)
    U11(tt,A)	→	A	(2)
    and(tt,X)	→	X	(30)
    U111(tt)	→	false	(3)
    U41(tt,A)	→	A	(11)
    U21(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(9)
    _and_(false,A)	→	U31(isBool(A))	(20)
    _and_(A,_xor_(B,C))	→	U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)	(19)
    _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(162)
    _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(159)
    _and_(A,A)	→	U11(isBool(A),A)	(18)
    _and_(true,A)	→	U41(isBool(A),A)	(21)
    _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C),ext)	(160)
    _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(161)
    U31(tt)	→	false	(10)
    _xor_(false,A)	→	U121(isBool(A),A)	(29)
    _xor_(A,A)	→	U111(isBool(A))	(28)
    _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(165)
    _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(164)
    isBool(true)	→	tt	(35)
    isBool(false)	→	tt	(34)
    isBool(_xor_(V1,V2))	→	and(isBool(V1),isBool(V2))	(41)
    isBool(not_(V1))	→	isBool(V1)	(42)
    isBool(_isEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(38)
    isBool(_implies_(V1,V2))	→	and(isBool(V1),isBool(V2))	(37)
    isBool(_isNotEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(39)
    isBool(_or_(V1,V2))	→	and(isBool(V1),isBool(V2))	(40)
    isBool(_and_(V1,V2))	→	and(isBool(V1),isBool(V2))	(36)
    _and_(_and_(x,y),z)	→	_and_(x,_and_(y,z))	(49)
    _and_(x,y)	→	_and_(y,x)	(46)
    _xor_(x,y)	→	_xor_(y,x)	(48)
    _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(51)

    (w.r.t. the implicit argument filter of the reduction pair), the pair

    _and_#(_and_(A,A),ext)

    →

    _and_#(U11(isBool(A),A),ext)

    (132)

    could be deleted.

    1.1.2.1.1.1.1.1 AC Reduction Pair Processor with Usable Rules

    Using the non-linear polynomial interpretation over the naturals

    [_and_#(x1, x2)]	=	2 · x2 + 2 · x1 + 2 · x1 · x2
    [_and_(x1, x2)]	=	1 + 2 · x2 + 2 · x1 + 2 · x1 · x2
    [_xor_(x1, x2)]	=	2 + 1 · x2 + 1 · x1
    [U21(x1,...,x4)]	=	2 + 2 · x4 + 2 · x3 + 3 · x2 + 2 · x1 + 2 · x2 · x4 + 2 · x2 · x3 + 1 · x1 · x2
    [and(x1, x2)]	=	1 · x1 · x2
    [isBool(x1)]	=	1
    [U31(x1)]	=	1 · x1 · x1
    [tt]	=	1
    [false]	=	0
    [true]	=	0
    [not_(x1)]	=	0
    [_isEqualTo_(x1, x2)]	=	0
    [isUniversal(x1)]	=	0
    [_implies_(x1, x2)]	=	0
    [_isNotEqualTo_(x1, x2)]	=	0
    [_or_(x1, x2)]	=	0
    [U11(x1, x2)]	=	1 · x1 · x2
    [U41(x1, x2)]	=	1 · x2
    [U121(x1, x2)]	=	1 · x2
    [U111(x1)]	=	1 + 1 · x1

    together with the usable rules

    U31(tt)	→	false	(10)
    and(tt,X)	→	X	(30)
    U21(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(9)
    isBool(true)	→	tt	(35)
    isBool(false)	→	tt	(34)
    isBool(_xor_(V1,V2))	→	and(isBool(V1),isBool(V2))	(41)
    isBool(not_(V1))	→	isBool(V1)	(42)
    isBool(_isEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(38)
    isBool(_implies_(V1,V2))	→	and(isBool(V1),isBool(V2))	(37)
    isBool(_isNotEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(39)
    isBool(_or_(V1,V2))	→	and(isBool(V1),isBool(V2))	(40)
    isBool(_and_(V1,V2))	→	and(isBool(V1),isBool(V2))	(36)
    U11(tt,A)	→	A	(2)
    _and_(false,A)	→	U31(isBool(A))	(20)
    _and_(A,_xor_(B,C))	→	U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)	(19)
    _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(162)
    _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(159)
    _and_(A,A)	→	U11(isBool(A),A)	(18)
    _and_(true,A)	→	U41(isBool(A),A)	(21)
    _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C),ext)	(160)
    _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(161)
    U41(tt,A)	→	A	(11)
    _xor_(false,A)	→	U121(isBool(A),A)	(29)
    _xor_(A,A)	→	U111(isBool(A))	(28)
    _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(165)
    _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(164)
    U111(tt)	→	false	(3)
    U121(tt,A)	→	A	(4)
    _and_(_and_(x,y),z)	→	_and_(x,_and_(y,z))	(49)
    _and_(x,y)	→	_and_(y,x)	(46)
    _xor_(x,y)	→	_xor_(y,x)	(48)
    _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(51)

    (w.r.t. the implicit argument filter of the reduction pair), the pair

    _and_#(_and_(A,_xor_(B,C)),ext)

    →

    _and_#(U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C),ext)

    (135)

    could be deleted.

    1.1.2.1.1.1.1.1.1 AC Dependency Pair Problem is trivial

    There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.
• The 3^rd component contains the pair

  _xor_#(_xor_(false,A),ext)	→	_xor_#(U121(isBool(A),A),ext)	(156)
  _xor_#(_xor_(A,A),ext)	→	_xor_#(U111(isBool(A)),ext)	(153)
  _xor_#(_xor_(x,y),z)	→	_xor_#(y,z)	(60)
  _xor_#(x,y)	→	_xor_#(y,x)	(54)
  _xor_#(_xor_(x,y),z)	→	_xor_#(x,_xor_(y,z))	(57)

  1.1.3 AC Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [_xor_#(x1, x2)]	=	3 · x1 + 3 · x2
  [_xor_(x1, x2)]	=	3 + 1 · x1 + 1 · x2
  [U111(x1)]	=	3
  [isBool(x1)]	=	1
  [false]	=	3
  [U121(x1, x2)]	=	2 + 1 · x1 + 1 · x2
  [tt]	=	0
  [and(x1, x2)]	=	1 · x2
  [_isEqualTo_(x1, x2)]	=	0
  [isUniversal(x1)]	=	0
  [_implies_(x1, x2)]	=	0
  [_isNotEqualTo_(x1, x2)]	=	0
  [_or_(x1, x2)]	=	0
  [true]	=	0
  [_and_(x1, x2)]	=	0
  [not_(x1)]	=	3 · x1

  together with the usable rules

  U121(tt,A)	→	A	(4)
  U111(tt)	→	false	(3)
  and(tt,X)	→	X	(30)
  isBool(_isEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(38)
  isBool(_implies_(V1,V2))	→	and(isBool(V1),isBool(V2))	(37)
  isBool(_isNotEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(39)
  isBool(_or_(V1,V2))	→	and(isBool(V1),isBool(V2))	(40)
  isBool(true)	→	tt	(35)
  isBool(_and_(V1,V2))	→	and(isBool(V1),isBool(V2))	(36)
  isBool(false)	→	tt	(34)
  isBool(_xor_(V1,V2))	→	and(isBool(V1),isBool(V2))	(41)
  isBool(not_(V1))	→	isBool(V1)	(42)
  _xor_(false,A)	→	U121(isBool(A),A)	(29)
  _xor_(A,A)	→	U111(isBool(A))	(28)
  _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(165)
  _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(164)
  _xor_(x,y)	→	_xor_(y,x)	(48)
  _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(51)

  (w.r.t. the implicit argument filter of the reduction pair), the pairs

  _xor_#(_xor_(x,y),z)	→	_xor_#(y,z)	(60)
  _xor_#(_xor_(false,A),ext)	→	_xor_#(U121(isBool(A),A),ext)	(156)

  could be deleted.

  1.1.3.1 AC Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [_xor_#(x1, x2)]	=	2 · x1 + 2 · x2
  [_xor_(x1, x2)]	=	2 + 1 · x1 + 1 · x2
  [U111(x1)]	=	0
  [isBool(x1)]	=	0
  [_isEqualTo_(x1, x2)]	=	0
  [and(x1, x2)]	=	3
  [isUniversal(x1)]	=	0
  [_implies_(x1, x2)]	=	0
  [_isNotEqualTo_(x1, x2)]	=	0
  [_or_(x1, x2)]	=	0
  [true]	=	0
  [tt]	=	0
  [_and_(x1, x2)]	=	0
  [false]	=	0
  [not_(x1)]	=	3 · x1
  [U121(x1, x2)]	=	1 · x2

  together with the usable rules

  _xor_(false,A)	→	U121(isBool(A),A)	(29)
  _xor_(A,A)	→	U111(isBool(A))	(28)
  _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(165)
  _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(164)
  U121(tt,A)	→	A	(4)
  U111(tt)	→	false	(3)
  _xor_(x,y)	→	_xor_(y,x)	(48)
  _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(51)

  (w.r.t. the implicit argument filter of the reduction pair), the pair

  _xor_#(_xor_(A,A),ext)

  →

  _xor_#(U111(isBool(A)),ext)

  (153)

  could be deleted.

  1.1.3.1.1 AC Dependency Pair Problem is trivial

  There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.
• The 4^th component contains the pair

  isBool#(_and_(V1,V2))	→	isBool#(V2)	(117)
  isBool#(_and_(V1,V2))	→	isBool#(V1)	(116)
  isBool#(_implies_(V1,V2))	→	isBool#(V1)	(119)
  isBool#(_implies_(V1,V2))	→	isBool#(V2)	(120)
  isBool#(_or_(V1,V2))	→	isBool#(V1)	(124)
  isBool#(_or_(V1,V2))	→	isBool#(V2)	(125)
  isBool#(_xor_(V1,V2))	→	isBool#(V1)	(127)
  isBool#(_xor_(V1,V2))	→	isBool#(V2)	(128)
  isBool#(not_(V1))	→	isBool#(V1)	(129)

  1.1.4 AC Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [isBool#(x1)]	=	2 · x1
  [_and_(x1, x2)]	=	3 · x1 + 1 · x2
  [_implies_(x1, x2)]	=	3 · x1 + 3 · x2
  [not_(x1)]	=	3 · x1
  [_or_(x1, x2)]	=	3 · x1 + 1 · x2
  [_xor_(x1, x2)]	=	3 · x1 + 3 · x2

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

  isBool#(_and_(V1,V2))	→	isBool#(V1)	(116)
  isBool#(_implies_(V1,V2))	→	isBool#(V1)	(119)
  isBool#(_implies_(V1,V2))	→	isBool#(V2)	(120)
  isBool#(not_(V1))	→	isBool#(V1)	(129)
  isBool#(_and_(V1,V2))	→	isBool#(V2)	(117)
  isBool#(_or_(V1,V2))	→	isBool#(V1)	(124)
  isBool#(_xor_(V1,V2))	→	isBool#(V2)	(128)
  isBool#(_or_(V1,V2))	→	isBool#(V2)	(125)
  isBool#(_xor_(V1,V2))	→	isBool#(V1)	(127)

  and the rules

  U101(tt,A,B)	→	_xor_(_and_(A,B),_xor_(A,B))	(1)
  U11(tt,A)	→	A	(2)
  U111(tt)	→	false	(3)
  U121(tt,A)	→	A	(4)
  U131(tt,B,U')	→	U132(equal(_isNotEqualTo_(B,true),true),U')	(5)
  U132(tt,U')	→	U'	(6)
  U141(tt,U)	→	U	(7)
  U151(tt,A)	→	_xor_(A,true)	(8)
  U21(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(9)
  U31(tt)	→	false	(10)
  U41(tt,A)	→	A	(11)
  U51(tt,A,B)	→	not_(_xor_(A,_and_(A,B)))	(12)
  U61(tt,U',U)	→	U62(equal(_isNotEqualTo_(U,U'),true))	(13)
  U62(tt)	→	false	(14)
  U71(tt)	→	true	(15)
  U81(tt,U',U)	→	if_then_else_fi(_isEqualTo_(U,U'),false,true)	(16)
  U91(tt)	→	false	(17)
  _and_(A,A)	→	U11(isBool(A),A)	(18)
  _and_(A,_xor_(B,C))	→	U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C)	(19)
  _and_(false,A)	→	U31(isBool(A))	(20)
  _and_(true,A)	→	U41(isBool(A),A)	(21)
  _implies_(A,B)	→	U51(and(isBool(A),isBool(B)),A,B)	(22)
  _isEqualTo_(U,U')	→	U61(and(isS(U'),isS(U)),U',U)	(23)
  _isEqualTo_(U,U)	→	U71(isS(U))	(24)
  _isNotEqualTo_(U,U')	→	U81(and(isS(U'),isS(U)),U',U)	(25)
  _isNotEqualTo_(U,U)	→	U91(isS(U))	(26)
  _or_(A,B)	→	U101(and(isBool(A),isBool(B)),A,B)	(27)
  _xor_(A,A)	→	U111(isBool(A))	(28)
  _xor_(false,A)	→	U121(isBool(A),A)	(29)
  and(tt,X)	→	X	(30)
  equal(X,X)	→	tt	(31)
  if_then_else_fi(B,U,U')	→	U131(and(isBool(B),and(isS(U'),isS(U))),B,U')	(32)
  if_then_else_fi(true,U,U')	→	U141(and(isS(U'),isS(U)),U)	(33)
  isBool(false)	→	tt	(34)
  isBool(true)	→	tt	(35)
  isBool(_and_(V1,V2))	→	and(isBool(V1),isBool(V2))	(36)
  isBool(_implies_(V1,V2))	→	and(isBool(V1),isBool(V2))	(37)
  isBool(_isEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(38)
  isBool(_isNotEqualTo_(V1,V2))	→	and(isUniversal(V1),isUniversal(V2))	(39)
  isBool(_or_(V1,V2))	→	and(isBool(V1),isBool(V2))	(40)
  isBool(_xor_(V1,V2))	→	and(isBool(V1),isBool(V2))	(41)
  isBool(not_(V1))	→	isBool(V1)	(42)
  not_(A)	→	U151(isBool(A),A)	(43)
  not_(false)	→	true	(44)
  not_(true)	→	false	(45)
  _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(159)
  _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C),ext)	(160)
  _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(161)
  _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(162)
  _or_(_or_(A,B),ext)	→	_or_(U101(and(isBool(A),isBool(B)),A,B),ext)	(163)
  _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(164)
  _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(165)

  could be deleted.

  1.1.4.1 AC Dependency Pair Problem is trivial

  There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.