Correctness of Enter2

Prove:

pre Enter1 ? ?Class1Class2 ? Enter2 ? Enter2 is a theorem of FOL

#d < Max ? p?? d ?

# d<= Max ? # l <= Max ? d = ran l ?

# d’<= Max ? # l’ <= Max ? d‘ = ran l’ ?

# l < Max ? # l’<= Max ? p?? ran l ? l’ = append(I,<p?>)

? # d < Max ? # d’<= Max ? p?? d ? d’ = d ? {p?}

?

#d < Max , p?? d, d = ran l, # d’<= Max, # l’ <= Max, d‘ = ran l’,

# l < Max, p?? ran l, l’ = append(l,<p?>)

# d < Max ? # d’<= Max ? p?? d ? d’ = d ? {p?}

Previous slide

Back to first slide

View graphic version