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
