Certification Problem

Input (TPDB TRS_Standard/AProVE_04/JFP_Ex31)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

• The 1^st component contains the pair

  top#(ok(x))	→	top#(active(x))	(24)
  top#(mark(x))	→	top#(proper(x))	(22)

  1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [proper(x1)]	=	1 · x1
  [b]	=	0
  [ok(x1)]	=	2 · x1
  [c]	=	0
  [d]	=	0
  [f(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 2 · x3
  [mark(x1)]	=	1 · x1
  [active(x1)]	=	2 · x1
  [m(x1)]	=	2 · x1
  [top#(x1)]	=	1 · x1

  together with the usable rules

  proper(b)	→	ok(b)	(6)
  proper(c)	→	ok(c)	(7)
  proper(d)	→	ok(d)	(8)
  proper(f(x,y,z))	→	f(proper(x),proper(y),proper(z))	(9)
  f(x,y,mark(z))	→	mark(f(x,y,z))	(4)
  f(ok(x),ok(y),ok(z))	→	ok(f(x,y,z))	(10)
  active(f(b,c,x))	→	mark(f(x,x,x))	(1)
  active(f(x,y,z))	→	f(x,y,active(z))	(2)
  active(d)	→	m(b)	(3)
  active(d)	→	mark(c)	(5)

  (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.1.1 Narrowing Processor

  We consider all narrowings of the pair below position 1 to get the following set of pairs

  top#(ok(f(b,c,x0)))	→	top#(mark(f(x0,x0,x0)))	(26)
  top#(ok(f(x0,x1,x2)))	→	top#(f(x0,x1,active(x2)))	(27)
  top#(ok(d))	→	top#(m(b))	(28)
  top#(ok(d))	→	top#(mark(c))	(29)

  1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    top#(mark(x))	→	top#(proper(x))	(22)
    top#(ok(f(b,c,x0)))	→	top#(mark(f(x0,x0,x0)))	(26)
    top#(ok(f(x0,x1,x2)))	→	top#(f(x0,x1,active(x2)))	(27)
    top#(ok(d))	→	top#(mark(c))	(29)

    1.1.1.1.1.1 Narrowing Processor

    We consider all narrowings of the pair below position 1 to get the following set of pairs

    top#(mark(b))	→	top#(ok(b))	(30)
    top#(mark(c))	→	top#(ok(c))	(31)
    top#(mark(d))	→	top#(ok(d))	(32)
    top#(mark(f(x0,x1,x2)))	→	top#(f(proper(x0),proper(x1),proper(x2)))	(33)

    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

      top#(mark(f(x0,x1,x2)))	→	top#(f(proper(x0),proper(x1),proper(x2)))	(33)
      top#(ok(f(b,c,x0)))	→	top#(mark(f(x0,x0,x0)))	(26)
      top#(ok(f(x0,x1,x2)))	→	top#(f(x0,x1,active(x2)))	(27)

      1.1.1.1.1.1.1.1 Semantic Labeling Processor

      The following interpretations form a model of the rules.

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

      [active(x1)]	=	0
      [b]	=	1
      [c]	=	0
      [d]	=	0
      [proper(x1)]	=	1x1
      [f(x1, x2, x3)]	=	0
      [m(x1)]	=	0
      [top#(x1)]	=	0
      [ok(x1)]	=	1x1
      [mark(x1)]	=	0

      We obtain the set of labeled pairs

      top#0(mark0(f000(x0,x1,x2)))	→	top#0(f000(proper0(x0),proper0(x1),proper0(x2)))	(34)
      top#0(ok0(f100(b,c,x0)))	→	top#0(mark0(f000(x0,x0,x0)))	(35)
      top#0(ok0(f101(b,c,x0)))	→	top#0(mark0(f111(x0,x0,x0)))	(36)
      top#0(mark0(f001(x0,x1,x2)))	→	top#0(f001(proper0(x0),proper0(x1),proper1(x2)))	(37)
      top#0(mark0(f010(x0,x1,x2)))	→	top#0(f010(proper0(x0),proper1(x1),proper0(x2)))	(38)
      top#0(mark0(f011(x0,x1,x2)))	→	top#0(f011(proper0(x0),proper1(x1),proper1(x2)))	(39)
      top#0(mark0(f100(x0,x1,x2)))	→	top#0(f100(proper1(x0),proper0(x1),proper0(x2)))	(40)
      top#0(mark0(f101(x0,x1,x2)))	→	top#0(f101(proper1(x0),proper0(x1),proper1(x2)))	(41)
      top#0(mark0(f110(x0,x1,x2)))	→	top#0(f110(proper1(x0),proper1(x1),proper0(x2)))	(42)
      top#0(mark0(f111(x0,x1,x2)))	→	top#0(f111(proper1(x0),proper1(x1),proper1(x2)))	(43)
      top#0(ok0(f000(x0,x1,x2)))	→	top#0(f000(x0,x1,active0(x2)))	(44)
      top#0(ok0(f001(x0,x1,x2)))	→	top#0(f000(x0,x1,active1(x2)))	(45)
      top#0(ok0(f010(x0,x1,x2)))	→	top#0(f010(x0,x1,active0(x2)))	(46)
      top#0(ok0(f011(x0,x1,x2)))	→	top#0(f010(x0,x1,active1(x2)))	(47)
      top#0(ok0(f100(x0,x1,x2)))	→	top#0(f100(x0,x1,active0(x2)))	(48)
      top#0(ok0(f101(x0,x1,x2)))	→	top#0(f100(x0,x1,active1(x2)))	(49)
      top#0(ok0(f110(x0,x1,x2)))	→	top#0(f110(x0,x1,active0(x2)))	(50)
      top#0(ok0(f111(x0,x1,x2)))	→	top#0(f110(x0,x1,active1(x2)))	(51)

      and the set of labeled rules:

      proper1(b)	→	ok1(b)	(52)
      proper0(c)	→	ok0(c)	(53)
      proper0(d)	→	ok0(d)	(54)
      proper0(f000(x,y,z))	→	f000(proper0(x),proper0(y),proper0(z))	(55)
      proper0(f001(x,y,z))	→	f001(proper0(x),proper0(y),proper1(z))	(56)
      proper0(f010(x,y,z))	→	f010(proper0(x),proper1(y),proper0(z))	(57)
      proper0(f011(x,y,z))	→	f011(proper0(x),proper1(y),proper1(z))	(58)
      proper0(f100(x,y,z))	→	f100(proper1(x),proper0(y),proper0(z))	(59)
      proper0(f101(x,y,z))	→	f101(proper1(x),proper0(y),proper1(z))	(60)
      proper0(f110(x,y,z))	→	f110(proper1(x),proper1(y),proper0(z))	(61)
      proper0(f111(x,y,z))	→	f111(proper1(x),proper1(y),proper1(z))	(62)
      f000(x,y,mark0(z))	→	mark0(f000(x,y,z))	(63)
      f000(x,y,mark1(z))	→	mark0(f001(x,y,z))	(64)
      f010(x,y,mark0(z))	→	mark0(f010(x,y,z))	(65)
      f010(x,y,mark1(z))	→	mark0(f011(x,y,z))	(66)
      f100(x,y,mark0(z))	→	mark0(f100(x,y,z))	(67)
      f100(x,y,mark1(z))	→	mark0(f101(x,y,z))	(68)
      f110(x,y,mark0(z))	→	mark0(f110(x,y,z))	(69)
      f110(x,y,mark1(z))	→	mark0(f111(x,y,z))	(70)
      f000(ok0(x),ok0(y),ok0(z))	→	ok0(f000(x,y,z))	(71)
      f001(ok0(x),ok0(y),ok1(z))	→	ok0(f001(x,y,z))	(72)
      f010(ok0(x),ok1(y),ok0(z))	→	ok0(f010(x,y,z))	(73)
      f011(ok0(x),ok1(y),ok1(z))	→	ok0(f011(x,y,z))	(74)
      f100(ok1(x),ok0(y),ok0(z))	→	ok0(f100(x,y,z))	(75)
      f101(ok1(x),ok0(y),ok1(z))	→	ok0(f101(x,y,z))	(76)
      f110(ok1(x),ok1(y),ok0(z))	→	ok0(f110(x,y,z))	(77)
      f111(ok1(x),ok1(y),ok1(z))	→	ok0(f111(x,y,z))	(78)
      active0(f100(b,c,x))	→	mark0(f000(x,x,x))	(79)
      active0(f101(b,c,x))	→	mark0(f111(x,x,x))	(80)
      active0(f000(x,y,z))	→	f000(x,y,active0(z))	(81)
      active0(f001(x,y,z))	→	f000(x,y,active1(z))	(82)
      active0(f010(x,y,z))	→	f010(x,y,active0(z))	(83)
      active0(f011(x,y,z))	→	f010(x,y,active1(z))	(84)
      active0(f100(x,y,z))	→	f100(x,y,active0(z))	(85)
      active0(f101(x,y,z))	→	f100(x,y,active1(z))	(86)
      active0(f110(x,y,z))	→	f110(x,y,active0(z))	(87)
      active0(f111(x,y,z))	→	f110(x,y,active1(z))	(88)
      active0(d)	→	m1(b)	(89)
      active0(d)	→	mark0(c)	(90)

      1.1.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

        top#0(ok0(f100(b,c,x0)))	→	top#0(mark0(f000(x0,x0,x0)))	(35)
        top#0(mark0(f000(x0,x1,x2)))	→	top#0(f000(proper0(x0),proper0(x1),proper0(x2)))	(34)
        top#0(ok0(f101(b,c,x0)))	→	top#0(mark0(f111(x0,x0,x0)))	(36)
        top#0(mark0(f001(x0,x1,x2)))	→	top#0(f001(proper0(x0),proper0(x1),proper1(x2)))	(37)
        top#0(ok0(f000(x0,x1,x2)))	→	top#0(f000(x0,x1,active0(x2)))	(44)
        top#0(ok0(f010(x0,x1,x2)))	→	top#0(f010(x0,x1,active0(x2)))	(46)
        top#0(ok0(f100(x0,x1,x2)))	→	top#0(f100(x0,x1,active0(x2)))	(48)
        top#0(ok0(f110(x0,x1,x2)))	→	top#0(f110(x0,x1,active0(x2)))	(50)
        top#0(mark0(f010(x0,x1,x2)))	→	top#0(f010(proper0(x0),proper1(x1),proper0(x2)))	(38)
        top#0(mark0(f011(x0,x1,x2)))	→	top#0(f011(proper0(x0),proper1(x1),proper1(x2)))	(39)
        top#0(mark0(f100(x0,x1,x2)))	→	top#0(f100(proper1(x0),proper0(x1),proper0(x2)))	(40)
        top#0(mark0(f101(x0,x1,x2)))	→	top#0(f101(proper1(x0),proper0(x1),proper1(x2)))	(41)
        top#0(mark0(f110(x0,x1,x2)))	→	top#0(f110(proper1(x0),proper1(x1),proper0(x2)))	(42)
        top#0(mark0(f111(x0,x1,x2)))	→	top#0(f111(proper1(x0),proper1(x1),proper1(x2)))	(43)

        1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the naturals

        [top#0(x1)]	=	1 · x1
        [ok0(x1)]	=	1 · x1
        [f100(x1, x2, x3)]	=	1 + 1 · x2
        [b]	=	0
        [c]	=	1
        [mark0(x1)]	=	1 · x1
        [f000(x1, x2, x3)]	=	0
        [proper0(x1)]	=	1 · x1
        [f101(x1, x2, x3)]	=	0
        [f111(x1, x2, x3)]	=	0
        [f001(x1, x2, x3)]	=	0
        [proper1(x1)]	=	0
        [active0(x1)]	=	0
        [f010(x1, x2, x3)]	=	0
        [f110(x1, x2, x3)]	=	0
        [f011(x1, x2, x3)]	=	0
        [mark1(x1)]	=	1 · x1
        [d]	=	0
        [ok1(x1)]	=	0
        [active1(x1)]	=	1 · x1
        [m1(x1)]	=	1 + 1 · x1

        together with the usable rules

        f000(x,y,mark0(z))	→	mark0(f000(x,y,z))	(63)
        f000(x,y,mark1(z))	→	mark0(f001(x,y,z))	(64)
        f000(ok0(x),ok0(y),ok0(z))	→	ok0(f000(x,y,z))	(71)
        proper0(c)	→	ok0(c)	(53)
        proper0(d)	→	ok0(d)	(54)
        proper0(f000(x,y,z))	→	f000(proper0(x),proper0(y),proper0(z))	(55)
        proper0(f001(x,y,z))	→	f001(proper0(x),proper0(y),proper1(z))	(56)
        proper0(f010(x,y,z))	→	f010(proper0(x),proper1(y),proper0(z))	(57)
        proper0(f011(x,y,z))	→	f011(proper0(x),proper1(y),proper1(z))	(58)
        proper0(f100(x,y,z))	→	f100(proper1(x),proper0(y),proper0(z))	(59)
        proper0(f101(x,y,z))	→	f101(proper1(x),proper0(y),proper1(z))	(60)
        proper0(f110(x,y,z))	→	f110(proper1(x),proper1(y),proper0(z))	(61)
        proper0(f111(x,y,z))	→	f111(proper1(x),proper1(y),proper1(z))	(62)
        f111(ok1(x),ok1(y),ok1(z))	→	ok0(f111(x,y,z))	(78)
        f001(ok0(x),ok0(y),ok1(z))	→	ok0(f001(x,y,z))	(72)
        f010(x,y,mark0(z))	→	mark0(f010(x,y,z))	(65)
        f010(x,y,mark1(z))	→	mark0(f011(x,y,z))	(66)
        f010(ok0(x),ok1(y),ok0(z))	→	ok0(f010(x,y,z))	(73)
        f100(x,y,mark0(z))	→	mark0(f100(x,y,z))	(67)
        f100(x,y,mark1(z))	→	mark0(f101(x,y,z))	(68)
        f100(ok1(x),ok0(y),ok0(z))	→	ok0(f100(x,y,z))	(75)
        f110(x,y,mark0(z))	→	mark0(f110(x,y,z))	(69)
        f110(x,y,mark1(z))	→	mark0(f111(x,y,z))	(70)
        f110(ok1(x),ok1(y),ok0(z))	→	ok0(f110(x,y,z))	(77)
        f011(ok0(x),ok1(y),ok1(z))	→	ok0(f011(x,y,z))	(74)
        f101(ok1(x),ok0(y),ok1(z))	→	ok0(f101(x,y,z))	(76)

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

        top#0(ok0(f100(b,c,x0)))

        →

        top#0(mark0(f000(x0,x0,x0)))

        (35)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the naturals

        [top#0(x1)]	=	1 · x1
        [mark0(x1)]	=	1
        [f000(x1, x2, x3)]	=	1
        [proper0(x1)]	=	0
        [ok0(x1)]	=	1 · x1
        [f101(x1, x2, x3)]	=	1
        [b]	=	0
        [c]	=	0
        [f111(x1, x2, x3)]	=	0
        [f001(x1, x2, x3)]	=	0
        [proper1(x1)]	=	0
        [active0(x1)]	=	0
        [f010(x1, x2, x3)]	=	1
        [f100(x1, x2, x3)]	=	1
        [f110(x1, x2, x3)]	=	1
        [f011(x1, x2, x3)]	=	0
        [d]	=	0
        [mark1(x1)]	=	1 · x1
        [ok1(x1)]	=	0
        [active1(x1)]	=	1 · x1
        [m1(x1)]	=	1 + 1 · x1

        together with the usable rules

        f000(x,y,mark0(z))	→	mark0(f000(x,y,z))	(63)
        f000(x,y,mark1(z))	→	mark0(f001(x,y,z))	(64)
        f000(ok0(x),ok0(y),ok0(z))	→	ok0(f000(x,y,z))	(71)
        f111(ok1(x),ok1(y),ok1(z))	→	ok0(f111(x,y,z))	(78)
        f001(ok0(x),ok0(y),ok1(z))	→	ok0(f001(x,y,z))	(72)
        f010(x,y,mark0(z))	→	mark0(f010(x,y,z))	(65)
        f010(x,y,mark1(z))	→	mark0(f011(x,y,z))	(66)
        f010(ok0(x),ok1(y),ok0(z))	→	ok0(f010(x,y,z))	(73)
        f100(x,y,mark0(z))	→	mark0(f100(x,y,z))	(67)
        f100(x,y,mark1(z))	→	mark0(f101(x,y,z))	(68)
        f100(ok1(x),ok0(y),ok0(z))	→	ok0(f100(x,y,z))	(75)
        f110(x,y,mark0(z))	→	mark0(f110(x,y,z))	(69)
        f110(x,y,mark1(z))	→	mark0(f111(x,y,z))	(70)
        f110(ok1(x),ok1(y),ok0(z))	→	ok0(f110(x,y,z))	(77)
        f011(ok0(x),ok1(y),ok1(z))	→	ok0(f011(x,y,z))	(74)
        f101(ok1(x),ok0(y),ok1(z))	→	ok0(f101(x,y,z))	(76)

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

        top#0(mark0(f001(x0,x1,x2)))	→	top#0(f001(proper0(x0),proper0(x1),proper1(x2)))	(37)
        top#0(mark0(f011(x0,x1,x2)))	→	top#0(f011(proper0(x0),proper1(x1),proper1(x2)))	(39)
        top#0(mark0(f111(x0,x1,x2)))	→	top#0(f111(proper1(x0),proper1(x1),proper1(x2)))	(43)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the naturals

        [top#0(x1)]	=	1 · x1
        [mark0(x1)]	=	1 · x1
        [f000(x1, x2, x3)]	=	0
        [proper0(x1)]	=	0
        [ok0(x1)]	=	1 · x1
        [f101(x1, x2, x3)]	=	1 + 1 · x1
        [b]	=	1
        [c]	=	0
        [f111(x1, x2, x3)]	=	0
        [active0(x1)]	=	0
        [f010(x1, x2, x3)]	=	0
        [f100(x1, x2, x3)]	=	1 + 1 · x1
        [f110(x1, x2, x3)]	=	0
        [proper1(x1)]	=	1 · x1
        [d]	=	0
        [f001(x1, x2, x3)]	=	0
        [f011(x1, x2, x3)]	=	0
        [mark1(x1)]	=	1 · x1
        [ok1(x1)]	=	1 · x1
        [active1(x1)]	=	1 · x1
        [m1(x1)]	=	1 + 1 · x1

        together with the usable rules

        f000(x,y,mark0(z))	→	mark0(f000(x,y,z))	(63)
        f000(x,y,mark1(z))	→	mark0(f001(x,y,z))	(64)
        f000(ok0(x),ok0(y),ok0(z))	→	ok0(f000(x,y,z))	(71)
        f111(ok1(x),ok1(y),ok1(z))	→	ok0(f111(x,y,z))	(78)
        f010(x,y,mark0(z))	→	mark0(f010(x,y,z))	(65)
        f010(x,y,mark1(z))	→	mark0(f011(x,y,z))	(66)
        f010(ok0(x),ok1(y),ok0(z))	→	ok0(f010(x,y,z))	(73)
        f100(x,y,mark0(z))	→	mark0(f100(x,y,z))	(67)
        f100(x,y,mark1(z))	→	mark0(f101(x,y,z))	(68)
        f100(ok1(x),ok0(y),ok0(z))	→	ok0(f100(x,y,z))	(75)
        f110(x,y,mark0(z))	→	mark0(f110(x,y,z))	(69)
        f110(x,y,mark1(z))	→	mark0(f111(x,y,z))	(70)
        f110(ok1(x),ok1(y),ok0(z))	→	ok0(f110(x,y,z))	(77)
        proper1(b)	→	ok1(b)	(52)
        f101(ok1(x),ok0(y),ok1(z))	→	ok0(f101(x,y,z))	(76)
        f001(ok0(x),ok0(y),ok1(z))	→	ok0(f001(x,y,z))	(72)
        f011(ok0(x),ok1(y),ok1(z))	→	ok0(f011(x,y,z))	(74)

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

        top#0(ok0(f101(b,c,x0)))

        →

        top#0(mark0(f111(x0,x0,x0)))

        (36)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the naturals

        [top#0(x1)]	=	1 · x1
        [mark0(x1)]	=	1
        [f000(x1, x2, x3)]	=	1
        [proper0(x1)]	=	0
        [ok0(x1)]	=	1 · x1
        [active0(x1)]	=	0
        [f010(x1, x2, x3)]	=	1
        [f100(x1, x2, x3)]	=	1
        [f110(x1, x2, x3)]	=	1
        [proper1(x1)]	=	0
        [f101(x1, x2, x3)]	=	0
        [c]	=	0
        [d]	=	0
        [f001(x1, x2, x3)]	=	0
        [f011(x1, x2, x3)]	=	0
        [f111(x1, x2, x3)]	=	0
        [mark1(x1)]	=	1 · x1
        [b]	=	0
        [active1(x1)]	=	1 · x1
        [m1(x1)]	=	1 + 1 · x1
        [ok1(x1)]	=	0

        together with the usable rules

        f000(x,y,mark0(z))	→	mark0(f000(x,y,z))	(63)
        f000(x,y,mark1(z))	→	mark0(f001(x,y,z))	(64)
        f000(ok0(x),ok0(y),ok0(z))	→	ok0(f000(x,y,z))	(71)
        f010(x,y,mark0(z))	→	mark0(f010(x,y,z))	(65)
        f010(x,y,mark1(z))	→	mark0(f011(x,y,z))	(66)
        f010(ok0(x),ok1(y),ok0(z))	→	ok0(f010(x,y,z))	(73)
        f100(x,y,mark0(z))	→	mark0(f100(x,y,z))	(67)
        f100(x,y,mark1(z))	→	mark0(f101(x,y,z))	(68)
        f100(ok1(x),ok0(y),ok0(z))	→	ok0(f100(x,y,z))	(75)
        f110(x,y,mark0(z))	→	mark0(f110(x,y,z))	(69)
        f110(x,y,mark1(z))	→	mark0(f111(x,y,z))	(70)
        f110(ok1(x),ok1(y),ok0(z))	→	ok0(f110(x,y,z))	(77)
        f101(ok1(x),ok0(y),ok1(z))	→	ok0(f101(x,y,z))	(76)

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

        top#0(mark0(f101(x0,x1,x2)))

        →

        top#0(f101(proper1(x0),proper0(x1),proper1(x2)))

        (41)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

        Using the linear polynomial interpretation over the naturals

        [top#0(x1)]	=	1 · x1
        [mark0(x1)]	=	1 + 1 · x1
        [f000(x1, x2, x3)]	=	1 · x3
        [proper0(x1)]	=	1 · x1
        [ok0(x1)]	=	1 · x1
        [active0(x1)]	=	1 · x1
        [f010(x1, x2, x3)]	=	1 + 1 · x3
        [f100(x1, x2, x3)]	=	1 + 1 · x1 + 1 · x3
        [f110(x1, x2, x3)]	=	1 + 1 · x3
        [proper1(x1)]	=	1 · x1
        [c]	=	0
        [d]	=	1
        [f001(x1, x2, x3)]	=	0
        [f011(x1, x2, x3)]	=	1
        [f101(x1, x2, x3)]	=	1 + 1 · x1
        [f111(x1, x2, x3)]	=	1
        [mark1(x1)]	=	1 + 1 · x1
        [b]	=	1
        [active1(x1)]	=	0
        [m1(x1)]	=	1 · x1
        [ok1(x1)]	=	1 · x1

        the pairs

        top#0(mark0(f000(x0,x1,x2)))	→	top#0(f000(proper0(x0),proper0(x1),proper0(x2)))	(34)
        top#0(mark0(f010(x0,x1,x2)))	→	top#0(f010(proper0(x0),proper1(x1),proper0(x2)))	(38)
        top#0(mark0(f100(x0,x1,x2)))	→	top#0(f100(proper1(x0),proper0(x1),proper0(x2)))	(40)
        top#0(mark0(f110(x0,x1,x2)))	→	top#0(f110(proper1(x0),proper1(x1),proper0(x2)))	(42)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the naturals

        [top#0(x1)]	=	1 · x1
        [ok0(x1)]	=	1 + 1 · x1
        [f000(x1, x2, x3)]	=	1 · x1
        [active0(x1)]	=	0
        [f010(x1, x2, x3)]	=	1 · x1
        [f100(x1, x2, x3)]	=	1 · x1
        [f110(x1, x2, x3)]	=	1 · x1
        [b]	=	0
        [c]	=	0
        [mark0(x1)]	=	0
        [f101(x1, x2, x3)]	=	0
        [f111(x1, x2, x3)]	=	0
        [f001(x1, x2, x3)]	=	1 · x1 + 1 · x3
        [active1(x1)]	=	1 · x1
        [f011(x1, x2, x3)]	=	1 · x1 + 1 · x3
        [d]	=	1
        [m1(x1)]	=	1 + 1 · x1
        [mark1(x1)]	=	1 · x1
        [ok1(x1)]	=	1 + 1 · x1

        together with the usable rules

        f000(x,y,mark0(z))	→	mark0(f000(x,y,z))	(63)
        f000(x,y,mark1(z))	→	mark0(f001(x,y,z))	(64)
        f000(ok0(x),ok0(y),ok0(z))	→	ok0(f000(x,y,z))	(71)
        f010(x,y,mark0(z))	→	mark0(f010(x,y,z))	(65)
        f010(x,y,mark1(z))	→	mark0(f011(x,y,z))	(66)
        f010(ok0(x),ok1(y),ok0(z))	→	ok0(f010(x,y,z))	(73)
        f100(x,y,mark0(z))	→	mark0(f100(x,y,z))	(67)
        f100(x,y,mark1(z))	→	mark0(f101(x,y,z))	(68)
        f100(ok1(x),ok0(y),ok0(z))	→	ok0(f100(x,y,z))	(75)
        f110(x,y,mark0(z))	→	mark0(f110(x,y,z))	(69)
        f110(x,y,mark1(z))	→	mark0(f111(x,y,z))	(70)
        f110(ok1(x),ok1(y),ok0(z))	→	ok0(f110(x,y,z))	(77)

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

        top#0(ok0(f000(x0,x1,x2)))	→	top#0(f000(x0,x1,active0(x2)))	(44)
        top#0(ok0(f010(x0,x1,x2)))	→	top#0(f010(x0,x1,active0(x2)))	(46)
        top#0(ok0(f100(x0,x1,x2)))	→	top#0(f100(x0,x1,active0(x2)))	(48)
        top#0(ok0(f110(x0,x1,x2)))	→	top#0(f110(x0,x1,active0(x2)))	(50)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 P is empty

        There are no pairs anymore.

• The 2^nd component contains the pair

  active#(f(x,y,z))

  →

  active#(z)

  (15)

  1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [f(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 1 · x3
  [active#(x1)]	=	1 · x1

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

  1.1.2.1 Size-Change Termination

  Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

  active#(f(x,y,z))	→	active#(z)	(15)
  1	>	1

  As there is no critical graph in the transitive closure, there are no infinite chains.

• The 3^rd component contains the pair

  proper#(f(x,y,z))	→	proper#(y)	(19)
  proper#(f(x,y,z))	→	proper#(x)	(18)
  proper#(f(x,y,z))	→	proper#(z)	(20)

  1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [f(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 1 · x3
  [proper#(x1)]	=	1 · x1

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

  1.1.3.1 Size-Change Termination

  Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

  proper#(f(x,y,z))	→	proper#(y)	(19)
  1	>	1
  proper#(f(x,y,z))	→	proper#(x)	(18)
  1	>	1
  proper#(f(x,y,z))	→	proper#(z)	(20)
  1	>	1

  As there is no critical graph in the transitive closure, there are no infinite chains.

• The 4^th component contains the pair

  f#(ok(x),ok(y),ok(z))	→	f#(x,y,z)	(21)
  f#(x,y,mark(z))	→	f#(x,y,z)	(16)

  1.1.4 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [ok(x1)]	=	1 · x1
  [mark(x1)]	=	1 · x1
  [f#(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 1 · x3

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

  1.1.4.1 Size-Change Termination

  Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

  f#(ok(x),ok(y),ok(z))	→	f#(x,y,z)	(21)
  1	>	1
  2	>	2
  3	>	3
  f#(x,y,mark(z))	→	f#(x,y,z)	(16)
  1	≥	1
  2	≥	2
  3	>	3

  As there is no critical graph in the transitive closure, there are no infinite chains.