Applicability of Enter2
Prove: pre Enter1 ? Class1Class2 ? pre Enter2 is a theorem of FOL
# d<= Max ? # l <= Max ? d = ran l
This is a theorem of FOL iff the following is a valid sequent:
#d < Max, p?? d, # d<= Max, # l <= Max, d = ran l
# l < Max ? p?? ran l
-
- # l < Max follows from #d < Max, d = ran l and # l = # ran l where
# l = # ran l follows as l doesn’t contain duplicates.
- p?? ran l follows from p?? d and d = ran l