Term Rewriting System R:

   [x, y, p, xs]
   app(app(and, true), true) -> true
   app(app(and, x), false) -> false
   app(app(and, false), y) -> false
   app(app(or, true), y) -> true
   app(app(or, x), true) -> true
   app(app(or, false), false) -> false
   app(app(forall, p), nil) -> true
   app(app(forall, p), app(app(cons, x), xs)) -> app(app(and, app(p, x)), app(app(forall, p), xs))
   app(app(forsome, p), nil) -> false
   app(app(forsome, p), app(app(cons, x), xs)) -> app(app(or, app(p, x)), app(app(forsome, p), xs))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   APP(app(forall, p), app(app(cons, x), xs)) -> APP(app(and, app(p, x)), app(app(forall, p), xs))
   APP(app(forall, p), app(app(cons, x), xs)) -> APP(and, app(p, x))
   APP(app(forall, p), app(app(cons, x), xs)) -> APP(p, x)
   APP(app(forall, p), app(app(cons, x), xs)) -> APP(app(forall, p), xs)
   APP(app(forsome, p), app(app(cons, x), xs)) -> APP(app(or, app(p, x)), app(app(forsome, p), xs))
   APP(app(forsome, p), app(app(cons, x), xs)) -> APP(or, app(p, x))
   APP(app(forsome, p), app(app(cons, x), xs)) -> APP(p, x)
   APP(app(forsome, p), app(app(cons, x), xs)) -> APP(app(forsome, p), xs)

Furthermore, R contains one SCC.


SCC1:

APP(app(forsome, p), app(app(cons, x), xs)) -> APP(app(forsome, p), xs)
APP(app(forsome, p), app(app(cons, x), xs)) -> APP(p, x)
APP(app(forsome, p), app(app(cons, x), xs)) -> APP(app(or, app(p, x)), app(app(forsome, p), xs))
APP(app(forall, p), app(app(cons, x), xs)) -> APP(app(forall, p), xs)
APP(app(forall, p), app(app(cons, x), xs)) -> APP(p, x)
APP(app(forall, p), app(app(cons, x), xs)) -> APP(app(and, app(p, x)), app(app(forall, p), xs))

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   app(app(and, true), true) -> true
   app(app(and, x), false) -> false
   app(app(forall, p), nil) -> true
   app(app(forall, p), app(app(cons, x), xs)) -> app(app(and, app(p, x)), app(app(forall, p), xs))
   app(app(forsome, p), nil) -> false
   app(app(or, x), true) -> true
   app(app(and, false), y) -> false
   app(app(or, false), false) -> false
   app(app(or, true), y) -> true
   app(app(forsome, p), app(app(cons, x), xs)) -> app(app(or, app(p, x)), app(app(forsome, p), xs))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(nil) = 0
POL(APP(x_1, x_2)) = 1 + x_1*x_2
POL(forsome) = 1
POL(and) = 0
POL(true) = 0
POL(or) = 0
POL(forall) = 1
POL(app(x_1, x_2)) = x_1 + x_1*x_2
POL(false) = 0
POL(cons) = 1

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 12.847 seconds.