24 #ifndef _cvc3__theory_uf__uf_proof_rules_h_
25 #define _cvc3__theory_uf__uf_proof_rules_h_
Data structure of expressions in CVC3.
virtual Theorem applyLambda(const Expr &e)=0
Beta reduction: |- (lambda x. f(x))(arg) = f(arg)
virtual Theorem relToClosure(const Theorem &rel)=0
virtual Theorem relTrans(const Theorem &t1, const Theorem &t2)=0
virtual Theorem rewriteOpDef(const Expr &e)=0
Replace LETDECL in the operator with the definition.