Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/264033)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

1.1 Dependency Pair Transformation

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  1#(1(2(0(2(x1)))))	→	1#(1(0(2(2(x1)))))	(135)
  1#(1(2(0(2(x1)))))	→	2#(1(0(2(x1))))	(137)
  2#(1(2(0(2(x1)))))	→	2#(1(0(x1)))	(157)
  2#(1(2(0(2(x1)))))	→	0#(x1)	(155)
  0#(1(2(0(2(x1)))))	→	2#(1(0(x1)))	(113)
  2#(1(2(0(2(x1)))))	→	2#(1(0(2(x1))))	(153)
  2#(1(2(0(2(x1)))))	→	2#(1(0(2(2(x1)))))	(151)
  2#(1(2(0(2(x1)))))	→	0#(1(2(2(x1))))	(147)
  0#(1(2(0(2(x1)))))	→	0#(x1)	(111)
  0#(1(2(0(2(x1)))))	→	2#(1(0(2(x1))))	(109)
  2#(1(1(0(2(x1)))))	→	0#(1(0(2(x1))))	(143)
  0#(1(2(0(2(x1)))))	→	0#(1(1(2(2(x1)))))	(107)
  0#(1(2(0(2(x1)))))	→	1#(1(2(2(x1))))	(106)
  1#(1(2(0(2(x1)))))	→	0#(x1)	(129)
  0#(1(2(0(2(x1)))))	→	0#(1(0(2(2(x1)))))	(104)
  1#(1(2(0(2(x1)))))	→	2#(1(2(x1)))	(126)
  1#(1(2(0(2(x1)))))	→	0#(1(2(2(x1))))	(121)

  1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the

  prec(1#)	=	0		stat(1#)	=	lex
  prec(2#)	=	0		stat(2#)	=	lex
  prec(0#)	=	0		stat(0#)	=	lex
  prec(1)	=	0		stat(1)	=	lex
  prec(0)	=	0		stat(0)	=	lex
  prec(2)	=	0		stat(2)	=	lex

  π(1#)	=	1
  π(2#)	=	1
  π(0#)	=	1
  π(1)	=	1
  π(0)	=	1
  π(2)	=	[1]

  together with the usable rules

  0(1(2(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(24)
  0(1(2(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(25)
  0(1(2(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(27)
  0(1(2(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(29)
  1(1(2(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(66)
  1(1(2(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(67)
  1(1(2(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(68)
  1(1(2(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(69)
  1(1(2(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(70)
  1(1(2(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(72)
  1(1(2(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(74)
  1(2(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(83)
  2(1(1(0(2(x1)))))	→	2(0(1(0(2(x1)))))	(93)
  2(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(97)
  2(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(98)
  2(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(99)
  2(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(100)

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

  1#(1(2(0(2(x1)))))	→	2#(1(0(2(x1))))	(137)
  2#(1(2(0(2(x1)))))	→	2#(1(0(x1)))	(157)
  2#(1(2(0(2(x1)))))	→	0#(x1)	(155)
  0#(1(2(0(2(x1)))))	→	2#(1(0(x1)))	(113)
  2#(1(2(0(2(x1)))))	→	2#(1(0(2(x1))))	(153)
  0#(1(2(0(2(x1)))))	→	0#(x1)	(111)
  0#(1(2(0(2(x1)))))	→	2#(1(0(2(x1))))	(109)
  1#(1(2(0(2(x1)))))	→	0#(x1)	(129)
  1#(1(2(0(2(x1)))))	→	2#(1(2(x1)))	(126)

  could be deleted.

  1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 2 components.

  • The 1^st component contains the pair

    2#(1(2(0(2(x1)))))

    →

    2#(1(0(2(2(x1)))))

    (151)

    1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the

    prec(2#)	=	0		stat(2#)	=	lex
    prec(1)	=	0		stat(1)	=	lex
    prec(0)	=	0		stat(0)	=	lex
    prec(2)	=	1		stat(2)	=	lex

    π(2#)	=	1
    π(1)	=	1
    π(0)	=	[]
    π(2)	=	[]

    together with the usable rules

    0(1(2(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(24)
    0(1(2(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(25)
    0(1(2(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(27)
    0(1(2(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(29)
    1(1(2(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(66)
    1(1(2(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(67)
    1(1(2(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(68)
    1(1(2(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(69)
    1(1(2(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(70)
    1(1(2(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(72)
    1(1(2(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(74)
    1(2(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(83)
    2(1(1(0(2(x1)))))	→	2(0(1(0(2(x1)))))	(93)
    2(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(97)
    2(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(98)
    2(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(99)
    2(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(100)

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

    2#(1(2(0(2(x1)))))

    →

    2#(1(0(2(2(x1)))))

    (151)

    could be deleted.

    1.1.1.1.1.1.1 P is empty

    There are no pairs anymore.

  • The 2^nd component contains the pair

    1#(1(2(0(2(x1)))))	→	1#(1(0(2(2(x1)))))	(135)
    1#(1(2(0(2(x1)))))	→	0#(1(2(2(x1))))	(121)
    0#(1(2(0(2(x1)))))	→	0#(1(1(2(2(x1)))))	(107)
    0#(1(2(0(2(x1)))))	→	1#(1(2(2(x1))))	(106)
    0#(1(2(0(2(x1)))))	→	0#(1(0(2(2(x1)))))	(104)

    1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

    Using the

    prec(1#)	=	0		stat(1#)	=	lex
    prec(0#)	=	0		stat(0#)	=	lex
    prec(1)	=	0		stat(1)	=	lex
    prec(0)	=	0		stat(0)	=	lex
    prec(2)	=	1		stat(2)	=	lex

    π(1#)	=	1
    π(0#)	=	1
    π(1)	=	1
    π(0)	=	[]
    π(2)	=	[]

    together with the usable rules

    0(1(2(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(24)
    0(1(2(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(25)
    0(1(2(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(27)
    0(1(2(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(29)
    1(1(2(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(66)
    1(1(2(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(67)
    1(1(2(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(68)
    1(1(2(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(69)
    1(1(2(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(70)
    1(1(2(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(72)
    1(1(2(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(74)
    1(2(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(83)
    2(1(1(0(2(x1)))))	→	2(0(1(0(2(x1)))))	(93)
    2(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(97)
    2(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(98)
    2(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(99)
    2(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(100)

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

    1#(1(2(0(2(x1)))))	→	1#(1(0(2(2(x1)))))	(135)
    0#(1(2(0(2(x1)))))	→	0#(1(0(2(2(x1)))))	(104)

    could be deleted.

    1.1.1.1.1.2.1 Subterm Criterion Processor

    We use the projection to multisets

    π(1#)	=	{ 1, 1 }
    π(0#)	=	{ 1, 1 }
    π(1)	=	{ 1, 1 }
    π(0)	=	{ 1, 1 }
    π(2)	=	{ 1, 1 }

    to remove the pairs:

    1#(1(2(0(2(x1)))))	→	0#(1(2(2(x1))))	(121)
    0#(1(2(0(2(x1)))))	→	1#(1(2(2(x1))))	(106)

    1.1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the naturals

    [0(x1)]	=	0 0 2 0 · x1 + 0 0 2 0
    [0#(x1)]	=	1 0 0 0 · x1 + 2 0 0 0
    [2(x1)]	=	0 1 0 0 · x1 + 0 0 1 0
    [1(x1)]	=	1 0 2 0 · x1 + 0 0 2 0

    together with the usable rules

    0(1(2(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(24)
    0(1(2(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(25)
    0(1(2(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(27)
    0(1(2(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(29)
    1(1(2(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(66)
    1(1(2(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(67)
    1(1(2(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(68)
    1(1(2(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(69)
    1(1(2(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(70)
    1(1(2(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(72)
    1(1(2(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(74)
    1(2(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(83)
    2(1(1(0(2(x1)))))	→	2(0(1(0(2(x1)))))	(93)
    2(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(97)
    2(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(98)
    2(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(99)
    2(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(100)

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

    0#(1(2(0(2(x1)))))

    →

    0#(1(1(2(2(x1)))))

    (107)

    could be deleted.

    1.1.1.1.1.2.1.1.1 P is empty

    There are no pairs anymore.