CodePlexProject Hosting for Open Source Software

1

Vote
At line 272 in the file NewBoundedBuffer occurs the proof step:

```
<2> (a (+) 1) (-) b = (a (+) 1) (+) OMinus(b)
BY OMinusDef, Z3 DEF ZN
```

which expands to the obligation:```
ASSUME NEW CONSTANT Msg,
...
ASSUME 2 * NatInductiveDefConclusion \in Nat \ {0}
PROVE \A a_1, b_1 \in 0..2 * NatInductiveDefConclusion - 1 :
a_1 (-) b_1 = a_1 (+) OMinus(b_1)
PROVE (a (+) 1) (-) b = a (+) 1 (+) OMinus(b)
```

The theorem OMinusDef is defined in the file IntegersModN.tla as:`THEOREM OMinusDef == \A a, b \in ZN : a (-) b = a (+) OMinus(b)`

and in there, ZN is defined as:`ZN == 0..(N-1)`

Since IntegersModN is instantiated via:`INSTANCE IntegersModN WITH N <- 2*N`

we would expect the obligation to contain `0..2*N-1`

, not `0..2*NatInductiveDefConclusion-1`

.
## comments