Certification Problem

Input (TPDB TRS_Standard/AotoYamada_05/009)

The rewrite relation of the following TRS is considered.

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

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)	(13)
app^#(app(forall,p),app(app(cons,x),xs))	→	app^#(p,x)	(14)
app^#(app(forall,p),app(app(cons,x),xs))	→	app^#(and,app(p,x))	(15)
app^#(app(forall,p),app(app(cons,x),xs))	→	app^#(app(and,app(p,x)),app(app(forall,p),xs))	(16)
app^#(app(forsome,p),app(app(cons,x),xs))	→	app^#(app(forsome,p),xs)	(17)
app^#(app(forsome,p),app(app(cons,x),xs))	→	app^#(p,x)	(18)
app^#(app(forsome,p),app(app(cons,x),xs))	→	app^#(or,app(p,x))	(19)
app^#(app(forsome,p),app(app(cons,x),xs))	→	app^#(app(or,app(p,x)),app(app(forsome,p),xs))	(20)

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)	(17)
app^#(app(forsome,p),app(app(cons,x),xs))	→	app^#(p,x)	(18)
app^#(app(forall,p),app(app(cons,x),xs))	→	app^#(p,x)	(14)
app^#(app(forall,p),app(app(cons,x),xs))	→	app^#(app(forall,p),xs)	(13)

We use the projection

π(app^#)

and remove the pairs:

app^#(app(forsome,p),app(app(cons,x),xs))	→	app^#(p,x)	(18)
app^#(app(forall,p),app(app(cons,x),xs))	→	app^#(p,x)	(14)

The dependency pairs are split into 2 components.