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)

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

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.