MAYBE

Problem:
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 if(x,y,y) -> y
 if(if(x,y,z),u(),v()) -> if(x,if(y,u(),v()),if(z,u(),v()))

Proof:
 Complexity Transformation Processor:
  strict:
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   if(x,y,y) -> y
   if(if(x,y,z),u(),v()) -> if(x,if(y,u(),v()),if(z,u(),v()))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [v] = 0,
     
     [u] = 0,
     
     [false] = 1,
     
     [if](x0, x1, x2) = x0 + x1 + x2,
     
     [true] = 0
    orientation:
     if(true(),x,y) = x + y >= x = x
     
     if(false(),x,y) = x + y + 1 >= y = y
     
     if(x,y,y) = x + 2y >= y = y
     
     if(if(x,y,z),u(),v()) = x + y + z >= x + y + z = if(x,if(y,u(),v()),if(z,u(),v()))
    problem:
     strict:
      if(true(),x,y) -> x
      if(x,y,y) -> y
      if(if(x,y,z),u(),v()) -> if(x,if(y,u(),v()),if(z,u(),v()))
     weak:
      if(false(),x,y) -> y
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [v] = 0,
       
       [u] = 0,
       
       [false] = 0,
       
       [if](x0, x1, x2) = x0 + x1 + x2,
       
       [true] = 1
      orientation:
       if(true(),x,y) = x + y + 1 >= x = x
       
       if(x,y,y) = x + 2y >= y = y
       
       if(if(x,y,z),u(),v()) = x + y + z >= x + y + z = if(x,if(y,u(),v()),if(z,u(),v()))
       
       if(false(),x,y) = x + y >= y = y
      problem:
       strict:
        if(x,y,y) -> y
        if(if(x,y,z),u(),v()) -> if(x,if(y,u(),v()),if(z,u(),v()))
       weak:
        if(true(),x,y) -> x
        if(false(),x,y) -> y
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [v] = 0,
         
         [u] = 0,
         
         [false] = 0,
         
         [if](x0, x1, x2) = x0 + x1 + x2 + 1,
         
         [true] = 0
        orientation:
         if(x,y,y) = x + 2y + 1 >= y = y
         
         if(if(x,y,z),u(),v()) = x + y + z + 2 >= x + y + z + 3 = if(x,if(y,u(),v()),if(z,u(),v()))
         
         if(true(),x,y) = x + y + 1 >= x = x
         
         if(false(),x,y) = x + y + 1 >= y = y
        problem:
         strict:
          if(if(x,y,z),u(),v()) -> if(x,if(y,u(),v()),if(z,u(),v()))
         weak:
          if(x,y,y) -> y
          if(true(),x,y) -> x
          if(false(),x,y) -> y
        Open