YES

Problem:
 strict:
  top(ok(new(x))) -> top(check(x))
  top(ok(old(x))) -> top(check(x))
 weak:
  bot() -> new(bot())
  check(new(x)) -> new(check(x))
  check(old(x)) -> old(check(x))
  check(old(x)) -> ok(old(x))
  new(ok(x)) -> ok(new(x))
  old(ok(x)) -> ok(old(x))

Proof:
 Arctic Interpretation Processor:
  dimension: 1
  interpretation:
   [old](x0) = 14x0,
   
   [ok](x0) = 8x0,
   
   [check](x0) = 8x0,
   
   [bot] = 1,
   
   [new](x0) = x0,
   
   [top](x0) = 8x0
  orientation:
   top(ok(new(x))) = 16x >= 16x = top(check(x))
   
   top(ok(old(x))) = 30x >= 16x = top(check(x))
   
   bot() = 1 >= 1 = new(bot())
   
   check(new(x)) = 8x >= 8x = new(check(x))
   
   check(old(x)) = 22x >= 22x = old(check(x))
   
   check(old(x)) = 22x >= 22x = ok(old(x))
   
   new(ok(x)) = 8x >= 8x = ok(new(x))
   
   old(ok(x)) = 22x >= 22x = ok(old(x))
  problem:
   strict:
    top(ok(new(x))) -> top(check(x))
   weak:
    bot() -> new(bot())
    check(new(x)) -> new(check(x))
    check(old(x)) -> old(check(x))
    check(old(x)) -> ok(old(x))
    new(ok(x)) -> ok(new(x))
    old(ok(x)) -> ok(old(x))
  Arctic Interpretation Processor:
   dimension: 2
   interpretation:
                [0 2]  
    [old](x0) = [0 6]x0,
    
               [0  -&]  
    [ok](x0) = [0  6 ]x0,
    
                  [4  2 ]  
    [check](x0) = [-& 6 ]x0,
    
            [0 ]
    [bot] = [-&],
    
                [0  -&]  
    [new](x0) = [-& 1 ]x0,
    
                [0  6 ]  
    [top](x0) = [-& 0 ]x0
   orientation:
                      [6  13]     [4  12]                 
    top(ok(new(x))) = [0  7 ]x >= [-& 6 ]x = top(check(x))
    
            [0 ]    [0 ]             
    bot() = [-&] >= [-&] = new(bot())
    
                    [4  3 ]     [4  2 ]                 
    check(new(x)) = [-& 7 ]x >= [-& 7 ]x = new(check(x))
    
                    [4  8 ]     [4  8 ]                 
    check(old(x)) = [6  12]x >= [4  12]x = old(check(x))
    
                    [4  8 ]     [0  2 ]              
    check(old(x)) = [6  12]x >= [6  12]x = ok(old(x))
    
                 [0  -&]     [0  -&]              
    new(ok(x)) = [1  7 ]x >= [0  7 ]x = ok(new(x))
    
                 [2  8 ]     [0  2 ]              
    old(ok(x)) = [6  12]x >= [6  12]x = ok(old(x))
   problem:
    strict:
     
    weak:
     bot() -> new(bot())
     check(new(x)) -> new(check(x))
     check(old(x)) -> old(check(x))
     check(old(x)) -> ok(old(x))
     new(ok(x)) -> ok(new(x))
     old(ok(x)) -> ok(old(x))
   Qed