PPT Slide
d: P Person
p?: Person
DoEnter1 (Enter1 ? Success) ? Full1 ? AlreadyPresent1
To show that DoEnter1 is total we calculate PreDoEnter1
PreDoEnter1
# d <= Max
Previous slide
Next slide
Back to first slide
View graphic version