Certification Problem

Input (TPDB TRS_Standard/Endrullis_06/labeling)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Forward Instantiation Processor

1.1.1 Forward Instantiation Processor

1.1.1.1 Semantic Labeling Processor

As carrier we take the set {0,1}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 2):

There are 128 ruless (increase limit for explicit display).

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  There are 104 ruless (increase limit for explicit display).

  1.1.1.1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [f#000(x1, x2, x3)]	=	1 + 1 · x1 + 1 · x2 + 1 · x3
  [f001(x1, x2, x3)]	=	1 + 1 · x1 + 1 · x2 + 1 · x3
  [a]	=	1
  [f000(x1, x2, x3)]	=	0
  [f011(x1, x2, x3)]	=	0
  [f100(x1, x2, x3)]	=	0
  [f101(x1, x2, x3)]	=	1 + 1 · x2
  [f010(x1, x2, x3)]	=	0
  [f111(x1, x2, x3)]	=	0
  [f110(x1, x2, x3)]	=	0
  [f#010(x1, x2, x3)]	=	1 · x1
  [f#001(x1, x2, x3)]	=	1 + 1 · x1 + 1 · x2
  [f#011(x1, x2, x3)]	=	1 · x1

  the pairs

  f#000(f001(x0,x1,a),f001(y_0,y_1,a),x3)	→	f#000(f001(y_0,y_1,a),x3,f000(x1,x0,f001(y_0,y_1,a)))	(7)
  f#000(f001(x0,x1,a),f011(y_0,y_1,a),x3)	→	f#000(f011(y_0,y_1,a),x3,f000(x1,x0,f011(y_0,y_1,a)))	(9)
  f#000(f001(x0,x1,a),f101(y_0,y_1,a),x3)	→	f#000(f101(y_0,y_1,a),x3,f000(x1,x0,f101(y_0,y_1,a)))	(11)
  f#000(f101(x0,x1,a),f001(y_0,y_1,a),x3)	→	f#000(f001(y_0,y_1,a),x3,f010(x1,x0,f001(y_0,y_1,a)))	(23)
  f#000(f001(x0,x1,a),f111(y_0,y_1,a),x3)	→	f#000(f111(y_0,y_1,a),x3,f000(x1,x0,f111(y_0,y_1,a)))	(13)
  f#000(f001(x0,f001(y_0,y_1,a),a),x2,x3)	→	f#000(f001(y_0,y_1,a),x0,x2)	(39)
  f#000(f001(x0,f011(y_0,y_1,a),a),x2,x3)	→	f#000(f011(y_0,y_1,a),x0,x2)	(43)
  f#000(f101(x0,x1,a),f011(y_0,y_1,a),x3)	→	f#000(f011(y_0,y_1,a),x3,f010(x1,x0,f011(y_0,y_1,a)))	(25)
  f#000(f101(x0,x1,a),f101(y_0,y_1,a),x3)	→	f#000(f101(y_0,y_1,a),x3,f010(x1,x0,f101(y_0,y_1,a)))	(27)
  f#000(f101(x0,x1,a),f111(y_0,y_1,a),x3)	→	f#000(f111(y_0,y_1,a),x3,f010(x1,x0,f111(y_0,y_1,a)))	(29)
  f#000(f101(x0,f001(y_0,y_1,a),a),x2,x3)	→	f#010(f001(y_0,y_1,a),x0,x2)	(55)
  f#010(f001(x0,f001(y_0,y_1,a),a),x2,x3)	→	f#001(f001(y_0,y_1,a),x0,x2)	(41)
  f#001(f001(x0,x1,a),f001(y_0,y_1,a),x3)	→	f#010(f001(y_0,y_1,a),x3,f000(x1,x0,f001(y_0,y_1,a)))	(8)
  f#010(f001(x0,f011(y_0,y_1,a),a),x2,x3)	→	f#001(f011(y_0,y_1,a),x0,x2)	(45)
  f#001(f011(x0,x1,a),f001(y_0,y_1,a),x3)	→	f#010(f001(y_0,y_1,a),x3,f100(x1,x0,f001(y_0,y_1,a)))	(16)
  f#010(f001(x0,f101(y_0,y_1,a),a),x2,x3)	→	f#001(f101(y_0,y_1,a),x0,x2)	(49)
  f#001(f101(x0,x1,a),f001(y_0,y_1,a),x3)	→	f#010(f001(y_0,y_1,a),x3,f010(x1,x0,f001(y_0,y_1,a)))	(24)
  f#010(f001(x0,f111(y_0,y_1,a),a),x2,x3)	→	f#001(f111(y_0,y_1,a),x0,x2)	(53)
  f#001(f111(x0,x1,a),f001(y_0,y_1,a),x3)	→	f#010(f001(y_0,y_1,a),x3,f110(x1,x0,f001(y_0,y_1,a)))	(32)
  f#010(f001(f001(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#001(f001(y_0,y_1,a),f001(y_2,y_3,a),x2)	(73)
  f#001(f001(x0,f001(y_0,y_1,a),a),x2,x3)	→	f#000(f001(y_0,y_1,a),x0,x2)	(40)
  f#000(f001(x0,f101(y_0,y_1,a),a),x2,x3)	→	f#000(f101(y_0,y_1,a),x0,x2)	(47)
  f#000(f101(x0,f101(y_0,y_1,a),a),x2,x3)	→	f#010(f101(y_0,y_1,a),x0,x2)	(63)
  f#010(f101(x0,f001(y_0,y_1,a),a),x2,x3)	→	f#011(f001(y_0,y_1,a),x0,x2)	(57)
  f#011(f001(x0,f001(y_0,y_1,a),a),x2,x3)	→	f#001(f001(y_0,y_1,a),x0,x2)	(42)
  f#001(f001(x0,x1,a),f101(y_0,y_1,a),x3)	→	f#010(f101(y_0,y_1,a),x3,f000(x1,x0,f101(y_0,y_1,a)))	(12)
  f#010(f101(x0,f101(y_0,y_1,a),a),x2,x3)	→	f#011(f101(y_0,y_1,a),x0,x2)	(65)
  f#011(f101(x0,f001(y_0,y_1,a),a),x2,x3)	→	f#011(f001(y_0,y_1,a),x0,x2)	(58)
  f#011(f001(x0,f011(y_0,y_1,a),a),x2,x3)	→	f#001(f011(y_0,y_1,a),x0,x2)	(46)
  f#001(f011(x0,x1,a),f101(y_0,y_1,a),x3)	→	f#010(f101(y_0,y_1,a),x3,f100(x1,x0,f101(y_0,y_1,a)))	(20)
  f#011(f001(x0,f101(y_0,y_1,a),a),x2,x3)	→	f#001(f101(y_0,y_1,a),x0,x2)	(50)
  f#001(f101(x0,x1,a),f101(y_0,y_1,a),x3)	→	f#010(f101(y_0,y_1,a),x3,f010(x1,x0,f101(y_0,y_1,a)))	(28)
  f#001(f101(x0,f001(y_0,y_1,a),a),x2,x3)	→	f#010(f001(y_0,y_1,a),x0,x2)	(56)
  f#010(f001(f001(y_2,y_3,a),f011(y_0,y_1,a),a),x2,x3)	→	f#001(f011(y_0,y_1,a),f001(y_2,y_3,a),x2)	(77)
  f#010(f001(f001(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#001(f101(y_0,y_1,a),f001(y_2,y_3,a),x2)	(81)
  f#001(f101(x0,f101(y_0,y_1,a),a),x2,x3)	→	f#010(f101(y_0,y_1,a),x0,x2)	(64)
  f#010(f001(f001(y_2,y_3,a),f111(y_0,y_1,a),a),x2,x3)	→	f#001(f111(y_0,y_1,a),f001(y_2,y_3,a),x2)	(85)
  f#010(f001(f011(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#001(f001(y_0,y_1,a),f011(y_2,y_3,a),x2)	(89)
  f#001(f001(x0,f011(y_0,y_1,a),a),x2,x3)	→	f#000(f011(y_0,y_1,a),x0,x2)	(44)
  f#001(f001(x0,f101(y_0,y_1,a),a),x2,x3)	→	f#000(f101(y_0,y_1,a),x0,x2)	(48)
  f#001(f001(x0,f111(y_0,y_1,a),a),x2,x3)	→	f#000(f111(y_0,y_1,a),x0,x2)	(52)
  f#001(f001(f001(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#000(f001(y_0,y_1,a),f001(y_2,y_3,a),x2)	(72)
  f#000(f001(x0,f111(y_0,y_1,a),a),x2,x3)	→	f#000(f111(y_0,y_1,a),x0,x2)	(51)
  f#000(f001(f001(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#000(f001(y_0,y_1,a),f001(y_2,y_3,a),x2)	(71)
  f#000(f001(f001(y_2,y_3,a),f011(y_0,y_1,a),a),x2,x3)	→	f#000(f011(y_0,y_1,a),f001(y_2,y_3,a),x2)	(75)
  f#000(f001(f001(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#000(f101(y_0,y_1,a),f001(y_2,y_3,a),x2)	(79)
  f#000(f001(f001(y_2,y_3,a),f111(y_0,y_1,a),a),x2,x3)	→	f#000(f111(y_0,y_1,a),f001(y_2,y_3,a),x2)	(83)
  f#000(f001(f011(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#000(f001(y_0,y_1,a),f011(y_2,y_3,a),x2)	(87)
  f#000(f001(f011(y_2,y_3,a),f011(y_0,y_1,a),a),x2,x3)	→	f#000(f011(y_0,y_1,a),f011(y_2,y_3,a),x2)	(91)
  f#000(f001(f011(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#000(f101(y_0,y_1,a),f011(y_2,y_3,a),x2)	(95)
  f#000(f001(f011(y_2,y_3,a),f111(y_0,y_1,a),a),x2,x3)	→	f#000(f111(y_0,y_1,a),f011(y_2,y_3,a),x2)	(99)
  f#000(f001(f101(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#000(f001(y_0,y_1,a),f101(y_2,y_3,a),x2)	(103)
  f#000(f001(f101(y_2,y_3,a),f011(y_0,y_1,a),a),x2,x3)	→	f#000(f011(y_0,y_1,a),f101(y_2,y_3,a),x2)	(107)
  f#000(f001(f101(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#000(f101(y_0,y_1,a),f101(y_2,y_3,a),x2)	(111)
  f#000(f001(f101(y_2,y_3,a),f111(y_0,y_1,a),a),x2,x3)	→	f#000(f111(y_0,y_1,a),f101(y_2,y_3,a),x2)	(115)
  f#000(f001(f111(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#000(f001(y_0,y_1,a),f111(y_2,y_3,a),x2)	(119)
  f#000(f001(f111(y_2,y_3,a),f011(y_0,y_1,a),a),x2,x3)	→	f#000(f011(y_0,y_1,a),f111(y_2,y_3,a),x2)	(123)
  f#000(f001(f111(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#000(f101(y_0,y_1,a),f111(y_2,y_3,a),x2)	(127)
  f#000(f001(f111(y_2,y_3,a),f111(y_0,y_1,a),a),x2,x3)	→	f#000(f111(y_0,y_1,a),f111(y_2,y_3,a),x2)	(131)
  f#001(f001(f001(y_2,y_3,a),f011(y_0,y_1,a),a),x2,x3)	→	f#000(f011(y_0,y_1,a),f001(y_2,y_3,a),x2)	(76)
  f#001(f001(f001(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#000(f101(y_0,y_1,a),f001(y_2,y_3,a),x2)	(80)
  f#001(f001(f001(y_2,y_3,a),f111(y_0,y_1,a),a),x2,x3)	→	f#000(f111(y_0,y_1,a),f001(y_2,y_3,a),x2)	(84)
  f#001(f001(f011(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#000(f001(y_0,y_1,a),f011(y_2,y_3,a),x2)	(88)
  f#001(f001(f011(y_2,y_3,a),f011(y_0,y_1,a),a),x2,x3)	→	f#000(f011(y_0,y_1,a),f011(y_2,y_3,a),x2)	(92)
  f#001(f001(f011(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#000(f101(y_0,y_1,a),f011(y_2,y_3,a),x2)	(96)
  f#001(f001(f011(y_2,y_3,a),f111(y_0,y_1,a),a),x2,x3)	→	f#000(f111(y_0,y_1,a),f011(y_2,y_3,a),x2)	(100)
  f#001(f001(f101(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#000(f001(y_0,y_1,a),f101(y_2,y_3,a),x2)	(104)
  f#001(f001(f101(y_2,y_3,a),f011(y_0,y_1,a),a),x2,x3)	→	f#000(f011(y_0,y_1,a),f101(y_2,y_3,a),x2)	(108)
  f#001(f001(f101(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#000(f101(y_0,y_1,a),f101(y_2,y_3,a),x2)	(112)
  f#001(f001(f101(y_2,y_3,a),f111(y_0,y_1,a),a),x2,x3)	→	f#000(f111(y_0,y_1,a),f101(y_2,y_3,a),x2)	(116)
  f#001(f001(f111(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#000(f001(y_0,y_1,a),f111(y_2,y_3,a),x2)	(120)
  f#001(f001(f111(y_2,y_3,a),f011(y_0,y_1,a),a),x2,x3)	→	f#000(f011(y_0,y_1,a),f111(y_2,y_3,a),x2)	(124)
  f#001(f001(f111(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#000(f101(y_0,y_1,a),f111(y_2,y_3,a),x2)	(128)
  f#001(f001(f111(y_2,y_3,a),f111(y_0,y_1,a),a),x2,x3)	→	f#000(f111(y_0,y_1,a),f111(y_2,y_3,a),x2)	(132)
  f#010(f001(f011(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#001(f101(y_0,y_1,a),f011(y_2,y_3,a),x2)	(97)
  f#010(f001(f101(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#001(f001(y_0,y_1,a),f101(y_2,y_3,a),x2)	(105)
  f#010(f001(f101(y_2,y_3,a),f011(y_0,y_1,a),a),x2,x3)	→	f#001(f011(y_0,y_1,a),f101(y_2,y_3,a),x2)	(109)
  f#010(f001(f101(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#001(f101(y_0,y_1,a),f101(y_2,y_3,a),x2)	(113)
  f#010(f001(f101(y_2,y_3,a),f111(y_0,y_1,a),a),x2,x3)	→	f#001(f111(y_0,y_1,a),f101(y_2,y_3,a),x2)	(117)
  f#001(f111(x0,x1,a),f101(y_0,y_1,a),x3)	→	f#010(f101(y_0,y_1,a),x3,f110(x1,x0,f101(y_0,y_1,a)))	(36)
  f#010(f001(f111(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#001(f001(y_0,y_1,a),f111(y_2,y_3,a),x2)	(121)
  f#010(f001(f111(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#001(f101(y_0,y_1,a),f111(y_2,y_3,a),x2)	(129)
  f#011(f001(x0,f111(y_0,y_1,a),a),x2,x3)	→	f#001(f111(y_0,y_1,a),x0,x2)	(54)
  f#011(f001(f001(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#001(f001(y_0,y_1,a),f001(y_2,y_3,a),x2)	(74)
  f#011(f001(f001(y_2,y_3,a),f011(y_0,y_1,a),a),x2,x3)	→	f#001(f011(y_0,y_1,a),f001(y_2,y_3,a),x2)	(78)
  f#011(f001(f001(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#001(f101(y_0,y_1,a),f001(y_2,y_3,a),x2)	(82)
  f#011(f001(f001(y_2,y_3,a),f111(y_0,y_1,a),a),x2,x3)	→	f#001(f111(y_0,y_1,a),f001(y_2,y_3,a),x2)	(86)
  f#011(f001(f011(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#001(f001(y_0,y_1,a),f011(y_2,y_3,a),x2)	(90)
  f#011(f001(f011(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#001(f101(y_0,y_1,a),f011(y_2,y_3,a),x2)	(98)
  f#011(f001(f101(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#001(f001(y_0,y_1,a),f101(y_2,y_3,a),x2)	(106)
  f#011(f001(f101(y_2,y_3,a),f011(y_0,y_1,a),a),x2,x3)	→	f#001(f011(y_0,y_1,a),f101(y_2,y_3,a),x2)	(110)
  f#011(f001(f101(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#001(f101(y_0,y_1,a),f101(y_2,y_3,a),x2)	(114)
  f#011(f001(f101(y_2,y_3,a),f111(y_0,y_1,a),a),x2,x3)	→	f#001(f111(y_0,y_1,a),f101(y_2,y_3,a),x2)	(118)
  f#011(f001(f111(y_2,y_3,a),f001(y_0,y_1,a),a),x2,x3)	→	f#001(f001(y_0,y_1,a),f111(y_2,y_3,a),x2)	(122)
  f#011(f001(f111(y_2,y_3,a),f101(y_0,y_1,a),a),x2,x3)	→	f#001(f101(y_0,y_1,a),f111(y_2,y_3,a),x2)	(130)
  f#011(f101(x0,f101(y_0,y_1,a),a),x2,x3)	→	f#011(f101(y_0,y_1,a),x0,x2)	(66)

  could be deleted.

  1.1.1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    f#000(f011(x0,x1,a),f011(y_0,y_1,a),x3)	→	f#000(f011(y_0,y_1,a),x3,f100(x1,x0,f011(y_0,y_1,a)))	(17)
    f#000(f011(x0,x1,a),f111(y_0,y_1,a),x3)	→	f#000(f111(y_0,y_1,a),x3,f100(x1,x0,f111(y_0,y_1,a)))	(21)
    f#000(f111(x0,x1,a),f011(y_0,y_1,a),x3)	→	f#000(f011(y_0,y_1,a),x3,f110(x1,x0,f011(y_0,y_1,a)))	(33)
    f#000(f111(x0,x1,a),f111(y_0,y_1,a),x3)	→	f#000(f111(y_0,y_1,a),x3,f110(x1,x0,f111(y_0,y_1,a)))	(37)

    1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [f#000(x1, x2, x3)]	=	1 · x2 + 1 · x3
    [f011(x1, x2, x3)]	=	1
    [a]	=	1
    [f100(x1, x2, x3)]	=	1
    [f111(x1, x2, x3)]	=	1 + 1 · x3
    [f110(x1, x2, x3)]	=	0
    [f001(x1, x2, x3)]	=	0
    [f101(x1, x2, x3)]	=	1 · x2
    [f000(x1, x2, x3)]	=	1 + 1 · x2
    [f010(x1, x2, x3)]	=	1 · x2

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

    f#000(f011(x0,x1,a),f111(y_0,y_1,a),x3)	→	f#000(f111(y_0,y_1,a),x3,f100(x1,x0,f111(y_0,y_1,a)))	(21)
    f#000(f111(x0,x1,a),f011(y_0,y_1,a),x3)	→	f#000(f011(y_0,y_1,a),x3,f110(x1,x0,f011(y_0,y_1,a)))	(33)
    f#000(f111(x0,x1,a),f111(y_0,y_1,a),x3)	→	f#000(f111(y_0,y_1,a),x3,f110(x1,x0,f111(y_0,y_1,a)))	(37)

    could be deleted.

    1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [f#000(x1, x2, x3)]	=	1 · x2 + 1 · x3
    [f011(x1, x2, x3)]	=	1
    [a]	=	0
    [f100(x1, x2, x3)]	=	0
    [f001(x1, x2, x3)]	=	0
    [f110(x1, x2, x3)]	=	1 · x1 + 1 · x2
    [f101(x1, x2, x3)]	=	1 · x2
    [f111(x1, x2, x3)]	=	1 · x1 + 1 · x2
    [f000(x1, x2, x3)]	=	1 + 1 · x2
    [f010(x1, x2, x3)]	=	1 · x2

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

    f#000(f011(x0,x1,a),f011(y_0,y_1,a),x3)

    →

    f#000(f011(y_0,y_1,a),x3,f100(x1,x0,f011(y_0,y_1,a)))

    (17)

    could be deleted.

    1.1.1.1.1.1.1.1.1.1 P is empty

    There are no pairs anymore.