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);
          Mon, 14 Sep 1992 18:39:30 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA00653;
          Mon, 14 Sep 92 10:13:52 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Ucthpx.UCT.AC.ZA by ted.cs.uidaho.edu (16.6/1.34) id AA00637;
          Mon, 14 Sep 92 10:11:40 -0700
Received: by ucthpx.uct.ac.za (/\==/\ Smail3.1.24.1 #24.2) id m0mUJuO-000NyrC;
          Mon, 14 Sep 92 19:08 SAST
Received: by elc.mth.uct.ac.za (4.1/SMI-4.1) id AA01107;
          Mon, 14 Sep 92 19:03:03+020
From: gavan@za.ac.uct.mth.elc (Gavan Tredoux)
Message-Id: <9209141703.AA01107@elc.mth.uct.ac.za>
Subject: Ordinals and well founded sets
To: info-hol@edu.uidaho.cs.ted
Date: Mon, 14 Sep 92 19:03:03 EET
X-Mailer: ELM [version 2.3 PL11]

Does anyone have a theory of ordinals and/or well-founded
sets available for reuse? This may be of general interest.

I'm formulating Hoare rules for unbounded non-determinism
in programs, proving termination.

Thanks
Gavan Tredoux
FACCS Lab
University of Cape Town