Investigating Preconditions
As p?? d, then #(d ?{p?}) = #d + 1
Therefore, #d < Max. As, #d < Max ? #d <= Max
Hence we can simplify PreEnter1 to:
PreEnter1
d: P Person
p?: Person
#d <= Max ?
#(d ?{p?}) <= Max ?
#d < Max ?
p?? d
Previous slide
Next slide
Back to first slide
View graphic version