\generic G, G2;defined in: ifThenElseRules.key Line: 10 Offset :4\generic G, G2;defined in: ifThenElseRules.key Line: 10 Offset :4 wellOrderLeqInt (int , int ); defined in: ifThenElseRules.key Line: 27 Offset :4ifthenelse_true {
\find ( \if ( true )\then ( then )\else ( else ))
\replacewith ( then )
\heuristics (concrete )
};defined in: ifThenElseRules.key Line: 34 Offset :4ifthenelse_true_for {
\find ( \if ( true )\then ( b )\else ( c ))
\replacewith ( b )
\heuristics (concrete )
\displayname "ifthenelse_true"
};defined in: ifThenElseRules.key Line: 40 Offset :4ifthenelse_false {
\find ( \if ( false )\then ( then )\else ( else ))
\replacewith ( else )
\heuristics (concrete )
};defined in: ifThenElseRules.key Line: 47 Offset :4ifthenelse_false_for {
\find ( \if ( false )\then ( b )\else ( c ))
\replacewith ( c )
\heuristics (concrete )
\displayname "ifthenelse_false"
};defined in: ifThenElseRules.key Line: 53 Offset :4ifthenelse_negated {
\find ( \if ( ! phi )\then ( then )\else ( else ))
\replacewith ( \if ( phi )\then ( else )\else ( then ))
\heuristics (simplify )
};defined in: ifThenElseRules.key Line: 60 Offset :4ifthenelse_negated_for {
\find ( \if ( ! phi )\then ( b )\else ( c ))
\replacewith ( \if ( phi )\then ( c )\else ( b ))
\heuristics (simplify )
\displayname "ifthenelse_negated"
};defined in: ifThenElseRules.key Line: 66 Offset :4ifthenelse_same_branches {
\find ( \if ( phi )\then ( then )\else ( then ))
\replacewith ( then )
\heuristics (concrete )
};defined in: ifThenElseRules.key Line: 73 Offset :4ifthenelse_same_branches_for {
\find ( \if ( phi )\then ( b )\else ( b ))
\replacewith ( b )
\heuristics (concrete )
\displayname "ifthenelse_same_branches"
};defined in: ifThenElseRules.key Line: 79 Offset :4ifthenelse_concrete {
\find ( \if ( phi )\then ( true )\else ( false ))
\replacewith ( phi )
\heuristics (concrete )
};defined in: ifThenElseRules.key Line: 86 Offset :4ifthenelse_concrete2 {
\find ( \if ( phi )\then ( false )\else ( true ))
\replacewith ( ! phi )
\heuristics (concrete )
\displayname "ifthenelse_concrete"
};defined in: ifThenElseRules.key Line: 92 Offset :4ifthenelse_concrete3 {
\find ( \if ( phi )\then ( then )\else ( else )= then )
\replacewith ( phi | else = then )
\heuristics (concrete )
\displayname "ifthenelse_concrete"
};defined in: ifThenElseRules.key Line: 99 Offset :4ifthenelse_concrete4 {
\find ( \if ( phi )\then ( then )\else ( else )= else )
\replacewith ( ! phi | then = else )
\heuristics (concrete )
\displayname "ifthenelse_concrete"
};defined in: ifThenElseRules.key Line: 106 Offset :4ifthenelse_split {
\find ( \if ( phi )\then ( then )\else ( else ))
\sameUpdateLevel
"#phi TRUE" : \replacewith ( then ) \add ( phi ==> );
"#phi FALSE" : \replacewith ( else ) \add ( ==> phi )
\heuristics (split_cond )
};defined in: ifThenElseRules.key Line: 113 Offset :4ifthenelse_split_for {
\find ( \if ( phi )\then ( b )\else ( c ))
\sameUpdateLevel
"#phi TRUE" : \replacewith ( b ) \add ( phi ==> );
"#phi FALSE" : \replacewith ( c ) \add ( ==> phi )
\heuristics (split_cond )
\displayname "ifthenelse_split"
};defined in: ifThenElseRules.key Line: 123 Offset :4ifExthenelse1_false {
\find ( \ifEx intVar ; ( false )\then ( then )\else ( else ))
\replacewith ( else )
\heuristics (concrete )
};defined in: ifThenElseRules.key Line: 138 Offset :4ifExthenelse1_false_for {
\find ( \ifEx intVar ; ( false )\then ( b )\else ( c ))
\replacewith ( c )
\heuristics (concrete )
\displayname "ifExthenelse1_false"
};defined in: ifThenElseRules.key Line: 144 Offset :4ifExthenelse1_eq_for {
\find ( \ifEx intVar ; ( intVar = t )\then ( b )\else ( c ))
\varcond \replacewith ( {\subst intVar ; t } b )
\heuristics (concrete )
\displayname "ifExthenelse1_eq"
};defined in: ifThenElseRules.key Line: 158 Offset :4ifExthenelse1_eq2 {
\find ( \ifEx intVar ; ( t = intVar )\then ( then )\else ( else ))
\varcond \replacewith ( {\subst intVar ; t } then )
\heuristics (concrete )
\displayname "ifExthenelse1_eq"
};defined in: ifThenElseRules.key Line: 166 Offset :4ifExthenelse1_eq2_for {
\find ( \ifEx intVar ; ( t = intVar )\then ( b )\else ( c ))
\varcond \replacewith ( {\subst intVar ; t } b )
\heuristics (concrete )
\displayname "ifExthenelse1_eq"
};defined in: ifThenElseRules.key Line: 174 Offset :4ifExthenelse1_eq_for_phi {
\find ( \ifEx intVar ; ( phi & intVar = t )\then ( b )\else ( c ))
\varcond \replacewith ( \if ( {\subst intVar ; t } phi )\then ( {\subst intVar ; t } b )\else ( c ))
\heuristics (concrete )
\displayname "ifExthenelse1_eq"
};defined in: ifThenElseRules.key Line: 191 Offset :4ifExthenelse1_eq2_phi {
\find ( \ifEx intVar ; ( phi & t = intVar )\then ( then )\else ( else ))
\varcond \replacewith ( \if ( {\subst intVar ; t } phi )\then ( {\subst intVar ; t } then )\else ( else ))
\heuristics (concrete )
\displayname "ifExthenelse1_eq"
};defined in: ifThenElseRules.key Line: 201 Offset :4ifExthenelse1_eq2_for_phi {
\find ( \ifEx intVar ; ( phi & t = intVar )\then ( b )\else ( c ))
\varcond \replacewith ( \if ( {\subst intVar ; t } phi )\then ( {\subst intVar ; t } b )\else ( c ))
\heuristics (concrete )
\displayname "ifExthenelse1_eq"
};defined in: ifThenElseRules.key Line: 211 Offset :4ifExthenelse1_unused_var_for {
\find ( \ifEx intVar ; ( phi )\then ( b )\else ( c ))
\varcond \replacewith ( \if ( \exists intVar ; phi )\then ( b )\else ( c ))
\heuristics (simplify )
\displayname "ifExthenelse1_unused_var"
};defined in: ifThenElseRules.key Line: 228 Offset :4ifExthenelse1_split {
\find ( \ifEx intVar ; ( phi )\then ( then )\else ( else ))
\sameUpdateLevel
\varcond \replacewith ( {\subst intVar ; intSk } then ) \add ( {\subst intVar ; intSk } phi , \forall intVar ; ( phi -> wellOrderLeqInt ( intSk , intVar ))==> );
\replacewith ( else ) \add ( ==> \exists intVar ; phi )
\heuristics (split_cond )
};defined in: ifThenElseRules.key Line: 236 Offset :4ifExthenelse1_solve {
\find ( \ifEx intVar ; ( phi )\then ( then )\else ( else ))
\sameUpdateLevel
\varcond \replacewith ( {\subst intVar ; intValue } then );
\replacewith ( \ifEx intVar ; ( phi )\then ( then )\else ( else )) \add ( ==> {\subst intVar ; intValue } phi & \forall intVar ; ( phi -> wellOrderLeqInt ( intValue , intVar )))
};defined in: ifThenElseRules.key Line: 248 Offset :4ifExthenelse1_min {
\find ( \ifEx intVar ; ( phi )\then ( then )\else ( else ))
\sameUpdateLevel
\varcond \replacewith ( \if ( phi )\then ( {\subst intVar ; 0 } then )\else ( else ))
\heuristics (concrete )
};defined in: ifThenElseRules.key Line: 258 Offset :4ifExthenelse1_split_for {
\find ( \ifEx intVar ; ( phi )\then ( b )\else ( c ))
\sameUpdateLevel
\varcond \replacewith ( {\subst intVar ; intSk } b ) \add ( {\subst intVar ; intSk } phi , \forall intVar ; ( phi -> wellOrderLeqInt ( intSk , intVar ))==> );
\replacewith ( c ) \add ( ==> \exists intVar ; phi )
\heuristics (split_cond )
\displayname "ifExthenelse1_split"
};defined in: ifThenElseRules.key Line: 266 Offset :4ifExthenelse1_solve_for {
\find ( \ifEx intVar ; ( phi )\then ( b )\else ( c ))
\sameUpdateLevel
\varcond \replacewith ( {\subst intVar ; intValue } b );
\replacewith ( \ifEx intVar ; ( phi )\then ( b )\else ( c )) \add ( ==> {\subst intVar ; intValue } phi & \forall intVar ; ( phi -> wellOrderLeqInt ( intValue , intVar )))
\displayname "ifExthenelse1_solve"
};defined in: ifThenElseRules.key Line: 279 Offset :4ifExthenelse1_min_for {
\find ( \ifEx intVar ; ( phi )\then ( b )\else ( c ))
\sameUpdateLevel
\varcond \replacewith ( \if ( phi )\then ( {\subst intVar ; 0 } b )\else ( c ))
\heuristics (concrete )
\displayname "ifExthenelse1_min"
};defined in: ifThenElseRules.key Line: 290 Offset :4def_wellOrderLeqInt {
\find ( wellOrderLeqInt ( intT1 , intT2 ))
\replacewith ( ( geq ( intT1 , intT2 )& lt ( intT2 , 0 ))| ( leq ( 0 , intT1 )& leq ( intT1 , intT2 )))
\heuristics (simplify )
};defined in: ifThenElseRules.key Line: 301 Offset :4