[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

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


  (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