\generic G, S1, S2, H;defined in: firstOrderRules.key Line: 8 Offset :4\generic G, S1, S2, H;defined in: firstOrderRules.key Line: 8 Offset :4\generic G, S1, S2, H;defined in: firstOrderRules.key Line: 8 Offset :4\generic G, S1, S2, H;defined in: firstOrderRules.key Line: 8 Offset :4allLeftHide {
\find ( \forall u ; b ==> )
\replacewith ( {\subst u ; t } ( b )==> ) \addrules ( insert_hidden {
\add ( \forall u ; b ==> )
};)
\heuristics (gamma_destructive )
};defined in: firstOrderRules.key Line: 41 Offset :4exRightHide {
\find ( ==> \exists u ; b )
\replacewith ( ==> {\subst u ; t } ( b )) \addrules ( insert_hidden {
\add ( ==> \exists u ; b )
};)
\heuristics (gamma_destructive )
};defined in: firstOrderRules.key Line: 50 Offset :4allRight {
\find ( ==> \forall u ; b )
\varcond \replacewith ( ==> {\subst u ; sk } b )
\heuristics (delta )
};defined in: firstOrderRules.key Line: 72 Offset :4exLeft {
\find ( \exists u ; b ==> )
\varcond \replacewith ( {\subst u ; sk } b ==> )
\heuristics (delta )
};defined in: firstOrderRules.key Line: 77 Offset :4all_unused {
\find ( \forall u ; b )
\varcond \replacewith ( b )
\heuristics (elimQuantifier )
};defined in: firstOrderRules.key Line: 84 Offset :4ex_unused {
\find ( \exists u ; b )
\varcond \replacewith ( b )
\heuristics (elimQuantifier )
};defined in: firstOrderRules.key Line: 90 Offset :4eqClose {
\find ( s = s )
\replacewith ( true )
\heuristics (concrete )
};defined in: firstOrderRules.key Line: 98 Offset :4eqSymm {
\find ( commEqLeft = commEqRight )
\replacewith ( commEqRight = commEqLeft )
\heuristics (order_terms )
};defined in: firstOrderRules.key Line: 103 Offset :4make_insert_eq {
\find ( sr = tr ==> )
\addrules ( insert_eq {
\find ( sr )
\replacewith ( tr )
};)
};defined in: firstOrderRules.key Line: 109 Offset :4make_insert_eq_nonrigid {
\find ( s = t ==> )
\addrules ( insert_eq_nonrigid {
\find ( s )
\sameUpdateLevel
\replacewith ( t )
\displayname "insert_eq"
};)
};defined in: firstOrderRules.key Line: 118 Offset :4insert_eq_all {
\find ( sr = tr ==> )
\replacewith ( ==> ) \addrules ( auto_insert_eq {
\find ( sr )
\replacewith ( tr )
\heuristics (simplify )
};)
};defined in: firstOrderRules.key Line: 128 Offset :4apply_subst {
\find ( {\subst u ; t } target )
\replacewith ( {\subst u ; t } target )
\heuristics (try_apply_subst )
};defined in: firstOrderRules.key Line: 140 Offset :4apply_subst_for {
\schemaVar \formula phi ;
\find ( {\subst u ; t } phi )
\replacewith ( {\subst u ; t } phi )
\heuristics (try_apply_subst )
\displayname "apply_subst"
};defined in: firstOrderRules.key Line: 148 Offset :4subst_to_eq {
\find ( {\subst u ; t } target )
\sameUpdateLevel
\varcond \replacewith ( {\subst u ; sk } target ) \add ( sk = t ==> )
\heuristics (simplify )
};defined in: firstOrderRules.key Line: 158 Offset :4subst_to_eq_for {
\schemaVar \formula phi ;
\find ( {\subst u ; t } phi )
\sameUpdateLevel
\varcond \replacewith ( {\subst u ; sk } phi ) \add ( sk = t ==> )
\heuristics (simplify )
\displayname "subst_to_eq"
};defined in: firstOrderRules.key Line: 167 Offset :4applyEq {
\assumes ( s = t1 ==> )
\find ( s )
\sameUpdateLevel
\replacewith ( t1 )
\heuristics (apply_equations , apply_select_eq )
\displayname "applyEq"
};defined in: firstOrderRules.key Line: 181 Offset :4applyEqReverse {
\assumes ( s = t1 ==> )
\find ( t1 )
\sameUpdateLevel
\replacewith ( s )
\heuristics (apply_auxiliary_eq )
\displayname "applyEqReverse"
};defined in: firstOrderRules.key Line: 190 Offset :4applyEqRigid {
\schemaVar \term [ rigid ]H tr1 ;
\assumes ( sr = tr1 ==> )
\find ( sr )
\replacewith ( tr1 )
\heuristics (apply_equations )
\displayname "applyEq"
};defined in: firstOrderRules.key Line: 199 Offset :4pullOut {
\find ( t )
\sameUpdateLevel
\varcond \replacewith ( sk ) \add ( t = sk ==> )
\heuristics (semantics_blasting )
};defined in: firstOrderRules.key Line: 209 Offset :4equalUnique {
\schemaVar \term any f , f2 ;
\schemaVar \formula result ;
\find ( f = f2 )
\varcond \replacewith ( result )
\heuristics (concrete )
};defined in: firstOrderRules.key Line: 239 Offset :4