Certification Problem

Input (TPDB TRS_Standard/Zantema_05/z06)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

• The 1^st component contains the pair

  f#(a,f(b,x))	→	f#(a,f(a,f(a,x)))	(5)
  f#(a,f(b,x))	→	f#(a,f(a,x))	(4)
  f#(a,f(b,x))	→	f#(a,x)	(3)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the

  prec(f#)	=	0		stat(f#)	=	lex
  prec(f)	=	0		stat(f)	=	lex
  prec(b)	=	1		stat(b)	=	lex
  prec(a)	=	0		stat(a)	=	lex

  π(f#)	=	2
  π(f)	=	[1,2]
  π(b)	=	[]
  π(a)	=	[]

  together with the usable rule

  f(a,f(b,x))

  →

  f(a,f(a,f(a,x)))

  (1)

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

  f#(a,f(b,x))	→	f#(a,f(a,f(a,x)))	(5)
  f#(a,f(b,x))	→	f#(a,f(a,x))	(4)
  f#(a,f(b,x))	→	f#(a,x)	(3)

  could be deleted.

  1.1.1.1 P is empty

  There are no pairs anymore.

• The 2^nd component contains the pair

  f#(b,f(a,x))	→	f#(b,f(b,f(b,x)))	(8)
  f#(b,f(a,x))	→	f#(b,f(b,x))	(7)
  f#(b,f(a,x))	→	f#(b,x)	(6)

  1.1.2 Reduction Pair Processor with Usable Rules

  Using the

  prec(f#)	=	0		stat(f#)	=	lex
  prec(f)	=	0		stat(f)	=	lex
  prec(b)	=	0		stat(b)	=	lex
  prec(a)	=	1		stat(a)	=	lex

  π(f#)	=	2
  π(f)	=	[1,2]
  π(b)	=	[]
  π(a)	=	[]

  together with the usable rule

  f(b,f(a,x))

  →

  f(b,f(b,f(b,x)))

  (2)

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

  f#(b,f(a,x))	→	f#(b,f(b,f(b,x)))	(8)
  f#(b,f(a,x))	→	f#(b,f(b,x))	(7)
  f#(b,f(a,x))	→	f#(b,x)	(6)

  could be deleted.

  1.1.2.1 P is empty

  There are no pairs anymore.