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 property be true of the
_spec version.
Michael
On 25 Feb 2016, at 20:53, Sumayya Shiraz
<[email protected]<mailto:[email protected]>> wrote:
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
