[racket] Symbolic expression, reduction, equivalence, ....

Hello

I am defining a new algebra with internal compositional laws over symbolic elements.

After the definition of the properties of the operators, I would to express well formed formula (wff) in that algebra, which are symbolic expression :
(e1 \oplus e2) \perp e3   : for example.

I would like to apply theorem reductions on theses wff, pattern matching, and prove that reduced expressions are equivalent.

Could you suggest a package which could bring me some interesting functions ?

What type of structure could you suggest me to store a wff :
mlist, vector, sets, ...

Best regards, David.

*******************************************************
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						
*******************************************************