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** F FB /\*
* mux_list_imp (TL (num_BV_f (SUC (LENGTH y)) (BV_n (not_0 c) + 1)))
c** F FC /\*
* Adder_imp_n (LENGTH y + LENGTH y)*
* (num_BV_f (LENGTH FA + LENGTH FB) (BV_n FA * BV_n FB))*
* (make_list_F (LENGTH y) ++ FC) F y co) <=>*
* (co :: y =*
* (num_BV_f (SUC (LENGTH y + LENGTH y)) (BV_n a * BV_n b + BV_n c))) *
* ------------------------------------*
* 0. LENGTH a = LENGTH y*
* 1. LENGTH b = LENGTH y*
* 2. LENGTH c = LENGTH y*
* 3. !n a.*
* num_BV_f (SUC n) a =*
* HD (num_BV_f (SUC n) a)::TL (num_BV_f (SUC n) a)*
* : proof*
In above code, i want to apply the verified theorem
*mux_list_thm;*
*> val it =*
* |- !a b sel y.*
* (LENGTH b = LENGTH a) /\ (LENGTH y = LENGTH a) ==>*
* (mux_list_imp a b sel y <=> mux_list_spec a b sel y) : thm*
Now the problem is that i dont know length of FA. FB and FC in the above
goal to apply the *mux_lixt_thm. *
How can i find or describe its length and apply the above theorem to
simplify my goal
kindly reply me soon.
thanks a lot
------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
