I agree: your theorem is hard to prove because you don't have enough
information about FA etc. Can you prove that
mux_list_imp a b sel y ==> (LENGTH y = something)
If you can't, why not adjust mux_list_imp's definition so that you can?
Similarly, it would seem reasonable to have the same
Dear all
Is it possible to specify length of bool list of the existential quantifier.
I have following proof
* (?FA FB FC.*
* mux_list_imp (TL (num_BV_f (SUC (LENGTH y)) (BV_n (not_0 a) + 1)))
a** F FA /\*
* mux_list_imp (TL (num_BV_f (SUC (LENGTH y)) (BV_n (not_0 b) + 1)))
b**
