wd_Logical_Op_Neg {
\find ( WD ( ! a ))
\replacewith ( WD ( a ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 16 Offset :4wd_Logical_Op_And {
\find ( WD ( ( a & b )<< l >> ))
\varcond \replacewith ( WD ( a )& WD ( b ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 27 Offset :4wd_Logical_Op_AndSC {
\find ( WD ( ( ( a & b )<< l >> )))
\varcond \replacewith ( WD ( a )& ( a -> WD ( b )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 41 Offset :4wd_Logical_Op_Or {
\find ( WD ( ( a | b )<< l >> ))
\varcond \replacewith ( WD ( a )& WD ( b ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 55 Offset :4wd_Logical_Op_OrSC {
\find ( WD ( ( ( a | b )<< l >> )))
\varcond \replacewith ( WD ( a )& ( ! a -> WD ( b )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 69 Offset :4wd_Logical_Op_Imp {
\find ( WD ( ( a -> b )))
\replacewith ( WD ( a )& ( a -> WD ( b )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 83 Offset :4wd_Logical_Op_Eqv {
\find ( WD ( ( a <-> b )))
\replacewith ( WD ( a )& WD ( b ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 94 Offset :4wd_Logical_Op_Cond_Expr {
\find ( wd ( \if ( a )\then ( s )\else ( t )))
\replacewith ( WD ( a )& ( a -> wd ( s ))& ( ! a -> wd ( t )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 105 Offset :4wd_Logical_Op_Cond_Form {
\find ( WD ( \if ( a )\then ( b )\else ( c )))
\replacewith ( WD ( a )& ( a -> WD ( b ))& ( ! a -> WD ( c )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 116 Offset :4wd_Logical_Quant_All {
\find ( WD ( \forall i ; a ))
\replacewith ( \forall i ; WD ( a ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 157 Offset :4wd_Logical_Quant_Exist {
\find ( WD ( \exists i ; a ))
\replacewith ( \forall i ; WD ( a ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 168 Offset :4wd_Logical_Op_Neg {
\find ( WD ( ! a ))
\replacewith ( WD ( a ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 182 Offset :4wd_Logical_Op_And {
\find ( WD ( ( a & b )))
\replacewith ( ( WD ( a )& ! a )| ( WD ( b )& ! b )| ( WD ( a )& WD ( b )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 193 Offset :4wd_Logical_Op_Or {
\find ( WD ( ( a | b )))
\replacewith ( ( WD ( a )& a )| ( WD ( b )& b )| ( WD ( a )& WD ( b )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 204 Offset :4wd_Logical_Op_Imp {
\find ( WD ( ( a -> b )))
\replacewith ( ( WD ( a )& ! a )| ( WD ( b )& b )| ( WD ( a )& WD ( b )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 215 Offset :4wd_Logical_Op_Eqv {
\find ( WD ( ( a <-> b )))
\replacewith ( WD ( a )& WD ( b ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 226 Offset :4wd_Logical_Op_Cond_Expr {
\find ( wd ( \if ( a )\then ( s )\else ( t )))
\replacewith ( ( WD ( a )& wd ( s )& a )| ( WD ( a )& wd ( t )& ! a )| ( wd ( s )& wd ( t )& ( s = t )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 237 Offset :4wd_Logical_Op_Cond_Form {
\find ( WD ( \if ( a )\then ( b )\else ( c )))
\replacewith ( ( WD ( a )& WD ( b )& a )| ( WD ( a )& WD ( c )& ! a )| ( WD ( b )& WD ( c )& ( b <-> c )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 248 Offset :4wd_Logical_Op_ExCond_Expr {
\find ( wd ( \ifEx j ; ( a )\then ( s )\else ( t )))
\varcond \replacewith ( ( \exists j ; ( WD ( a )& wd ( s )& a & ( ( wellOrderLeqInt ( jPrime , j )& ( jPrime != j ))-> {\subst j ; jPrime } ( WD ( a )& ! a ))))| ( \forall j ; ( WD ( a )& wd ( t )& ! a ))| ( \forall j ; ( wd ( s )& wd ( t )& ( s = t ))))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 259 Offset :4wd_Logical_Op_ExCond_Form {
\find ( WD ( \ifEx j ; ( a )\then ( b )\else ( c )))
\varcond \replacewith ( ( \exists j ; ( WD ( a )& WD ( b )& a & ( ( wellOrderLeqInt ( jPrime , j )& ( jPrime != j ))-> {\subst j ; jPrime } ( WD ( a )& ! a ))))| ( \forall j ; ( WD ( a )& WD ( c )& ! a ))| ( \forall j ; ( WD ( b )& WD ( c )& ( b <-> c ))))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 278 Offset :4wd_Logical_Quant_All {
\find ( WD ( \forall i ; a ))
\replacewith ( ( \exists i ; ( WD ( a )& ! a ))| ( \forall i ; WD ( a )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 297 Offset :4wd_Logical_Quant_Exist {
\find ( WD ( \exists i ; a ))
\replacewith ( ( \exists i ; ( WD ( a )& a ))| ( \forall i ; WD ( a )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 308 Offset :4wd_T_Logical_Op_Neg {
\find ( T ( ! a ))
\replacewith ( F ( a ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 322 Offset :4wd_F_Logical_Op_Neg {
\find ( F ( ! a ))
\replacewith ( T ( a ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 333 Offset :4wd_T_Logical_Op_And {
\find ( T ( ( a & b )))
\replacewith ( T ( a )& T ( b ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 344 Offset :4wd_F_Logical_Op_And {
\find ( F ( ( a & b )))
\replacewith ( F ( a )| F ( b ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 355 Offset :4wd_T_Logical_Op_Or {
\find ( T ( ( a | b )))
\replacewith ( T ( a )| T ( b ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 366 Offset :4wd_F_Logical_Op_Or {
\find ( F ( ( a | b )))
\replacewith ( F ( a )& F ( b ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 377 Offset :4wd_T_Logical_Op_Imp {
\find ( T ( ( a -> b )))
\replacewith ( F ( a )| T ( b ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 388 Offset :4wd_F_Logical_Op_Imp {
\find ( F ( ( a -> b )))
\replacewith ( T ( a )& F ( b ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 399 Offset :4wd_T_Logical_Op_Eqv {
\find ( T ( ( a <-> b )))
\replacewith ( ( T ( a )& T ( b ))| ( F ( a )& F ( b )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 410 Offset :4wd_F_Logical_Op_Eqv {
\find ( F ( ( a <-> b )))
\replacewith ( ( T ( a )& F ( b ))| ( F ( a )& T ( b )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 421 Offset :4wd_Logical_Op_Cond_Expr {
\find ( wd ( \if ( a )\then ( s )\else ( t )))
\replacewith ( ( T ( a )& wd ( s ))| ( F ( a )& wd ( t ))| ( wd ( s )& wd ( t )& ( s = t )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 432 Offset :4wd_T_Logical_Op_Cond_Form {
\find ( T ( \if ( a )\then ( b )\else ( c )))
\replacewith ( ( T ( a )& T ( b ))| ( F ( a )& T ( c ))| ( T ( b )& T ( c )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 443 Offset :4wd_F_Logical_Op_Cond_Form {
\find ( F ( \if ( a )\then ( b )\else ( c )))
\replacewith ( ( T ( a )& F ( b ))| ( F ( a )& F ( c ))| ( F ( b )& F ( c )))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 454 Offset :4wd_Logical_Op_ExCond_Expr {
\find ( wd ( \ifEx j ; ( a )\then ( s )\else ( t )))
\varcond \replacewith ( ( \exists j ; ( T ( a )& wd ( s )& ( ( wellOrderLeqInt ( jPrime , j )& ( jPrime != j ))-> {\subst j ; jPrime } F ( a ))))| ( \forall j ; ( F ( a )& wd ( t )))| ( \forall j ; ( wd ( s )& wd ( t )& ( s = t ))))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 465 Offset :4wd_T_Logical_Op_ExCond_Form {
\find ( T ( \ifEx j ; ( a )\then ( b )\else ( c )))
\varcond \replacewith ( ( \exists j ; ( T ( a )& T ( b )& ( ( wellOrderLeqInt ( jPrime , j )& ( jPrime != j ))-> {\subst j ; jPrime } F ( a ))))| ( \forall j ; ( F ( a )& T ( c )))| ( \forall j ; ( T ( b )& T ( c ))))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 484 Offset :4wd_F_Logical_Op_ExCond_Form {
\find ( F ( \ifEx j ; ( a )\then ( b )\else ( c )))
\varcond \replacewith ( ( \exists j ; ( T ( a )& F ( b )& ( ( wellOrderLeqInt ( jPrime , j )& ( jPrime != j ))-> {\subst j ; jPrime } F ( a ))))| ( \forall j ; ( F ( a )& F ( c )))| ( \forall j ; ( F ( b )& F ( c ))))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 503 Offset :4wd_T_Logical_Quant_All {
\find ( T ( \forall i ; a ))
\replacewith ( \forall i ; T ( a ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 522 Offset :4wd_F_Logical_Quant_All {
\find ( F ( \forall i ; a ))
\replacewith ( \exists i ; F ( a ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 533 Offset :4wd_T_Logical_Quant_Exist {
\find ( T ( \exists i ; a ))
\replacewith ( \exists i ; T ( a ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 544 Offset :4wd_F_Logical_Quant_Exist {
\find ( F ( \exists i ; a ))
\replacewith ( \forall i ; F ( a ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 555 Offset :4wd_Y_Split {
\find ( WD ( a ))
\varcond \replacewith ( T ( a )| F ( a ))
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 568 Offset :4wd_T_Resolve {
\find ( T ( a ))
\varcond \replacewith ( WD ( a )& a )
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 582 Offset :4wd_F_Resolve {
\find ( F ( a ))
\varcond \replacewith ( WD ( a )& ! a )
\heuristics (simplify )
};defined in: wdFormulaRules.key Line: 596 Offset :4