This paper describes how to verify get level arithmetic designs as RT level. In our method, each bit of output is represented by a multiplexer based structure of linear integer equations, and RT level properties are directly applied to this representation. This reduces the need for large BDD or BMD data structures and uses far less memory. For this implementation, we use a canonical form of linear TED [1].