can we do:
SL = 0 <=> (h0 = 0 AND h1 = 0 AND...)
SL != 0 <=> (h0 != 0 AND h1 != 0 AND ...)
.....
This will assert that if we don't choose the selector as 0, we need EVERYTHING to not be equal to 0
As long as we have the list of possible assignments for each variable and restrict those selections, maybe this is ok?
Instead of individually asserting SL0 = 0 <=> h0 = 0 SL0 = 0 <=> h1 = 0, ...
can we do: SL = 0 <=> (h0 = 0 AND h1 = 0 AND...) SL != 0 <=> (h0 != 0 AND h1 != 0 AND ...) .....
This will assert that if we don't choose the selector as 0, we need EVERYTHING to not be equal to 0 As long as we have the list of possible assignments for each variable and restrict those selections, maybe this is ok?