On Thu, May 29, 2008 at 7:09 PM, Jerome <jerome@xxxxxxxxxxxxxx> wrote: > I'm cc'ing the list to try and get our conversation back over > there. I've attached a dump of the original 'curry' theory, as well as > the 'dualton' theory you were working on, for background. Okay. The more eyes the better. > The first two don't really help; I think the third one has potential > though. One that I'm working on is: > > sets_lemmas_ext[T: TYPE]: THEORY > BEGIN > a, b: VAR T > A: VAR non_empty_finite_set[T] > > doubleton?(A): bool = singleton?(rest(A)) > > remove_is_element: LEMMA > FORALL (a, b: (A) | a /= b): doubleton?(A) IMPLIES > remove(a, A) = singleton(b) AND remove(b, A) = singleton(a) > END sets_lemmas_ext > > Does this make sense? I get some dead-ends when trying to prove it, so > I may be missing something. Essentially, however, in the curry_x proof > it would be ideal to bring something like this in and instantiate it > with "k!1" and "choose(U!1)". What do you think of the version I'm attaching here? I like "doubleton". It makes more sense than "dualton". :-) -- Jerry James http://loganjerry.googlepages.com/
Attachment:
doubleton.pvs
Description: Binary data
Attachment:
doubleton.prf
Description: Binary data