On Thu, 10 Mar 2011 03:39:33 Alexander Krauss wrote: > In such cases it is often easier to give a "purely logical" > definition using definite description in the style of > "l_c_p S = (THE xs. > (ALL ys : s. is_suffix xs ys) > & (EX ys : s. ALL x. ~ is_suffix (x # xs) ys))" I think you want to switch the quantifiers in the the last line to give & (ALL x. EX ys : s. ~ is_suffix (x # xs) ys))" Otherwise "l_c_p s" is only well-defined when the longest common suffix is also an element of s. Also, it looks like you put a capital S in the first line, and lower-case s elsewhere. Tim <><
Description: This is a digitally signed message part.