YES

We show the termination of the TRS R:

  and(true(),y) -> y
  and(false(),y) -> false()
  eq(nil(),nil()) -> true()
  eq(cons(t,l),nil()) -> false()
  eq(nil(),cons(t,l)) -> false()
  eq(cons(t,l),cons(|t'|,|l'|)) -> and(eq(t,|t'|),eq(l,|l'|))
  eq(var(l),var(|l'|)) -> eq(l,|l'|)
  eq(var(l),apply(t,s)) -> false()
  eq(var(l),lambda(x,t)) -> false()
  eq(apply(t,s),var(l)) -> false()
  eq(apply(t,s),apply(|t'|,|s'|)) -> and(eq(t,|t'|),eq(s,|s'|))
  eq(apply(t,s),lambda(x,t)) -> false()
  eq(lambda(x,t),var(l)) -> false()
  eq(lambda(x,t),apply(t,s)) -> false()
  eq(lambda(x,t),lambda(|x'|,|t'|)) -> and(eq(x,|x'|),eq(t,|t'|))
  if(true(),var(k),var(|l'|)) -> var(k)
  if(false(),var(k),var(|l'|)) -> var(|l'|)
  ren(var(l),var(k),var(|l'|)) -> if(eq(l,|l'|),var(k),var(|l'|))
  ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
  ren(x,y,lambda(z,t)) -> lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)))

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: eq#(cons(t,l),cons(|t'|,|l'|)) -> and#(eq(t,|t'|),eq(l,|l'|))
p2: eq#(cons(t,l),cons(|t'|,|l'|)) -> eq#(t,|t'|)
p3: eq#(cons(t,l),cons(|t'|,|l'|)) -> eq#(l,|l'|)
p4: eq#(var(l),var(|l'|)) -> eq#(l,|l'|)
p5: eq#(apply(t,s),apply(|t'|,|s'|)) -> and#(eq(t,|t'|),eq(s,|s'|))
p6: eq#(apply(t,s),apply(|t'|,|s'|)) -> eq#(t,|t'|)
p7: eq#(apply(t,s),apply(|t'|,|s'|)) -> eq#(s,|s'|)
p8: eq#(lambda(x,t),lambda(|x'|,|t'|)) -> and#(eq(x,|x'|),eq(t,|t'|))
p9: eq#(lambda(x,t),lambda(|x'|,|t'|)) -> eq#(x,|x'|)
p10: eq#(lambda(x,t),lambda(|x'|,|t'|)) -> eq#(t,|t'|)
p11: ren#(var(l),var(k),var(|l'|)) -> if#(eq(l,|l'|),var(k),var(|l'|))
p12: ren#(var(l),var(k),var(|l'|)) -> eq#(l,|l'|)
p13: ren#(x,y,apply(t,s)) -> ren#(x,y,t)
p14: ren#(x,y,apply(t,s)) -> ren#(x,y,s)
p15: ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
p16: ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)

and R consists of:

r1: and(true(),y) -> y
r2: and(false(),y) -> false()
r3: eq(nil(),nil()) -> true()
r4: eq(cons(t,l),nil()) -> false()
r5: eq(nil(),cons(t,l)) -> false()
r6: eq(cons(t,l),cons(|t'|,|l'|)) -> and(eq(t,|t'|),eq(l,|l'|))
r7: eq(var(l),var(|l'|)) -> eq(l,|l'|)
r8: eq(var(l),apply(t,s)) -> false()
r9: eq(var(l),lambda(x,t)) -> false()
r10: eq(apply(t,s),var(l)) -> false()
r11: eq(apply(t,s),apply(|t'|,|s'|)) -> and(eq(t,|t'|),eq(s,|s'|))
r12: eq(apply(t,s),lambda(x,t)) -> false()
r13: eq(lambda(x,t),var(l)) -> false()
r14: eq(lambda(x,t),apply(t,s)) -> false()
r15: eq(lambda(x,t),lambda(|x'|,|t'|)) -> and(eq(x,|x'|),eq(t,|t'|))
r16: if(true(),var(k),var(|l'|)) -> var(k)
r17: if(false(),var(k),var(|l'|)) -> var(|l'|)
r18: ren(var(l),var(k),var(|l'|)) -> if(eq(l,|l'|),var(k),var(|l'|))
r19: ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
r20: ren(x,y,lambda(z,t)) -> lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)))

The estimated dependency graph contains the following SCCs:

  {p13, p14, p15, p16}
  {p2, p3, p4, p6, p7, p9, p10}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
p2: ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
p3: ren#(x,y,apply(t,s)) -> ren#(x,y,s)
p4: ren#(x,y,apply(t,s)) -> ren#(x,y,t)

and R consists of:

r1: and(true(),y) -> y
r2: and(false(),y) -> false()
r3: eq(nil(),nil()) -> true()
r4: eq(cons(t,l),nil()) -> false()
r5: eq(nil(),cons(t,l)) -> false()
r6: eq(cons(t,l),cons(|t'|,|l'|)) -> and(eq(t,|t'|),eq(l,|l'|))
r7: eq(var(l),var(|l'|)) -> eq(l,|l'|)
r8: eq(var(l),apply(t,s)) -> false()
r9: eq(var(l),lambda(x,t)) -> false()
r10: eq(apply(t,s),var(l)) -> false()
r11: eq(apply(t,s),apply(|t'|,|s'|)) -> and(eq(t,|t'|),eq(s,|s'|))
r12: eq(apply(t,s),lambda(x,t)) -> false()
r13: eq(lambda(x,t),var(l)) -> false()
r14: eq(lambda(x,t),apply(t,s)) -> false()
r15: eq(lambda(x,t),lambda(|x'|,|t'|)) -> and(eq(x,|x'|),eq(t,|t'|))
r16: if(true(),var(k),var(|l'|)) -> var(k)
r17: if(false(),var(k),var(|l'|)) -> var(|l'|)
r18: ren(var(l),var(k),var(|l'|)) -> if(eq(l,|l'|),var(k),var(|l'|))
r19: ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
r20: ren(x,y,lambda(z,t)) -> lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)))

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      ren#_A(x1,x2,x3) = ((0,0,0,0),(1,0,0,0),(1,1,0,0),(1,0,0,0)) x2 + ((0,0,0,0),(1,0,0,0),(1,0,0,0),(1,1,0,0)) x3
      lambda_A(x1,x2) = ((0,0,0,0),(1,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + ((1,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x2 + (3,2,0,4)
      var_A(x1) = (1,3,1,1)
      cons_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(1,0,1,0)) x1 + ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x2 + (1,1,1,1)
      nil_A() = (1,1,1,1)
      ren_A(x1,x2,x3) = ((0,0,0,0),(1,0,0,0),(0,0,0,0),(0,1,0,0)) x1 + ((1,0,0,0),(0,0,0,0),(1,1,0,0),(0,1,1,0)) x3 + (0,4,0,1)
      apply_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + x2 + (1,4,1,1)
      and_A(x1,x2) = x2
      true_A() = (1,2,2,1)
      false_A() = (0,0,0,0)
      eq_A(x1,x2) = (2,1,1,0)
      if_A(x1,x2,x3) = (1,4,0,0)

The next rules are strictly ordered:

  p1, p2, p3, p4

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: eq#(cons(t,l),cons(|t'|,|l'|)) -> eq#(t,|t'|)
p2: eq#(lambda(x,t),lambda(|x'|,|t'|)) -> eq#(t,|t'|)
p3: eq#(lambda(x,t),lambda(|x'|,|t'|)) -> eq#(x,|x'|)
p4: eq#(apply(t,s),apply(|t'|,|s'|)) -> eq#(s,|s'|)
p5: eq#(apply(t,s),apply(|t'|,|s'|)) -> eq#(t,|t'|)
p6: eq#(var(l),var(|l'|)) -> eq#(l,|l'|)
p7: eq#(cons(t,l),cons(|t'|,|l'|)) -> eq#(l,|l'|)

and R consists of:

r1: and(true(),y) -> y
r2: and(false(),y) -> false()
r3: eq(nil(),nil()) -> true()
r4: eq(cons(t,l),nil()) -> false()
r5: eq(nil(),cons(t,l)) -> false()
r6: eq(cons(t,l),cons(|t'|,|l'|)) -> and(eq(t,|t'|),eq(l,|l'|))
r7: eq(var(l),var(|l'|)) -> eq(l,|l'|)
r8: eq(var(l),apply(t,s)) -> false()
r9: eq(var(l),lambda(x,t)) -> false()
r10: eq(apply(t,s),var(l)) -> false()
r11: eq(apply(t,s),apply(|t'|,|s'|)) -> and(eq(t,|t'|),eq(s,|s'|))
r12: eq(apply(t,s),lambda(x,t)) -> false()
r13: eq(lambda(x,t),var(l)) -> false()
r14: eq(lambda(x,t),apply(t,s)) -> false()
r15: eq(lambda(x,t),lambda(|x'|,|t'|)) -> and(eq(x,|x'|),eq(t,|t'|))
r16: if(true(),var(k),var(|l'|)) -> var(k)
r17: if(false(),var(k),var(|l'|)) -> var(|l'|)
r18: ren(var(l),var(k),var(|l'|)) -> if(eq(l,|l'|),var(k),var(|l'|))
r19: ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
r20: ren(x,y,lambda(z,t)) -> lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      eq#_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2
      cons_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
      lambda_A(x1,x2) = ((1,0,0,0),(1,0,0,0),(1,0,0,0),(1,1,0,0)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
      apply_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
      var_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7

We remove them from the problem.  Then no dependency pair remains.