TRS:
 {         app(nil(), YS) -> YS,
         app(cons(X), YS) -> cons(X),
                  from(X) -> cons(X),
         zWadr(nil(), YS) -> nil(),
         zWadr(XS, nil()) -> nil(),
  zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X))),
                prefix(L) -> cons(nil())}
 POP* + Boolean Semantic Labelling:
  Normal positions:
  pi(prefix_sl=1) = [1], pi(prefix_sl=0) = [1], pi(zWadr_sl=1) = [1,2], pi(zWadr_sl=0) = [1,2], pi(from_sl=1) = [1], pi(from_sl=0) = [1], pi(app_sl=1) = [1,2], pi(app_sl=0) = [1]
  
Safe positions:
   pi(cons_sl=1) = [1], pi(cons_sl=0) = [1], pi(app_sl=0) = [2]
  
Precedence:
   zWadr_sl=0 > app_sl=0, 
   zWadr_sl=0 > cons_sl=0, 
   from_sl=0 > cons_sl=0, 
   prefix_sl=0 > cons_sl=0, 
   prefix_sl=0 > nil_sl=0
   empty
  
Interpretation:
   app^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 1
   nil^(0):
    | 1
   cons^(1):
   0 | 0
   1 | 0
   from^(1):
   0 | 0
   1 | 0
   zWadr^(2):
   00 | 0
   01 | 1
   10 | 1
   11 | 1
   prefix^(1):
   0 | 0
   1 | 0
   
  
Labelling:
   app^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   nil^(0):
    | 0
   cons^(1):
   0 | 0
   1 | 0
   from^(1):
   0 | 0
   1 | 0
   zWadr^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   prefix^(1):
   0 | 0
   1 | 0
   
  
Labelled predicative System:
   {                 app_sl=0(nil_sl=0();YS) -> YS,
                     app_sl=0(nil_sl=0();YS) -> YS,
                  app_sl=0(cons_sl=0(;X);YS) -> cons_sl=0(;X),
                  app_sl=0(cons_sl=0(;X);YS) -> cons_sl=0(;X),
                  app_sl=0(cons_sl=0(;X);YS) -> cons_sl=0(;X),
                  app_sl=0(cons_sl=0(;X);YS) -> cons_sl=0(;X),
                               from_sl=0(X;) -> cons_sl=0(;X),
                               from_sl=0(X;) -> cons_sl=0(;X),
                  zWadr_sl=0(nil_sl=0(),YS;) -> nil_sl=0(),
                  zWadr_sl=0(nil_sl=0(),YS;) -> nil_sl=0(),
                  zWadr_sl=0(XS,nil_sl=0();) -> nil_sl=0(),
                  zWadr_sl=0(XS,nil_sl=0();) -> nil_sl=0(),
    zWadr_sl=0(cons_sl=0(;X),cons_sl=0(;Y);) -> cons_sl=0(;app_sl=0(Y;cons_sl=0(;X))),
    zWadr_sl=0(cons_sl=0(;X),cons_sl=0(;Y);) -> cons_sl=0(;app_sl=0(Y;cons_sl=0(;X))),
    zWadr_sl=0(cons_sl=0(;X),cons_sl=0(;Y);) -> cons_sl=0(;app_sl=0(Y;cons_sl=0(;X))),
    zWadr_sl=0(cons_sl=0(;X),cons_sl=0(;Y);) -> cons_sl=0(;app_sl=0(Y;cons_sl=0(;X))),
                             prefix_sl=0(L;) -> cons_sl=0(;nil_sl=0()),
                             prefix_sl=0(L;) -> cons_sl=0(;nil_sl=0())}
  

  Qed