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

Please Help Me



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