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: 2
  interpretation:
               [0 2]  
   [old](x0) = [2 2]x0,
   
                
   [ok](x0) = x0,
   
                 [0 0]  
   [check](x0) = [0 0]x0,
   
           [3]
   [bot] = [3],
   
               [0  0 ]  
   [new](x0) = [-& -&]x0,
   
               [6  6 ]  
   [top](x0) = [-& -&]x0
  orientation:
                     [6  6 ]     [6  6 ]                 
   top(ok(new(x))) = [-& -&]x >= [-& -&]x = top(check(x))
   
                     [8  8 ]     [6  6 ]                 
   top(ok(old(x))) = [-& -&]x >= [-& -&]x = top(check(x))
   
           [3]    [3 ]             
   bot() = [3] >= [-&] = new(bot())
   
                   [0 0]     [0  0 ]                 
   check(new(x)) = [0 0]x >= [-& -&]x = new(check(x))
   
                   [2 2]     [2 2]                 
   check(old(x)) = [2 2]x >= [2 2]x = old(check(x))
   
                   [2 2]     [0 2]              
   check(old(x)) = [2 2]x >= [2 2]x = ok(old(x))
   
                [0  0 ]     [0  0 ]              
   new(ok(x)) = [-& -&]x >= [-& -&]x = ok(new(x))
   
                [0 2]     [0 2]              
   old(ok(x)) = [2 2]x >= [2 2]x = 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))
  Matrix Interpretation Processor: dim=2
   
   interpretation:
                [2 0]     [2]
    [old](x0) = [0 1]x0 + [0],
    
                    [0]
    [ok](x0) = x0 + [2],
    
                  [1 0]  
    [check](x0) = [1 1]x0,
    
            [0]
    [bot] = [0],
    
                [1 0]  
    [new](x0) = [1 1]x0,
    
                [2 1]     [0]
    [top](x0) = [0 0]x0 + [2]
   orientation:
                      [3 1]    [2]    [3 1]    [0]                
    top(ok(new(x))) = [0 0]x + [2] >= [0 0]x + [2] = top(check(x))
    
            [0]    [0]             
    bot() = [0] >= [0] = new(bot())
    
                    [1 0]     [1 0]                 
    check(new(x)) = [2 1]x >= [2 1]x = new(check(x))
    
                    [2 0]    [2]    [2 0]    [2]                
    check(old(x)) = [2 1]x + [2] >= [1 1]x + [0] = old(check(x))
    
                    [2 0]    [2]    [2 0]    [2]             
    check(old(x)) = [2 1]x + [2] >= [0 1]x + [2] = ok(old(x))
    
                 [1 0]    [0]    [1 0]    [0]             
    new(ok(x)) = [1 1]x + [2] >= [1 1]x + [2] = ok(new(x))
    
                 [2 0]    [2]    [2 0]    [2]             
    old(ok(x)) = [0 1]x + [2] >= [0 1]x + [2] = 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