close {
\assumes ( b ==> )
\find ( ==> b )
\closegoal
\heuristics (closure )
\displayname "close"
};defined in: propRule.key Line: 22 Offset :4closeAntec {
\assumes ( ==> b )
\find ( b ==> )
\closegoal
\displayname "close"
};defined in: propRule.key Line: 28 Offset :4closeFalse {
\find ( false ==> )
\closegoal
\heuristics (closure )
};defined in: propRule.key Line: 34 Offset :4closeTrue {
\find ( ==> true )
\closegoal
\heuristics (closure )
};defined in: propRule.key Line: 37 Offset :4replace_known_left {
\assumes ( b ==> )
\find ( b )
\sameUpdateLevel
\replacewith ( true )
\heuristics (replace_known_left )
};defined in: propRule.key Line: 42 Offset :4replace_known_right {
\assumes ( ==> b )
\find ( b )
\sameUpdateLevel
\replacewith ( false )
\heuristics (replace_known_right )
};defined in: propRule.key Line: 49 Offset :4true_left {
\find ( true ==> )
\replacewith ( ==> )
\heuristics (concrete )
};defined in: propRule.key Line: 58 Offset :4false_right {
\find ( ==> false )
\replacewith ( ==> )
\heuristics (concrete )
};defined in: propRule.key Line: 62 Offset :4notLeft {
\find ( ! b ==> )
\replacewith ( ==> b )
\heuristics (alpha )
};defined in: propRule.key Line: 67 Offset :4notRight {
\find ( ==> ! b )
\replacewith ( b ==> )
\heuristics (alpha )
};defined in: propRule.key Line: 71 Offset :4impLeft {
\find ( b -> c ==> )
\replacewith ( ==> b );
\replacewith ( c ==> )
\heuristics (beta )
};defined in: propRule.key Line: 76 Offset :4doubleImpLeft {
\find ( b -> c -> d ==> )
\replacewith ( ==> b );
\replacewith ( ==> c );
\replacewith ( d ==> )
\heuristics (beta )
};defined in: propRule.key Line: 82 Offset :4impRight {
\find ( ==> b -> c )
\replacewith ( b ==> c )
\heuristics (alpha )
};defined in: propRule.key Line: 89 Offset :4andLeft {
\find ( b & c ==> )
\replacewith ( b , c ==> )
\heuristics (alpha )
};defined in: propRule.key Line: 95 Offset :4andRight {
\find ( ==> b & c )
\replacewith ( ==> b );
\replacewith ( ==> c )
\heuristics (beta )
};defined in: propRule.key Line: 99 Offset :4orLeft {
\find ( b | c ==> )
"#b" : \replacewith ( b ==> );
"#c" : \replacewith ( c ==> )
\heuristics (beta )
};defined in: propRule.key Line: 105 Offset :4orRight {
\find ( ==> b | c )
\replacewith ( ==> b , c )
\heuristics (alpha )
};defined in: propRule.key Line: 113 Offset :4equiv_left {
\find ( b <-> c ==> )
\replacewith ( b , c ==> );
\replacewith ( ==> b , c )
\heuristics (beta )
};defined in: propRule.key Line: 118 Offset :4equiv_right {
\find ( ==> b <-> c )
"Case '->'" : \replacewith ( b ==> c );
"Case '<-'" : \replacewith ( c ==> b )
\heuristics (beta )
};defined in: propRule.key Line: 125 Offset :4split_or_strong {
\find ( b | c ==> )
\replacewith ( b ==> );
\replacewith ( c ==> b )
};defined in: propRule.key Line: 147 Offset :4rotate_and {
\find ( b & ( c & d ))
\replacewith ( c & ( b & d ))
};defined in: propRule.key Line: 155 Offset :4rotate_or {
\find ( b | ( c | d ))
\replacewith ( c | ( b | d ))
};defined in: propRule.key Line: 159 Offset :4insert_eqv_once_lr {
\find ( br <-> cr ==> )
\addrules ( insert_eqv {
\find ( br )
\replacewith ( cr )
};)
};defined in: propRule.key Line: 165 Offset :4insert_eqv_once_rl {
\find ( br <-> cr ==> )
\addrules ( insert_eqv {
\find ( cr )
\replacewith ( br )
};)
};defined in: propRule.key Line: 173 Offset :4insert_eqv_lr {
\find ( br <-> cr ==> )
\addrules ( insert_eqv {
\find ( br )
\replacewith ( cr )
\heuristics (simplify )
};)
};defined in: propRule.key Line: 182 Offset :4insert_eqv_rl {
\find ( br <-> cr ==> )
\addrules ( insert_eqv {
\find ( cr )
\replacewith ( br )
\heuristics (simplify )
};)
};defined in: propRule.key Line: 191 Offset :4double_not {
\find ( ! ( ! b ))
\replacewith ( b )
\heuristics (concrete )
};defined in: propRule.key Line: 202 Offset :4concrete_not_1 {
\find ( ! true )
\replacewith ( false )
\heuristics (concrete )
};defined in: propRule.key Line: 207 Offset :4concrete_not_2 {
\find ( ! false )
\replacewith ( true )
\heuristics (concrete )
};defined in: propRule.key Line: 211 Offset :4concrete_impl_1 {
\find ( true -> b )
\replacewith ( b )
\heuristics (concrete )
};defined in: propRule.key Line: 216 Offset :4concrete_impl_2 {
\find ( false -> b )
\replacewith ( true )
\heuristics (concrete )
};defined in: propRule.key Line: 220 Offset :4concrete_impl_3 {
\find ( b -> false )
\replacewith ( ! b )
\heuristics (concrete )
};defined in: propRule.key Line: 224 Offset :4concrete_impl_4 {
\find ( b -> true )
\replacewith ( true )
\heuristics (concrete )
};defined in: propRule.key Line: 228 Offset :4concrete_and_1 {
\find ( true & b )
\replacewith ( b )
\heuristics (concrete )
};defined in: propRule.key Line: 233 Offset :4concrete_and_2 {
\find ( false & b )
\replacewith ( false )
\heuristics (concrete )
};defined in: propRule.key Line: 237 Offset :4concrete_and_3 {
\find ( b & true )
\replacewith ( b )
\heuristics (concrete )
};defined in: propRule.key Line: 241 Offset :4concrete_and_4 {
\find ( b & false )
\replacewith ( false )
\heuristics (concrete )
};defined in: propRule.key Line: 245 Offset :4concrete_or_1 {
\find ( true | b )
\replacewith ( true )
\heuristics (concrete )
};defined in: propRule.key Line: 250 Offset :4concrete_or_2 {
\find ( false | b )
\replacewith ( b )
\heuristics (concrete )
};defined in: propRule.key Line: 254 Offset :4concrete_or_3 {
\find ( b | true )
\replacewith ( true )
\heuristics (concrete )
};defined in: propRule.key Line: 258 Offset :4concrete_or_4 {
\find ( b | false )
\replacewith ( b )
\heuristics (concrete )
};defined in: propRule.key Line: 262 Offset :4concrete_or_5 {
\find ( ( c & b )| ( c & ( ! b )))
\replacewith ( c )
\heuristics (concrete )
\displayname "distr_elim"
};defined in: propRule.key Line: 267 Offset :4concrete_eq_1 {
\find ( true <-> b )
\replacewith ( b )
\heuristics (concrete )
};defined in: propRule.key Line: 274 Offset :4concrete_eq_2 {
\find ( false <-> b )
\replacewith ( ! b )
\heuristics (concrete )
};defined in: propRule.key Line: 278 Offset :4concrete_eq_3 {
\find ( b <-> true )
\replacewith ( b )
\heuristics (concrete )
};defined in: propRule.key Line: 282 Offset :4concrete_eq_4 {
\find ( b <-> false )
\replacewith ( ! b )
\heuristics (concrete )
};defined in: propRule.key Line: 286 Offset :4introduceAxiom {
\add ( cutFormula ==> )
};defined in: propRule.key Line: 298 Offset :4cut_direct {
\find ( cutFormula )
\sameUpdateLevel
"CUT: #cutFormula TRUE" : \replacewith ( true ) \add ( cutFormula ==> );
"CUT: #cutFormula FALSE" : \replacewith ( false ) \add ( ==> cutFormula )
\heuristics (cut_direct )
};defined in: propRule.key Line: 310 Offset :4cut_direct_r {
\find ( ==> b )
\replacewith ( ==> b );
\add ( b ==> )
};defined in: propRule.key Line: 320 Offset :4cut_direct_l {
\find ( b ==> )
\replacewith ( b ==> );
\add ( ==> b )
};defined in: propRule.key Line: 325 Offset :4hide_left {
\find ( b ==> )
\replacewith ( ==> ) \addrules ( insert_hidden {
\add ( b ==> )
};)
};defined in: propRule.key Line: 334 Offset :4hide_right {
\find ( ==> b )
\replacewith ( ==> ) \addrules ( insert_hidden {
\add ( ==> b )
};)
};defined in: propRule.key Line: 343 Offset :4case_distinction_r {
\find ( ==> b )
\addrules ( to_true {
\find ( ==> b )
\replacewith ( ==> true )
\heuristics (simplify )
};);
\addrules ( to_false {
\find ( ==> b )
\replacewith ( ==> false )
\heuristics (simplify )
};)
\displayname "case_distinction"
};defined in: propRule.key Line: 352 Offset :4case_distinction_l {
\find ( b ==> )
\addrules ( to_true {
\find ( b ==> )
\replacewith ( true ==> )
\heuristics (simplify )
};);
\addrules ( to_false {
\find ( b ==> )
\replacewith ( false ==> )
\heuristics (simplify )
};)
\displayname "case_distinction"
};defined in: propRule.key Line: 369 Offset :4