Precedence:  from > first > cons > [0,nil] > add > s
Status Mapping: All symbols Lex
Marking Map: 
     MMap(add_, 1) = from, cons, nil, first, s, 0, add, if, false, true, and
     MMap(add_, 2) = from, cons, nil, first, s, 0, add, if, false, true, and
     MMap(cons, 1) = from, cons, nil, first, s, 0, add, if, false, true, and
     MMap(cons, 2) = from, first
     MMap(first_, 1) = from, cons, nil, first, s, 0, add, if, false, true, and
     MMap(first_, 2) = from, cons, nil, first, s, 0, add, if, false, true, and
     MMap(s, 1) = from, cons, nil, first, s, 0, if, false, true, and, add

Termination was proved succesfully.