theory Spi_DC_SI imports Spi_Ded_Cons Spi_SI begin end