[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: YAMAZAKI Takashi <yamazaki@csl.ec.t.kanazawa-u.ac.jp>*Subject*: Re: Please Help Me*From*: Sam Owre <owre@csl.sri.com>*Date*: Mon, 20 Jan 2003 11:48:12 -0800*cc*: pvs-help@csl.sri.com, owre@csl.sri.com*In-Reply-To*: Your message of "Mon, 20 Jan 2003 20:57:52 +0900." <200301202057.52100.yamazaki@csl.ec.t.kanazawa-u.ac.jp>*Sender*: pvs-help-owner@csl.sri.com

I managed to prove it using the prelude lemma "lub_nat" to get at the largest natural less than j where the train is safe, and measure-induct+ so that the induction works from i+1 to i. I'm making no claims that it is the best proof, but here it is: ("" (grind :if-match nil) (lemma "lub_nat") (inst -1 "{i | i < j!1 AND train!1(i) = safe}" "j!1") (("1" (grind :if-match nil) (inst 1 "n!1") (assert) (case "FORALL (k: upto(j!1)): n!1 < k IMPLIES train!1(k) = approaching") (("1" (skosimp) (inst -1 "m!1") (assert)) ("2" (hide 2) (measure-induct+ "j!1 - k" ("k")) (inst -1 "x!1 + 1") (("1" (assert) (inst -8 "x!1") (assert) (inst -5 "x!1") (assert)) ("2" (assert)))))) ("2" (grind)))) Note that using measure-induct+ directly on the original formula leads to an unprovable TCC; this is due to the heuristics used by measure-induct+ to create the induction formula. The case step just provides an alternative equivalent form that works. Sam > I can not prove the following lemma. > > This THEORY is a part of railload crossing. > > =========== > > test: THEORY > BEGIN > > train_state: TYPE = { safe, approaching, crossing} > Train: TYPE = [ nat -> train_state ] > train: VAR Train > i, j, k, m: VAR nat > > > test_lemma: LEMMA > (FORALL i: train(i+1) = approaching IMPLIES > train(i) = approaching OR train(i) = safe) AND > train(0) = safe AND > train(j) = approaching > > IMPLIES > > (EXISTS k: > k < j AND train(k) = safe AND > (FORALL m: > k < m AND m <= j IMPLIES > train(m) = approaching )) > > END test > > =========== > > > Would you mind please telling me about this? > > > Kanazawa Univ ,Japan > YAMAZAKI Takashi >

**References**:**Please Help Me***From:*YAMAZAKI Takashi <yamazaki@csl.ec.t.kanazawa-u.ac.jp>

- Prev by Date:
**Please Help Me** - Next by Date:
**a C function to traverse a list.** - Prev by thread:
**Please Help Me** - Next by thread:
**About an error** - Index(es):