Certification Problem

Input (TPDB TRS_Standard/AotoYamada_05/012)

The rewrite relation of the following TRS is considered.

app(app(and,true),true)	→	true	(1)
app(app(and,x),false)	→	false	(2)
app(app(and,false),y)	→	false	(3)
app(app(or,true),y)	→	true	(4)
app(app(or,x),true)	→	true	(5)
app(app(or,false),false)	→	false	(6)
app(app(forall,p),nil)	→	true	(7)
app(app(forall,p),app(app(cons,x),xs))	→	app(app(and,app(p,x)),app(app(forall,p),xs))	(8)
app(app(forsome,p),nil)	→	false	(9)
app(app(forsome,p),app(app(cons,x),xs))	→	app(app(or,app(p,x)),app(app(forsome,p),xs))	(10)

Prove or disprove termination.

Yes.

The following set of initial dependency pairs has been identified.

app^#(app(forall,p),app(app(cons,x),xs))	→	app^#(app(forall,p),xs)	(11)
app^#(app(forall,p),app(app(cons,x),xs))	→	app^#(p,x)	(12)
app^#(app(forall,p),app(app(cons,x),xs))	→	app^#(and,app(p,x))	(13)
app^#(app(forall,p),app(app(cons,x),xs))	→	app^#(app(and,app(p,x)),app(app(forall,p),xs))	(14)
app^#(app(forsome,p),app(app(cons,x),xs))	→	app^#(app(forsome,p),xs)	(15)
app^#(app(forsome,p),app(app(cons,x),xs))	→	app^#(p,x)	(16)
app^#(app(forsome,p),app(app(cons,x),xs))	→	app^#(or,app(p,x))	(17)
app^#(app(forsome,p),app(app(cons,x),xs))	→	app^#(app(or,app(p,x)),app(app(forsome,p),xs))	(18)

The dependency pairs are split into 1 component.

The 1^st component contains the pair

app^#(app(forsome,p),app(app(cons,x),xs))	→	app^#(app(forsome,p),xs)	(15)
app^#(app(forsome,p),app(app(cons,x),xs))	→	app^#(p,x)	(16)
app^#(app(forall,p),app(app(cons,x),xs))	→	app^#(p,x)	(12)
app^#(app(forall,p),app(app(cons,x),xs))	→	app^#(app(forall,p),xs)	(11)

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

app^#(app(forsome,p),app(app(cons,x),xs))	→	app^#(app(forsome,p),xs)	(15)

2	>	2
1	≥	1
app^#(app(forsome,p),app(app(cons,x),xs))	→	app^#(p,x)	(16)

2	>	2
1	>	1
app^#(app(forall,p),app(app(cons,x),xs))	→	app^#(p,x)	(12)

2	>	2
1	>	1
app^#(app(forall,p),app(app(cons,x),xs))	→	app^#(app(forall,p),xs)	(11)

2	>	2
1	≥	1

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