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
