[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: instantiation




Kim:
 I'm unable to see why that should be a theorem.
Your axioms provide no way of proving that a < b
doesn't hold.  ax0, ax1, ax2 assert a < b for some
a's and b's, and trans allows a < b assertions to be
chained.  But there is no way of obtaining a NOT a < b
assertion from these axioms.  

You perhaps know that the enumerated type generates an
ord function so that ord(a1) = 0, ..., ord(a5) = 4.
This can be used to define a < b as ord(a) < ord(b).
With this definition, all the axioms and the theorem can be
proved using GRIND.  

-Shankar