boolean_equal {
\find ( bo = bo )
\replacewith ( true )
\heuristics (simplify_boolean , concrete )
};defined in: booleanRules.key Line: 10 Offset :4boolean_equal_2 {
\find ( b1 = TRUE <-> b2 = TRUE )
\replacewith ( b1 = b2 )
\heuristics (simplify_boolean , concrete )
\displayname "boolean_equal"
};defined in: booleanRules.key Line: 16 Offset :4boolean_not_equal_1 {
\find ( TRUE = FALSE )
\replacewith ( false )
\heuristics (simplify_boolean , concrete )
\displayname "boolean_not_equal"
};defined in: booleanRules.key Line: 23 Offset :4boolean_not_equal_2 {
\find ( FALSE = TRUE )
\replacewith ( false )
\heuristics (simplify_boolean , concrete )
\displayname "boolean_not_equal"
};defined in: booleanRules.key Line: 29 Offset :4true_to_not_false {
\find ( bo = TRUE )
\replacewith ( ! bo = FALSE )
};defined in: booleanRules.key Line: 36 Offset :4false_to_not_true {
\find ( bo = FALSE )
\replacewith ( ! bo = TRUE )
\heuristics (simplify_boolean , concrete )
};defined in: booleanRules.key Line: 43 Offset :4boolean_true_commute {
\find ( TRUE = bo )
\replacewith ( bo = TRUE )
\heuristics (simplify_boolean )
\displayname "boolean commute"
};defined in: booleanRules.key Line: 49 Offset :4boolean_false_commute {
\find ( FALSE = bo )
\replacewith ( bo = FALSE )
\heuristics (simplify_boolean )
\displayname "boolean commute"
};defined in: booleanRules.key Line: 56 Offset :4ex_bool {
\schemaVar \variables boolean x ;
\schemaVar \formula c ;
\find ( \exists x ; c )
\replacewith ( {\subst x ; FALSE } c | {\subst x ; TRUE } c )
\heuristics (boolean_cases )
};defined in: booleanRules.key Line: 63 Offset :4all_bool {
\schemaVar \variables boolean x ;
\schemaVar \formula c ;
\find ( \forall x ; c )
\replacewith ( {\subst x ; FALSE } c & {\subst x ; TRUE } c )
\heuristics (boolean_cases )
};defined in: booleanRules.key Line: 71 Offset :4apply_eq_boolean {
\assumes ( ==> bo = TRUE )
\find ( bo )
\sameUpdateLevel
\replacewith ( FALSE )
\heuristics (apply_equations )
};defined in: booleanRules.key Line: 81 Offset :4apply_eq_boolean_2 {
\assumes ( ==> bo = FALSE )
\find ( bo )
\sameUpdateLevel
\replacewith ( TRUE )
\heuristics (apply_equations )
\displayname "apply_eq_boolean"
};defined in: booleanRules.key Line: 89 Offset :4apply_eq_boolean_rigid {
\schemaVar \term [ rigid ]boolean br ;
\assumes ( ==> br = TRUE )
\find ( br )
\replacewith ( FALSE )
\heuristics (apply_equations )
\displayname "apply_eq_boolean"
};defined in: booleanRules.key Line: 98 Offset :4apply_eq_boolean_rigid_2 {
\schemaVar \term [ rigid ]boolean br ;
\assumes ( ==> br = FALSE )
\find ( br )
\replacewith ( TRUE )
\heuristics (apply_equations )
\displayname "apply_eq_boolean"
};defined in: booleanRules.key Line: 107 Offset :4\lemma ifthenelse_equals {
\schemaVar \formula b , c ;
\find ( \if ( b )\then ( TRUE )\else ( FALSE )= \if ( c )\then ( TRUE )\else ( FALSE ))
\replacewith ( b <-> c )
\heuristics (concrete )
};defined in: booleanRules.key Line: 116 Offset :4\lemma ifthenelse_equals_1 {
\schemaVar \formula b ;
\schemaVar \term boolean c ;
\find ( \if ( b )\then ( TRUE )\else ( FALSE )= c )
\replacewith ( b <-> c = TRUE )
};defined in: booleanRules.key Line: 124 Offset :4\lemma ifthenelse_equals_2 {
\schemaVar \term boolean b ;
\schemaVar \formula c ;
\find ( b = \if ( c )\then ( TRUE )\else ( FALSE ))
\replacewith ( b = TRUE <-> c )
};defined in: booleanRules.key Line: 133 Offset :4