Closed bendisposto closed 9 years ago
I had an invariant in a model (mc2 from http://deploy-eprints.ecs.soton.ac.uk/152/3/pomc_paper.zip)
∀i,s·(s∈open ∧ i∈INVARIANTS\invs_to_verify[{s}] ⇒ s ↦ i ∈ truth)
Camille replaced \in by ∈ and I got
∀i,s·(s∈open ∧ i∈INVARIANTS∈vs_to_verify[{s}] ⇒ s ↦ i ∈ truth)
This is a bug in the Unicode Translator (see probparsers project).
I had an invariant in a model (mc2 from http://deploy-eprints.ecs.soton.ac.uk/152/3/pomc_paper.zip)
∀i,s·(s∈open ∧ i∈INVARIANTS\invs_to_verify[{s}] ⇒ s ↦ i ∈ truth)
Camille replaced \in by ∈ and I got
∀i,s·(s∈open ∧ i∈INVARIANTS∈vs_to_verify[{s}] ⇒ s ↦ i ∈ truth)