Consider the TRS R consisting of the rewrite rules

1: a__and(true,X) -> mark(X)
2: a__and(false,Y) -> false
3: a__if(true,X,Y) -> mark(X)
4: a__if(false,X,Y) -> mark(Y)
5: a__add(0,X) -> mark(X)
6: a__add(s(X),Y) -> s(add(X,Y))
7: a__first(0,X) -> nil
8: a__first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
9: a__from(X) -> cons(X,from(s(X)))
10: mark(and(X1,X2)) -> a__and(mark(X1),X2)
11: mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
12: mark(add(X1,X2)) -> a__add(mark(X1),X2)
13: mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
14: mark(from(X)) -> a__from(X)
15: mark(true) -> true
16: mark(false) -> false
17: mark(0) -> 0
18: mark(s(X)) -> s(X)
19: mark(nil) -> nil
20: mark(cons(X1,X2)) -> cons(X1,X2)
21: a__and(X1,X2) -> and(X1,X2)
22: a__if(X1,X2,X3) -> if(X1,X2,X3)
23: a__add(X1,X2) -> add(X1,X2)
24: a__first(X1,X2) -> first(X1,X2)
25: a__from(X) -> from(X)

There are 14 dependency pairs:

26: A__AND(true,X) -> MARK(X)
27: A__IF(true,X,Y) -> MARK(X)
28: A__IF(false,X,Y) -> MARK(Y)
29: A__ADD(0,X) -> MARK(X)
30: MARK(and(X1,X2)) -> A__AND(mark(X1),X2)
31: MARK(and(X1,X2)) -> MARK(X1)
32: MARK(if(X1,X2,X3)) -> A__IF(mark(X1),X2,X3)
33: MARK(if(X1,X2,X3)) -> MARK(X1)
34: MARK(add(X1,X2)) -> A__ADD(mark(X1),X2)
35: MARK(add(X1,X2)) -> MARK(X1)
36: MARK(first(X1,X2)) -> A__FIRST(mark(X1),mark(X2))
37: MARK(first(X1,X2)) -> MARK(X1)
38: MARK(first(X1,X2)) -> MARK(X2)
39: MARK(from(X)) -> A__FROM(X)

The approximated dependency graph contains one SCC:
{26-35,37,38}.

- Consider the SCC {26-35,37,38}.
By taking the polynomial interpretation
[0] = [false] = [nil] = [true] = 1,
[mark](x) = [s](x) = x,
[a__from](x) = [from](x) = [MARK](x) = x + 1,
[a__add](x,y) = [A__ADD](x,y) = [a__and](x,y) = [A__AND](x,y) = [a__first](x,y) = [add](x,y) = [and](x,y) = [first](x,y) = x + y + 1,
[a__if](x,y,z) = [A__IF](x,y,z) = [if](x,y,z) = x + y + z + 1
and [cons](x,y) = y,
the rules in {6,8-25}
are weakly decreasing and
the rules in {1-5,7,26-35,37,38}
are strictly decreasing.

Hence the TRS is terminating.