Proof:
InitClass2’ ? Class1Class2’ ? InitClass1’
? <by definition>
# l’<= Max ? l’ = <> ?
# d’<= Max ? # l’ <= Max ? d’ = ran l’
? # d’<= Max ? d’ = ?
This is true iff # l’<= Max, l’ = <>, # d’<= Max, d’ = ran l’
# d’<= Max ? d’ = ?
is a valid sequent, which it is.
Previous slide
Next slide
Back to first slide
View graphic version