===============================================================================
== This directory contains HOL88 proofs due to Tom Melhan in 1987. They      ==
== were updated for HOL98 by Mike Gordon in 2000 for use in teaching at      ==
== OGI, and they still run in HOL4 (though the compiling preludes could      ==
== perhaps do with some updating).                                           ==
===============================================================================

The definitions are:

 tempabsTheory.Inf 
 |- !sig. Inf sig = !t. ?t'. t < t' /\ sig t' 

 tempabsTheory.when
 |- !sig cntl. sig when cntl = sig o Timeof cntl

 dffTheory.Rise
 |- !s t. Rise s t = ~s t /\ s (t + 1) 

 dffTheory.Dtype
 |- !ck d q.
      Dtype (ck,d,q) = !t. q (t + 1) = (if Rise ck t then d t else q t)
 
 dffTheory.Del
 |- !inp out. Del (inp,out) = !t. out (t + 1) = inp t

The theorem we need is:

  dffTheory.Dtype_correct
  |- !ck.
       Inf (Rise ck) ==>
       !d q. Dtype (ck,d,q) ==> Del (d when Rise ck,q when Rise ck)