YES

Problem:
 o(x) -> a(l(x))
 a(l(x)) -> l(a(a(x)))
 l(o(x)) -> o(l(x))
 a(x) -> x
 H(0(),x) -> o(x)
 a(H(H(0(),y),z)) -> c1(y,z)
 a(H(H(H(0(),x),y),z)) -> c2(x,y,z)
 c2(x,y,z) -> o(H(y,z))
 a(c1(x,y)) -> c1(x,H(x,y))
 a(c2(x,y,z)) -> c2(x,H(x,y),z)
 c1(y,z) -> o(z)

Proof:
 Embedding Processor:
  strict:
   o(x) -> a(l(x))
   a(l(x)) -> l(a(a(x)))
   l(o(x)) -> o(l(x))
   a(x) -> x
   H(0(),x) -> o(x)
   a(H(H(0(),y),z)) -> c1(y,z)
   a(H(H(H(0(),x),y),z)) -> c2(x,y,z)
   c2(x,y,z) -> o(H(y,z))
   a(c1(x,y)) -> c1(x,H(x,y))
   a(c2(x,y,z)) -> c2(x,H(x,y),z)
   c1(y,z) -> o(z)
  weak:
   o(x0) -> x0
   a(x0) -> x0
   l(x0) -> x0
   H(x0,x1) -> x0
   H(x0,x1) -> x1
   c1(x0,x1) -> x0
   c1(x0,x1) -> x1
   c2(x0,x1,x2) -> x0
   c2(x0,x1,x2) -> x1
   c2(x0,x1,x2) -> x2
  Higher Ordinal Interpretation Processor:
   degree: 3
   reverse arguments: false
   interpretation:
    o(x6) =  (+) x6
    a(x7) =  (+) x7
    l(x8) =  (+) x8
    H(x9,x10) = omega^( (+) x9) (+) x10
    0() =  (+) 1
    c1(x11,x12) = x12 + omega^(x11 (+) 1)
    c2(x13,x14,x15) = omega^(x14 + omega^(x13 (+) 1)) (+) x15
   problem:
    strict:
     o(x) -> a(l(x))
     a(l(x)) -> l(a(a(x)))
     l(o(x)) -> o(l(x))
     a(x) -> x
     a(c1(x,y)) -> c1(x,H(x,y))
     a(c2(x,y,z)) -> c2(x,H(x,y),z)
    weak:
     o(x0) -> x0
     a(x0) -> x0
     l(x0) -> x0
     f7() -> c1(x11,x12)
     f8(x15) -> c2(x13,x14,x15)
   Matrix Interpretation Processor: dim=2
    
    interpretation:
                [2 0]     [2]
     [f8](x0) = [2 2]x0 + [0],
     
            [2]
     [f7] = [2],
     
                        [1]
     [c2](x0, x1, x2) = [0],
     
                    [0]
     [c1](x0, x1) = [2],
     
                   [0]
     [H](x0, x1) = [0],
     
                 
     [a](x0) = x0,
     
               [1 1]  
     [l](x0) = [0 1]x0,
     
               [1 2]     [0]
     [o](x0) = [0 1]x0 + [2]
    orientation:
            [1 2]    [0]    [1 1]           
     o(x) = [0 1]x + [2] >= [0 1]x = a(l(x))
     
               [1 1]     [1 1]              
     a(l(x)) = [0 1]x >= [0 1]x = l(a(a(x)))
     
               [1 3]    [2]    [1 3]    [0]          
     l(o(x)) = [0 1]x + [2] >= [0 1]x + [2] = o(l(x))
     
                      
     a(x) = x >= x = x
     
                  [0]    [0]               
     a(c1(x,y)) = [2] >= [2] = c1(x,H(x,y))
     
                    [1]    [1]                 
     a(c2(x,y,z)) = [0] >= [0] = c2(x,H(x,y),z)
     
             [1 2]     [0]           
     o(x0) = [0 1]x0 + [2] >= x0 = x0
     
                          
     a(x0) = x0 >= x0 = x0
     
             [1 1]             
     l(x0) = [0 1]x0 >= x0 = x0
     
            [2]    [0]              
     f7() = [2] >= [2] = c1(x11,x12)
     
               [2 0]      [2]    [1]                  
     f8(x15) = [2 2]x15 + [0] >= [0] = c2(x13,x14,x15)
    problem:
     strict:
      o(x) -> a(l(x))
      a(l(x)) -> l(a(a(x)))
      a(x) -> x
      a(c1(x,y)) -> c1(x,H(x,y))
      a(c2(x,y,z)) -> c2(x,H(x,y),z)
     weak:
      o(x0) -> x0
      a(x0) -> x0
      l(x0) -> x0
      f7() -> c1(x11,x12)
      f8(x15) -> c2(x13,x14,x15)
      f9() -> c1(x16,x17)
      f10() -> H(x18,x19)
      f11() -> c2(x20,x21,x22)
    Matrix Interpretation Processor: dim=2
     
     interpretation:
              [0]
      [f11] = [0],
      
              [0]
      [f10] = [0],
      
             [0]
      [f9] = [0],
      
                 [2 0]     [0]
      [f8](x0) = [0 0]x0 + [1],
      
             [0]
      [f7] = [0],
      
                         [0]
      [c2](x0, x1, x2) = [0],
      
                     [0]
      [c1](x0, x1) = [0],
      
                    [0]
      [H](x0, x1) = [0],
      
                [1 1]  
      [a](x0) = [0 1]x0,
      
                [1 0]     [0]
      [l](x0) = [0 3]x0 + [2],
      
                [2 3]     [2]
      [o](x0) = [2 3]x0 + [3]
     orientation:
             [2 3]    [2]    [1 3]    [2]          
      o(x) = [2 3]x + [3] >= [0 3]x + [2] = a(l(x))
      
                [1 3]    [2]    [1 2]    [0]             
      a(l(x)) = [0 3]x + [2] >= [0 3]x + [2] = l(a(a(x)))
      
             [1 1]          
      a(x) = [0 1]x >= x = x
      
                   [0]    [0]               
      a(c1(x,y)) = [0] >= [0] = c1(x,H(x,y))
      
                     [0]    [0]                 
      a(c2(x,y,z)) = [0] >= [0] = c2(x,H(x,y),z)
      
              [2 3]     [2]           
      o(x0) = [2 3]x0 + [3] >= x0 = x0
      
              [1 1]             
      a(x0) = [0 1]x0 >= x0 = x0
      
              [1 0]     [0]           
      l(x0) = [0 3]x0 + [2] >= x0 = x0
      
             [0]    [0]              
      f7() = [0] >= [0] = c1(x11,x12)
      
                [2 0]      [0]    [0]                  
      f8(x15) = [0 0]x15 + [1] >= [0] = c2(x13,x14,x15)
      
             [0]    [0]              
      f9() = [0] >= [0] = c1(x16,x17)
      
              [0]    [0]             
      f10() = [0] >= [0] = H(x18,x19)
      
              [0]    [0]                  
      f11() = [0] >= [0] = c2(x20,x21,x22)
     problem:
      strict:
       o(x) -> a(l(x))
       a(x) -> x
       a(c1(x,y)) -> c1(x,H(x,y))
       a(c2(x,y,z)) -> c2(x,H(x,y),z)
      weak:
       o(x0) -> x0
       a(x0) -> x0
       l(x0) -> x0
       f7() -> c1(x11,x12)
       f8(x15) -> c2(x13,x14,x15)
       f9() -> c1(x16,x17)
       f10() -> H(x18,x19)
       f11() -> c2(x20,x21,x22)
       f12() -> c1(x23,x24)
       f13() -> H(x25,x26)
       f14() -> c2(x27,x28,x29)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [f14] = 0,
       
       [f13] = 0,
       
       [f12] = 0,
       
       [f11] = 0,
       
       [f10] = 0,
       
       [f9] = 0,
       
       [f8](x0) = 2x0,
       
       [f7] = 0,
       
       [c2](x0, x1, x2) = 0,
       
       [c1](x0, x1) = 0,
       
       [H](x0, x1) = 0,
       
       [a](x0) = 2x0 + 1,
       
       [l](x0) = x0,
       
       [o](x0) = 2x0 + 2
      orientation:
       o(x) = 2x + 2 >= 2x + 1 = a(l(x))
       
       a(x) = 2x + 1 >= x = x
       
       a(c1(x,y)) = 1 >= 0 = c1(x,H(x,y))
       
       a(c2(x,y,z)) = 1 >= 0 = c2(x,H(x,y),z)
       
       o(x0) = 2x0 + 2 >= x0 = x0
       
       a(x0) = 2x0 + 1 >= x0 = x0
       
       l(x0) = x0 >= x0 = x0
       
       f7() = 0 >= 0 = c1(x11,x12)
       
       f8(x15) = 2x15 >= 0 = c2(x13,x14,x15)
       
       f9() = 0 >= 0 = c1(x16,x17)
       
       f10() = 0 >= 0 = H(x18,x19)
       
       f11() = 0 >= 0 = c2(x20,x21,x22)
       
       f12() = 0 >= 0 = c1(x23,x24)
       
       f13() = 0 >= 0 = H(x25,x26)
       
       f14() = 0 >= 0 = c2(x27,x28,x29)
      problem:
       strict:
        
       weak:
        o(x0) -> x0
        a(x0) -> x0
        l(x0) -> x0
        f7() -> c1(x11,x12)
        f8(x15) -> c2(x13,x14,x15)
        f9() -> c1(x16,x17)
        f10() -> H(x18,x19)
        f11() -> c2(x20,x21,x22)
        f12() -> c1(x23,x24)
        f13() -> H(x25,x26)
        f14() -> c2(x27,x28,x29)
        f15() -> c1(x30,x31)
        f16() -> H(x32,x33)
        f17() -> c2(x34,x35,x36)
      Qed