Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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, 15 Jun 1994 21:21:28 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA16223;
          Wed, 15 Jun 1994 14:11:52 -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 AA16219;
          Wed, 15 Jun 1994 14:11:46 -0600
Received: from scylla.oracorp.com by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA17301;
          Wed, 15 Jun 1994 13:10:20 -0700
Received: from goedel.oracorp.com by oracorp.com (4.1/2.1-ORA Corporation) 
          id AA17384; Wed, 15 Jun 94 16:09:12 EDT
Date: Wed, 15 Jun 94 16:09:09 EDT
From: davidg@oracorp.com
Received: by goedel.oracorp.com (4.1/1.3-ORA Corporation) id AA01289;
          Wed, 15 Jun 94 16:09:09 EDT
Message-Id: <9406152009.AA01289@goedel.oracorp.com>
To: info-hol@cs.uidaho.edu
Subject: Real-time scheduling; DIV, MOD, REM


I'm looking for information about any work that's been done, in HOL,
on proving facts in real-time scheduling theory.  Since the proofs are
often combinatorial in character, and require manipulations with DIV,
MOD, REM, I'm also interested in knowing if there's a well-developed
library of facts about these operators or tactics for simplifying the
expressions in which they occur.  I'm not a subscriber to this
mailing list, so I'd appreciate replies by e-mail.

- David Guaspari
  davidg@oracorp.com