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)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
app#(app(forsome,p),app(app(cons,x),xs)) → app#(or,app(p,x)) (11)
app#(app(forall,p),app(app(cons,x),xs)) → app#(and,app(p,x)) (12)
app#(app(forall,p),app(app(cons,x),xs)) → 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#(p,x) (15)
app#(app(forsome,p),app(app(cons,x),xs)) → app#(app(or,app(p,x)),app(app(forsome,p),xs)) (16)
app#(app(forall,p),app(app(cons,x),xs)) → app#(app(forall,p),xs) (17)
app#(app(forsome,p),app(app(cons,x),xs)) → app#(app(forsome,p),xs) (18)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.