Certification Problem

Input (TPDB TRS_Standard/Secret_05_TRS/teparla2)

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 1 component.

• The 1^st component contains the pair

  f#(y,f(x,f(a,x)))	→	f#(a,y)	(6)
  f#(y,f(x,f(a,x)))	→	f#(f(f(a,x),f(x,a)),f(a,y))	(3)

  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):

  [a]	=	1
  [f(x1, x2)]	=	0
  [f#(x1, x2)]	=	0

  We obtain the set of labeled pairs

  f#00(y,f00(x,f10(a,x)))	→	f#10(a,y)	(10)
  f#00(y,f00(x,f10(a,x)))	→	f#00(f00(f10(a,x),f01(x,a)),f10(a,y))	(11)
  f#00(y,f10(x,f11(a,x)))	→	f#00(f00(f11(a,x),f11(x,a)),f10(a,y))	(12)
  f#10(y,f00(x,f10(a,x)))	→	f#00(f00(f10(a,x),f01(x,a)),f11(a,y))	(13)
  f#10(y,f10(x,f11(a,x)))	→	f#00(f00(f11(a,x),f11(x,a)),f11(a,y))	(14)
  f#00(y,f10(x,f11(a,x)))	→	f#10(a,y)	(15)
  f#10(y,f00(x,f10(a,x)))	→	f#11(a,y)	(16)
  f#10(y,f10(x,f11(a,x)))	→	f#11(a,y)	(17)

  and the set of labeled rules:

  f00(y,f00(x,f10(a,x)))	→	f00(f00(f10(a,x),f01(x,a)),f10(a,y))	(18)
  f00(y,f10(x,f11(a,x)))	→	f00(f00(f11(a,x),f11(x,a)),f10(a,y))	(19)
  f10(y,f00(x,f10(a,x)))	→	f00(f00(f10(a,x),f01(x,a)),f11(a,y))	(20)
  f10(y,f10(x,f11(a,x)))	→	f00(f00(f11(a,x),f11(x,a)),f11(a,y))	(21)
  f00(x,f00(x,y))	→	f01(f01(f01(x,a),a),a)	(22)
  f00(x,f01(x,y))	→	f01(f01(f01(x,a),a),a)	(23)
  f10(x,f10(x,y))	→	f01(f01(f11(x,a),a),a)	(24)
  f10(x,f11(x,y))	→	f01(f01(f11(x,a),a),a)	(25)

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    f#00(y,f00(x,f10(a,x)))	→	f#00(f00(f10(a,x),f01(x,a)),f10(a,y))	(11)
    f#00(y,f10(x,f11(a,x)))	→	f#00(f00(f11(a,x),f11(x,a)),f10(a,y))	(12)

    1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [f10(x1, x2)]	=	1 · x1 + 1 · x2
    [f00(x1, x2)]	=	1 · x1 + 1 · x2
    [a]	=	0
    [f01(x1, x2)]	=	1 · x1 + 1 · x2
    [f11(x1, x2)]	=	1 · x1 + 1 · x2
    [f#00(x1, x2)]	=	1 · x1 + 1 · x2

    together with the usable rules

    f10(y,f00(x,f10(a,x)))	→	f00(f00(f10(a,x),f01(x,a)),f11(a,y))	(20)
    f10(y,f10(x,f11(a,x)))	→	f00(f00(f11(a,x),f11(x,a)),f11(a,y))	(21)
    f10(x,f10(x,y))	→	f01(f01(f11(x,a),a),a)	(24)
    f10(x,f11(x,y))	→	f01(f01(f11(x,a),a),a)	(25)
    f00(x,f01(x,y))	→	f01(f01(f01(x,a),a),a)	(23)

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

    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#00(y,f10(x,f11(a,x)))

      →

      f#00(f00(f11(a,x),f11(x,a)),f10(a,y))

      (12)

      1.1.1.1.1.1.1 Monotonic Reduction Pair Processor

      Using the linear polynomial interpretation over the naturals

      [f10(x1, x2)]	=	1 + 1 · x1 + 1 · x2
      [f00(x1, x2)]	=	1 · x1 + 1 · x2
      [a]	=	0
      [f01(x1, x2)]	=	1 · x1 + 1 · x2
      [f11(x1, x2)]	=	1 · x1 + 1 · x2
      [f#00(x1, x2)]	=	1 · x1 + 1 · x2

      the rules

      f10(y,f00(x,f10(a,x)))	→	f00(f00(f10(a,x),f01(x,a)),f11(a,y))	(20)
      f10(y,f10(x,f11(a,x)))	→	f00(f00(f11(a,x),f11(x,a)),f11(a,y))	(21)
      f10(x,f10(x,y))	→	f01(f01(f11(x,a),a),a)	(24)
      f10(x,f11(x,y))	→	f01(f01(f11(x,a),a),a)	(25)

      could be deleted.

      1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

      Using the linear polynomial interpretation over the naturals

      [f#00(x1, x2)]	=	1 · x1 + 1 · x2
      [f10(x1, x2)]	=	1 · x1 + 1 · x2
      [f11(x1, x2)]	=	1 · x1 + 1 · x2
      [a]	=	0
      [f00(x1, x2)]	=	1 · x1 + 1 · x2

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

      1.1.1.1.1.1.1.1.1 Reduction Pair Processor

      Using the linear polynomial interpretation over the naturals

      [f#00(x1, x2)]	=	1 · x1 + 1 · x2
      [f10(x1, x2)]	=	1 · x1 + 1 · x2
      [f11(x1, x2)]	=	1 + 1 · x2
      [a]	=	0
      [f00(x1, x2)]	=	0

      the pair

      f#00(y,f10(x,f11(a,x)))

      →

      f#00(f00(f11(a,x),f11(x,a)),f10(a,y))

      (12)

      could be deleted.

      1.1.1.1.1.1.1.1.1.1 P is empty

      There are no pairs anymore.