YES

Problem:
 strict:
  o(lambda(x),y) -> lambda(o(x,d(1(),o(y,p()))))
  o(d(x,y),z) -> d(o(x,z),o(y,z))
  o(o(x,y),z) -> o(x,o(y,z))
  lambda(x) -> x
  o(x,y) -> x
  o(x,y) -> y
  d(x,y) -> x
  d(x,y) -> y
 weak:
  o(x,y) -> d(x,y)
  o(x,y) -> d(y,x)

Proof:
 RT Transformation Processor:
  o(lambda(x),y) -> lambda(o(x,d(1(),o(y,p()))))
  o(d(x,y),z) -> d(o(x,z),o(y,z))
  o(o(x,y),z) -> o(x,o(y,z))
  lambda(x) -> x
  o(x,y) -> x
  o(x,y) -> y
  d(x,y) -> x
  d(x,y) -> y
  o(x,y) -> d(x,y)
  o(x,y) -> d(y,x)
  WPO Processor:
   algebra: MSum
   weight function:
    w0 = 0
    w(lambda) = 6
    w(d) = w(p) = w(1) = w(o) = 0
   status function:
    st(d) = [0, 1]
    st(p) = st(1) = []
    st(o) = [0, 1]
    st(lambda) = [0]
   subterm penalty function:
    sp(lambda, 0) = 4
    sp(d, 1) = sp(d, 0) = sp(o, 1) = sp(o, 0) = 0
   subterm coefficient function:
    sc(d, 1) = sc(d, 0) = sc(o, 1) = sc(o, 0) = sc(lambda, 0) = 1
   weight status function:
    ws(1) = ws(o) = pol
    ws(d) = ws(p) = ws(lambda) = max
   precedence:
    o > d ~ p ~ 1 ~ lambda
   problem:
    
   Qed