Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 9 Sep 1993 23:15:19 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA26066; Thu, 9 Sep 93 15:07:58 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from tuminfo2.informatik.tu-muenchen.de by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA26061; Thu, 9 Sep 93 15:07:55 -0700 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <57667>; Fri, 10 Sep 1993 00:07:59 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8081>; Fri, 10 Sep 1993 00:07:45 +0200 From: Konrad Slind To: info-hol@cs.uidaho.edu Subject: jjj proof challenge Message-Id: <93Sep10.000745met_dst.8081@sunbroy14.informatik.tu-muenchen.de> Date: Fri, 10 Sep 1993 00:07:31 +0200 ... and in fact, one wouldn't even have to think about the existential if one noticed, in the "crux" step of the proof: (--`?v. (P v \/ (?w. R w)) /\ ((?z. R z) ==> Q v)`--) ============================= (--`P x`--) (--`Q y`--) that `?w. R w` and `?z. R z` were not only alpha-convertible, but boolean and "v"-free, so that the following invocation gives a particularly simple situation. - e (BOOL_CASES_TAC (--`?w:'b. R w`--) THEN REWRITE_TAC[]); OK.. 2 subgoals: (--`?v. P v`--) ============================= (--`P x`--) (--`Q y`--) (--`?v. Q v`--) ============================= (--`P x`--) (--`Q y`--)