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

Reply via email to