theory Spi_Bt_Equiv imports Spi_Bitrace begin end