[racket] Redex Reduction rule

Hello, 

I have bought the book on Redex, but i am still in difficulty on the following point :

- I have defined a grammar describing processus (obtained from the unfolding of Petri nets).
- I am blocked on the definition of a firing rule allowing to fire an event e_i when a set of condition ⊕ b_1 b_2 ... is present.

(define-language Process-lang
  [n variable bool b e (¬ n)] ; node
  [bool t f] ; boolean
  [e variable (¬ e)] ; event
  [b variable (¬ b)] ; condition
  [on ⊕ ⊥]  ; n-nary operators (building operator and exclusion)
  [o2 ≺]  ; binary operators (causality)

; process  
 [P variable (⊕ Q ... )] 
  [Q variable P n] 
  [C-P (⊕ C-P P) (⊕ P C-P) hole]

; Conflicts  
 [X variable (⊥ Y ... )] 
  [Y variable X n ] 
  [C-X (⊥ C-X P) (⊥ P C-X) hole]  

; Expression  
  [E variable (on F ...) (b o2 e) (P o2 X)]
  [F variable E P ]
  [C-E (on C-E E) (on E C-E) (E o2 C-E) (C-E o2 E) hole]
)

(define Process-red
  (reduction-relation
   Process-lang

...

 (--> (in-hole C-E (⊕ b_1  ... E_1 ... ((⊕ b_2 ...) ≺ n) E_2 ...))
       (in-hole C-E  ( ?????.....?????? ?) "Caus_1"))
....

I want to find a rule allowing to reduce


(⊕
 b_4
 b_2
 b_3
 (b_2 ≺ (⊥ e_3 e_2))
 (e_2 ≺ b_6)
 (e_6 ≺ b_7)
 (b_7 ≺ e_7)
 (e_4 ≺ b_5)
 (b_5 ≺ e_5)
 (b_3 ≺ (⊥ e_4 e_6))
 ((⊕ b_3 b_6) ≺ e_6)
 ((⊕ b_3 b_4) ≺ e_4))


IN 

(⊕
 e_4
 b_2
 (b_2 ≺ (⊥ e_3 e_2))
 (e_2 ≺ b_6)
 (e_6 ≺ b_7)
 (b_7 ≺ e_7)
 (e_4 ≺ b_5)
 (b_5 ≺ e_5)
 (b_3 ≺ (⊥ e_4 e_6))
 ((⊕ b_3 b_6) ≺ e_6)
 )


b_3 and b_4 have been used to produce e_4

Respectuously, 


(joined the entire files)
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Redex_Unf_1.3.rkt
Type: application/octet-stream
Size: 9217 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20121001/23ef4ada/attachment-0002.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: testRedex.rkt
Type: application/octet-stream
Size: 4076 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20121001/23ef4ada/attachment-0003.obj>
-------------- next part --------------

*******************************************************
David Delfieu, tel : 02 40 90 50 45			
EC à Polytech'Nantes - Département Génie Électrique 
Site de Gavy, 44603 Saint Nazaire Cedex		
Chercheur à L'IRCCyN						
*******************************************************