Hi, I'd like to try converting the equality to SUBSET form by using
Pred_setTheory.SUBSET_ANTISYM (THEOREM) --------------------------------------- |- !s t. s SUBSET t /\ t SUBSET s ==> (s = t) and then use property like topology_hvgTheory.BIGUNION_MONO_IMAGE (THEOREM) [1] ------------------------------------------------ |- (!x. x IN s ==> f x SUBSET g x) ==> BIGUNION (IMAGE f s) SUBSET BIGUNION (IMAGE g s) This way you can figure out the relation between 'f' and 'g'... [1] http://hvg.ece.concordia.ca/code/hol/DFT/index.php On Sat, Sep 15, 2018 at 4:27 PM Chun Tian (binghe) <binghe.l...@gmail.com> wrote: > Hi, > > I have a need to prove that, for two certain functions f, (g :num->’a set) > > BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num)) > > Following its informal proof, it seems only possible to prove the > following result (by induction) first: > > !(n :num). BIGUNION (IMAGE f (count n)) = BIGUNION (IMAGE g (count > n)) > > but once I got this intermediate result, how I can reach to the original > statement? Is there any other assumption needed for going from finite to > infinite union? > > Thanks, > > Chun Tian > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > -- Waqar Ahmad, Ph.D. Post Doc at Hardware Verification Group (HVG) Department of Electrical and Computer Engineering Concordia University, QC, Canada Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
