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; Wed, 12 Jul 1995 17:31:47 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA076605248; Wed, 12 Jul 1995 10:07:28 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from valhalla.cs.wright.edu by leopard.cs.byu.edu with SMTP (1.37.109.15/16.2) id AA076565246; Wed, 12 Jul 1995 10:07:26 -0600 Received: by valhalla.cs.wright.edu; id AA15188; Wed, 12 Jul 1995 12:08:34 -0400 From: Robert Eastham Received: (reastham@localhost) by violin.cs.wright.edu (8.6.12/8.6.9) id MAA21436 for info-hol@lal.cs.byu.edu; Wed, 12 Jul 1995 12:10:26 -0400 Date: Wed, 12 Jul 1995 12:10:26 -0400 Message-Id: <199507121610.MAA21436@violin.cs.wright.edu> To: info-hol@leopard.cs.byu.edu Subject: Conditionals How do I handle proofs which contain conditionals? For example, I am left with a subgoal: !t. out(SUC t) = inp t /\ inp(SUC t) -------------------------------------- !t. out t = ((t=0) => F | (inp (t-SUC 0))) /\ inp t How do I finish this proof? A rewrite with the assumptions does not finish this. Bob Eastham reastham@valhalla.cs.wright.edu