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; Tue, 5 Apr 1994 10:26:22 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA24598;
          Tue, 5 Apr 1994 03:12:32 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from lorraine.loria.fr by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA24594;
          Tue, 5 Apr 1994 03:12:28 -0600
Received: from myrtille.loria.fr (myrtille.loria.fr [152.81.6.12]) 
          by lorraine.loria.fr (8.6.5/8.6.5) with ESMTP id LAA16708 
          for <info-hol@leopard.cs.byu.edu>; Tue, 5 Apr 1994 11:13:09 +0200
From: Otmane Ait Mohamed <Othmene.Ait-Mohamed@loria.fr>
Received: from localhost (amohamed@localhost) 
          by myrtille.loria.fr (8.6.4/8.6.4) id LAA11977 
          for info-hol@leopard.cs.byu.edu; Tue, 5 Apr 1994 11:13:32 +0200
Date: Tue, 5 Apr 1994 11:13:32 +0200
Message-Id: <199404050913.LAA11977@myrtille.loria.fr>
To: info-hol@leopard.cs.byu.edu
Subject: recursives defs over sets.


Let f,g:string->* and 
  
     FN:(string)set and

     R:*->*->bool.

I want to define a recursive function over set  by:


  "AND f g  {}      = ?x.~(x IN FN) /\ R (f x) (g x)    

  !S.FINITE S ==>

  AND f g (y INSERT S) = (y IN S) => AND f g S | (R (f y) (g y) /\ AND f g S)"


Has anyone defined such function? I'd appreciate any help or pointers.


Thanks in advance.


--otmane.