Hi,
I've a question on proving set subset relation, and apply MATCH to set.
Here's a goal:
?la ins. ins IN c /\ INS_SPEC lq ins la
------------------------------------
0. !lq.
lq IN BIGUNION {run_to i lp c | i < k} ==>
?la ins. ins IN c /\ INS_SPEC lq ins la
1. i < k
2. lq IN BIGUNION {run_to i' lp c | i' < i}
Obviously, if I prove BIGUNION {run_to i' lp c | i' < i}
in 2 is a subset of BIGUNION {run_to i lp c | i < k} in 0 with i < k,
then I can apply a match on the element of the set and solve the goal.
My question is that how I can prove this obvious subset relation between
the two sets and apply or match it to assumption 0 to prove the goal.
Thank you very much.
Lu
------------------------------------------------------------------------------
Come build with us! The BlackBerry(R) Developer Conference in SF, CA
is the only developer event you need to attend this year. Jumpstart your
developing skills, take BlackBerry mobile applications to market and stay
ahead of the curve. Join us from November 9 - 12, 2009. Register now!
http://p.sf.net/sfu/devconference
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
