Excellent , That works !
Thank you
On Tue, May 13, 2014 at 7:24 PM, Magnus Myreen
<magnus.myr...@cl.cam.ac.uk>wrote:
> 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
