|
From: Osman H. <o_...@en...> - 2006-07-14 18:34:06
|
Hi HOL users, I am trying to prove the following theorem in HOL |- ?(n:num). !(r:real). r < & n It is somewhat related to the REAL_BIGNUM theorem found in the realTheory: |- !r. ?n. r < &n and by looking at this REAL_BIGNUM theorem my goal seems provable: As for every real number there exists a greater 'num' so there must be a 'num' which is greater than the greatest real number. I tried using quite a few different approaches but couldnt succeed so far and the main bottleneck being the fact that the existential quantifier is outside the universal one. Any feedback/clues would be greatly appreciated. Thanks and best regards, --Osman |