How about the following? `∀n. n ≤ C' ⇒ n ≠ w` by METIS_TAC []
(This is what Michael suggested...) Cheers, Magnus On 13 May 2014 10:08, masoume tajvidi <mas.tajv...@gmail.com> wrote: > Thank you all for your quick response. > Actually all these Tactics work but they are so smart that disappear what I > want to stay there in the assumptions( ∀n. n ≤ C' ⇒ n ≠ w). > I assume I need a very basic Tactic for exactly this aim and no more > simplification. > Cheers, > Masoumeh > > > On Tue, May 13, 2014 at 6:35 PM, Magnus Myreen <magnus.myr...@cl.cam.ac.uk> > wrote: >> >> Hi Masoume, >> >> Have you tried RES_TAC? I think RES_TAC should get you ∀n. n ≤ C' ⇒ n >> ≠ w as an assumption. >> >> Cheers, >> Magnus >> >> >> On 13 May 2014 09:01, masoume tajvidi <mas.tajv...@gmail.com> wrote: >> > Hi , >> > I have a subgoal like this: >> > >> > F >> > ------------------------------------ >> > 0. (winner' = w) ⇒ (winner = w) >> > 1. Max_vote C' v' = (winner,max) >> > 2. Max_vote C' v = (winner',max') >> > 3. LENGTH v' = LENGTH v >> > 4. w ≠ 0 >> > 5. ∀n. n < LENGTH v ⇒ (EL n v' = w) ∨ (EL n v = EL n v') >> > 6. Count w v > max' >> > 7. T >> > 8. Count w v' = max >> > 9. SUC C' = w >> > 10. Count w v' ≥ Count w v >> > 11. winner' ≤ C' >> > 12. winner ≤ C' >> > 13. (SUC C' = w) ⇒ ∀n. n ≤ C' ⇒ n ≠ w >> > >> > I need to reach ∀n. n ≤ C' ⇒ n ≠ w as another assumption. >> > I think from Assumption 9 and 13 it is inferable, but do not know what >> > Tactic to use. >> > Could anybody suggest me some Tactics? >> > >> > Thank you:) >> > >> > >> > >> > >> > ------------------------------------------------------------------------------ >> > "Accelerate Dev Cycles with Automated Cross-Browser Testing - For FREE >> > Instantly run your Selenium tests across 300+ browser/OS combos. >> > Get unparalleled scalability from the best Selenium testing platform >> > available >> > Simple to use. Nothing to install. Get started now for free." >> > http://p.sf.net/sfu/SauceLabs >> > _______________________________________________ >> > hol-info mailing list >> > hol-info@lists.sourceforge.net >> > https://lists.sourceforge.net/lists/listinfo/hol-info >> > > > ------------------------------------------------------------------------------ "Accelerate Dev Cycles with Automated Cross-Browser Testing - For FREE Instantly run your Selenium tests across 300+ browser/OS combos. Get unparalleled scalability from the best Selenium testing platform available Simple to use. Nothing to install. Get started now for free." http://p.sf.net/sfu/SauceLabs _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
