Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 16 Aug 1994 20:44:18 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA09397; Tue, 16 Aug 1994 13:39:32 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA09393; Tue, 16 Aug 1994 13:39:28 -0600 Received: from toadflax.cs.ucdavis.edu (toadflax.cs.ucdavis.edu [128.120.56.188]) by dworshak.cs.uidaho.edu (8.6.9/1.0) with SMTP id MAA18620 for ; Tue, 16 Aug 1994 12:35:10 -0700 Received: from ice.cs.ucdavis.edu by toadflax.cs.ucdavis.edu (4.1/UCD.CS.2.5) id AA07504; Tue, 16 Aug 94 12:35:01 PDT Received: by ice.cs.ucdavis.edu (5.65/UCD.CS.2.5) id AA21851; Tue, 16 Aug 1994 12:34:59 -0700 Date: Tue, 16 Aug 1994 12:34:59 -0700 From: shaw@cs.ucdavis.edu (Rob Shaw) Message-Id: <9408161934.AA21851@ice.cs.ucdavis.edu> To: info-hol@cs.uidaho.edu Subject: Why the genvar's ? I don't understand why genvar's are being created. Consider this goal: set_goal(["x < y"; "y <= x"],"F");; "F" 2 ["y <= x" ] 1 ["x < y" ] () : void Run time: 0.0s ----------- And here's a perfectly vaild theorem that should allow me to rewrite the term F: SYM (EQF_INTRO (SPECL ["x:num"; "y:num"] LESS_EQ_ANTISYM));; |- F = x < y /\ y <= x Run time: 0.0s Intermediate theorems generated: 7 ----------- But when I try to rewrite with this theorem, it creates genvars: e( REWRITE_TAC [SYM (EQF_INTRO (SPECL ["x:num"; "y:num"] LESS_EQ_ANTISYM))] );; OK.. "GEN%VAR%557 < GEN%VAR%558 /\ GEN%VAR%558 <= GEN%VAR%557" 2 ["y <= x" ] 1 ["x < y" ] Why don't I get the new goal "(x < y) /\ (y <= x)" ? Thanx! Rob