Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <24717-0@swan.cl.cam.ac.uk>; Thu, 23 Jul 1992 19:17:36 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA10469; Thu, 23 Jul 92 11:07:06 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from leopard.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) id AA10464; Thu, 23 Jul 92 11:07:02 -0700 Received: by leopard.cs.uidaho.edu (16.7/1.34) id AA27324; Thu, 23 Jul 92 11:10:21 -0700 From: weiss@edu.uidaho.cs.leopard (Phil Weiss) Message-Id: <9207231810.AA27324@leopard.cs.uidaho.edu> Subject: Equivalence of GSPEC(\x. ( ,F)) and EMPTY To: info-hol@edu.uidaho.cs.ted (HOL Mailing List) Date: Thu, 23 Jul 92 11:10:21 PDT Mailer: Elm [revision: 66.33] Could anyone tell me if they have managed to prove GSPEC (\x. (, F)) = EMPTY for all expressions? Or if they have written a conversion? The only way I have found which is usable in all cases is three steps REWRITE_TAC [GSPEC_DEF] BETA_TAC REWRITE_TAC [PAIR_EQ] but this has side effects. Any help would be appreciated. Phil. -- Philip Weiss Laboratory for Applied Logic weiss@leopard.cs.uidaho.edu (Disclaimer: My views are not their views) weiss872@snake.cs.uidaho.edu