Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Sat, 19 Dec 1992 13:16:11 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06054;
          Sat, 19 Dec 92 03:09:04 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA06049;
          Sat, 19 Dec 92 03:08:57 -0800
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA11625;
          Sat, 19 Dec 92 03:08:21 -0800
Message-Id: <9212191108.AA11625@maui.cs.ucla.edu>
To: Phil Windley <windley@edu.uidaho.cs.panther>
Subject: Re: Well founded induction
Cc: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list)
Date: Sat, 19 Dec 92 03:08:20 PST
From: chou@edu.ucla.cs

Hi Phil,

Though your original goal cannot be proved by induction directly,
I think the following goal CAN be proved by induction on t:

  ! g t .
    ( ? t1 . (g t1) /\ (t1 <= t) )
     ==>
    ( ? t2 . (g t2) /\ (t2 <= t) /\
             ( ! t' . (t2 < t') /\ (t' <= t) ==> ~(g t') ) /\
	     ( ? s . Temp_Abs g s = t2 ) )

from which your goal follows.

Cheers,
- Ching Tsun