wd_Constant_Formula {
\find ( WD ( ( f )<< l >> ))
\varcond \replacewith ( true )
\heuristics (simplify )
};defined in: wdGeneralRules.key Line: 14 Offset :4wd_Constant_Term {
\find ( wd ( ( t )<< l >> ))
\varcond \replacewith ( true )
\heuristics (simplify )
};defined in: wdGeneralRules.key Line: 29 Offset :4wd_Undef_Formula {
\find ( WD ( ( f )<< l >> ))
\varcond \replacewith ( false )
\heuristics (simplify )
};defined in: wdGeneralRules.key Line: 44 Offset :4wd_Undef_Term {
\find ( wd ( ( t )<< l >> ))
\varcond \replacewith ( false )
\heuristics (simplify )
};defined in: wdGeneralRules.key Line: 59 Offset :4wd_Subst_Formula {
\find ( WD ( {\subst v ; u } f ))
\replacewith ( wd ( u )& {\subst v ; u } WD ( f ))
\heuristics (simplify )
};defined in: wdGeneralRules.key Line: 74 Offset :4wd_T_Subst_Formula {
\find ( T ( {\subst v ; u } f ))
\replacewith ( wd ( u )& {\subst v ; u } T ( f ))
\heuristics (simplify )
};defined in: wdGeneralRules.key Line: 85 Offset :4wd_F_Subst_Formula {
\find ( F ( {\subst v ; u } f ))
\replacewith ( wd ( u )& {\subst v ; u } F ( f ))
\heuristics (simplify )
};defined in: wdGeneralRules.key Line: 96 Offset :4wd_Subst_Term {
\find ( wd ( {\subst v ; u } t ))
\replacewith ( wd ( u )& {\subst v ; u } wd ( t ))
\heuristics (simplify )
};defined in: wdGeneralRules.key Line: 107 Offset :4wd_Type_Cast {
\find ( wd ( alpha :: cast ( t )))
\replacewith ( wd ( t )& ( alpha :: instance ( t )= TRUE ))
\heuristics (simplify )
};defined in: wdGeneralRules.key Line: 118 Offset :4wd_Type_ExactInstance {
\find ( wd ( alpha :: exactInstance ( t )))
\replacewith ( wd ( t ))
\heuristics (simplify )
};defined in: wdGeneralRules.key Line: 129 Offset :4wd_Type_Instance {
\find ( wd ( alpha :: instance ( t )))
\replacewith ( wd ( t ))
\heuristics (simplify )
};defined in: wdGeneralRules.key Line: 140 Offset :4wd_Pair {
\find ( wd ( pair ( s , t )))
\replacewith ( wd ( s )& wd ( t ))
\heuristics (simplify )
};defined in: wdGeneralRules.key Line: 151 Offset :4wd_Equality_Pred {
\find ( WD ( ( s = t )))
\replacewith ( wd ( s )& wd ( t ))
\heuristics (simplify )
};defined in: wdGeneralRules.key Line: 162 Offset :4