less_iff_diff_less_0 {
\find ( lt ( i0 , i1 ))
\replacewith ( lt ( sub ( i0 , i1 ), 0 ))
};defined in: integerSimplificationRules.key Line: 75 Offset :4leq_iff_diff_leq_0 {
\find ( leq ( i0 , i1 ))
\replacewith ( leq ( sub ( i0 , i1 ), 0 ))
};defined in: integerSimplificationRules.key Line: 81 Offset :4minus_distribute_1 {
\find ( neg ( add ( i , i1 )))
\replacewith ( add ( neg ( i ), neg ( i1 )))
\heuristics (simplify_int )
\displayname "minus_distribute"
};defined in: integerSimplificationRules.key Line: 87 Offset :4minus_distribute_2 {
\find ( neg ( sub ( i , i1 )))
\replacewith ( add ( neg ( i ), i1 ))
\heuristics (simplify_int )
\displayname "minus_distribute"
};defined in: integerSimplificationRules.key Line: 94 Offset :4leq_diff1_eq {
\find ( leq ( i0 , sub ( i1 , 1 )))
\replacewith ( lt ( i0 , i1 ))
\heuristics (simplify_int )
};defined in: integerSimplificationRules.key Line: 144 Offset :4le1_add1_eq_le {
\find ( lt ( i0 , add ( i1 , 1 )))
\replacewith ( leq ( i0 , i1 ))
\heuristics (simplify_int )
};defined in: integerSimplificationRules.key Line: 151 Offset :4zadd_left_cancel0 {
\find ( i0 = add ( i0 , i1 ))
\replacewith ( i1 = 0 )
};defined in: integerSimplificationRules.key Line: 158 Offset :4int_diff_minus_eq {
\find ( sub ( i0 , neg ( i1 )))
\replacewith ( add ( i0 , i1 ))
};defined in: integerSimplificationRules.key Line: 164 Offset :4square_nonneg {
\find ( leq ( 0 , mul ( i0 , i0 )))
\replacewith ( true )
\heuristics (simplify_int )
};defined in: integerSimplificationRules.key Line: 212 Offset :4mul_distribute_4 {
\find ( mul ( i0 , add ( i1 , i2 )))
\replacewith ( add ( mul ( i0 , i1 ), mul ( i0 , i2 )))
\displayname "multiply_distribute"
};defined in: integerSimplificationRules.key Line: 266 Offset :4mul_distribute_5 {
\find ( mul ( add ( i1 , i2 ), i0 ))
\replacewith ( add ( mul ( i0 , i1 ), mul ( i0 , i2 )))
\displayname "multiply_distribute"
};defined in: integerSimplificationRules.key Line: 273 Offset :4collect_same_terms_1 {
\find ( add ( mul ( i , j ), mul ( i , j )))
\replacewith ( mul ( 2 , mul ( i , j )))
\displayname "collect_same_terms"
};defined in: integerSimplificationRules.key Line: 287 Offset :4collect_same_terms_2 {
\find ( add ( add ( mul ( i , j ), mul ( i0 , i1 )), add ( mul ( i , j ), mul ( j0 , j1 ))))
\replacewith ( add ( mul ( 2 , mul ( i , j )), add ( mul ( i0 , i1 ), mul ( j0 , j1 ))))
\displayname "collect_same_terms"
};defined in: integerSimplificationRules.key Line: 294 Offset :4collect_same_terms_3 {
\find ( add ( add ( neg ( mul ( i , j )), mul ( i0 , i1 )), add ( neg ( mul ( i , j )), mul ( j0 , j1 ))))
\replacewith ( add ( neg ( mul ( 2 , mul ( i , j ))), add ( mul ( i0 , i1 ), mul ( j0 , j1 ))))
\displayname "collect_same_terms"
};defined in: integerSimplificationRules.key Line: 301 Offset :4leq_diff_1 {
\find ( leq ( i0 , add ( i0 , 1 )))
\replacewith ( true )
\heuristics (int_arithmetic )
};defined in: integerSimplificationRules.key Line: 378 Offset :4lt_diff_1 {
\find ( lt ( i0 , add ( i0 , 1 )))
\replacewith ( true )
\heuristics (int_arithmetic )
};defined in: integerSimplificationRules.key Line: 385 Offset :4geq_diff_1 {
\find ( geq ( add ( i0 , 1 ), i0 ))
\replacewith ( true )
\heuristics (int_arithmetic )
};defined in: integerSimplificationRules.key Line: 392 Offset :4gt_diff_1 {
\find ( gt ( add ( i0 , 1 ), i0 ))
\replacewith ( true )
\heuristics (int_arithmetic )
};defined in: integerSimplificationRules.key Line: 399 Offset :4i_minus_i_is_zero {
\find ( sub ( i , i ))
\replacewith ( 0 )
\heuristics (simplify_int )
};defined in: integerSimplificationRules.key Line: 406 Offset :4eq_sides {
\find ( i = j )
\replacewith ( sub ( i , j )= 0 )
};defined in: integerSimplificationRules.key Line: 432 Offset :4times_one_1 {
\find ( mul ( i , 1 ))
\replacewith ( i )
\heuristics (simplify_int )
\displayname "times_one"
};defined in: integerSimplificationRules.key Line: 438 Offset :4times_one_2 {
\find ( mul ( 1 , i ))
\replacewith ( i )
\heuristics (simplify_int )
\displayname "times_one"
};defined in: integerSimplificationRules.key Line: 445 Offset :4times_minus_one_1 {
\find ( mul ( i , - 1 ))
\replacewith ( neg ( i ))
\heuristics (simplify_int )
\displayname "times_minus_one"
};defined in: integerSimplificationRules.key Line: 452 Offset :4times_minus_one_2 {
\find ( mul ( - 1 , i ))
\replacewith ( neg ( i ))
\heuristics (simplify_int )
\displayname "times_minus_one"
};defined in: integerSimplificationRules.key Line: 459 Offset :4times_zero_1 {
\find ( mul ( i , 0 ))
\replacewith ( 0 )
\heuristics (simplify_literals )
\displayname "times_zero"
};defined in: integerSimplificationRules.key Line: 466 Offset :4times_zero_2 {
\find ( mul ( 0 , i ))
\replacewith ( 0 )
\heuristics (simplify_literals )
\displayname "times_zero"
};defined in: integerSimplificationRules.key Line: 473 Offset :4leq_to_gt {
\find ( leq ( i , j ))
\replacewith ( ! gt ( i , j ))
};defined in: integerSimplificationRules.key Line: 480 Offset :4geq_to_lt {
\find ( geq ( i , j ))
\replacewith ( ! lt ( i , j ))
};defined in: integerSimplificationRules.key Line: 486 Offset :4leq_to_gt_alt {
\find ( leq ( i , j ))
\replacewith ( lt ( i , j )| i = j )
};defined in: integerSimplificationRules.key Line: 492 Offset :4geq_to_lt_alt {
\find ( geq ( i , j ))
\replacewith ( gt ( i , j )| i = j )
};defined in: integerSimplificationRules.key Line: 498 Offset :4greater {
\find ( gt ( i , i0 ))
\replacewith ( lt ( i0 , i ))
};defined in: integerSimplificationRules.key Line: 504 Offset :4less_is_alternative_1 {
\assumes ( lt ( i , i0 ), lt ( i0 , i )==> )
\closegoal
};defined in: integerSimplificationRules.key Line: 531 Offset :4less_neg {
\find ( lt ( i , i0 ))
\replacewith ( ! ( lt ( i0 , i + 1 )))
};defined in: integerSimplificationRules.key Line: 555 Offset :4less_base {
\find ( lt ( i , i ))
\replacewith ( false )
\heuristics (simplify_int )
};defined in: integerSimplificationRules.key Line: 561 Offset :4add_zero_left {
\find ( add ( 0 , i ))
\replacewith ( i )
\heuristics (simplify_literals )
};defined in: integerSimplificationRules.key Line: 567 Offset :4add_zero_right {
\find ( add ( i , 0 ))
\replacewith ( i )
\heuristics (simplify_literals )
};defined in: integerSimplificationRules.key Line: 572 Offset :4switch_params {
\find ( add ( i0 , i1 ))
\replacewith ( add ( i1 , i0 ))
};defined in: integerSimplificationRules.key Line: 583 Offset :4mul_comm {
\find ( mul ( i0 , i1 ))
\replacewith ( mul ( i1 , i0 ))
};defined in: integerSimplificationRules.key Line: 594 Offset :4pull_out_neg_1 {
\find ( mul ( neg ( i0 ), i1 ))
\replacewith ( neg ( mul ( i0 , i1 )))
\displayname "pull_out_minus"
};defined in: integerSimplificationRules.key Line: 600 Offset :4pull_out_neg_2 {
\find ( mul ( i0 , neg ( i1 )))
\replacewith ( neg ( mul ( i0 , i1 )))
\displayname "pull_out_minus"
};defined in: integerSimplificationRules.key Line: 606 Offset :4add_eq_back {
\find ( add ( i1 , i )= add ( i1 , i0 ))
\replacewith ( i = i0 )
\heuristics (simplify_int )
};defined in: integerSimplificationRules.key Line: 648 Offset :4add_eq_back_2 {
\find ( add ( i , i1 )= add ( i0 , i1 ))
\replacewith ( i = i0 )
\heuristics (simplify_int )
\displayname "add_eq_back"
};defined in: integerSimplificationRules.key Line: 655 Offset :4add_eq_back_2_fst_comm {
\find ( add ( i1 , i )= add ( i0 , i1 ))
\replacewith ( i = i0 )
\heuristics (simplify_int )
\displayname "add_eq_back"
};defined in: integerSimplificationRules.key Line: 663 Offset :4add_eq_back_3 {
\find ( i1 = add ( i1 , i0 ))
\replacewith ( 0 = i0 )
\heuristics (simplify_int )
\displayname "add_eq_back"
};defined in: integerSimplificationRules.key Line: 671 Offset :4add_less_back {
\find ( lt ( add ( i1 , i ), add ( i1 , i0 )))
\replacewith ( lt ( i , i0 ))
\heuristics (simplify_int )
};defined in: integerSimplificationRules.key Line: 703 Offset :4add_less_back_zero_1 {
\find ( lt ( i , add ( i , i1 )))
\replacewith ( lt ( 0 , i1 ))
\heuristics (simplify_int )
\displayname "add_less_back"
};defined in: integerSimplificationRules.key Line: 710 Offset :4add_less_back_zero_1_comm {
\find ( lt ( i , add ( i1 , i )))
\replacewith ( lt ( 0 , i1 ))
\heuristics (simplify_int )
\displayname "add_less_back"
};defined in: integerSimplificationRules.key Line: 718 Offset :4add_less_back_zero_2 {
\find ( lt ( add ( i , i1 ), i ))
\replacewith ( lt ( i1 , 0 ))
\heuristics (simplify_int )
\displayname "add_less_back"
};defined in: integerSimplificationRules.key Line: 726 Offset :4add_less_back_zero_2_comm {
\find ( lt ( add ( i1 , i ), i ))
\replacewith ( lt ( i1 , 0 ))
\heuristics (simplify_int )
\displayname "add_less_back"
};defined in: integerSimplificationRules.key Line: 734 Offset :4sub {
\find ( sub ( i , i0 ))
\replacewith ( add ( i , neg ( i0 )))
\heuristics (simplify_int )
};defined in: integerSimplificationRules.key Line: 742 Offset :4sub_zero_1 {
\find ( Z ( neglit ( 0 ( #))))
\replacewith ( Z ( 0 ( #)))
\heuristics (simplify_literals )
};defined in: integerSimplificationRules.key Line: 747 Offset :4sub_zero_2 {
\find ( sub ( i , 0 ))
\replacewith ( i )
\heuristics (simplify_int )
};defined in: integerSimplificationRules.key Line: 753 Offset :4add_sub_elim_left {
\find ( add ( neg ( i ), i ))
\replacewith ( 0 )
\heuristics (simplify_int )
};defined in: integerSimplificationRules.key Line: 758 Offset :4add_sub_elim_right {
\find ( add ( i , neg ( i )))
\replacewith ( 0 )
\heuristics (simplify_int )
};defined in: integerSimplificationRules.key Line: 763 Offset :4add_sub_step {
\find ( add ( neg ( i ), neg ( i0 )))
\replacewith ( neg ( add ( i , i0 )))
};defined in: integerSimplificationRules.key Line: 768 Offset :4sub_sub_elim {
\find ( neg ( neg ( i )))
\replacewith ( i )
\heuristics (simplify_int )
};defined in: integerSimplificationRules.key Line: 773 Offset :4less_sub {
\find ( lt ( i , i0 ))
\replacewith ( lt ( neg ( i0 ), neg ( i )))
};defined in: integerSimplificationRules.key Line: 778 Offset :4less_plus {
\find ( lt ( 0 , add ( i0 , i1 )))
\replacewith ( lt ( neg ( i0 ), i1 ))
};defined in: integerSimplificationRules.key Line: 784 Offset :4lt_to_leq_1 {
\find ( lt ( i , j )| i = j )
\replacewith ( leq ( i , j ))
\heuristics (simplify_int )
};defined in: integerSimplificationRules.key Line: 797 Offset :4lt_to_leq_2 {
\assumes ( ==> lt ( i , j ))
\find ( ==> i = j )
\replacewith ( ==> leq ( i , j ))
\heuristics (simplify_int )
};defined in: integerSimplificationRules.key Line: 803 Offset :4lt_to_gt {
\find ( lt ( i , i0 ))
\replacewith ( gt ( i0 , i ))
};defined in: integerSimplificationRules.key Line: 811 Offset :4gt_to_lt {
\find ( gt ( i , i0 ))
\replacewith ( lt ( i0 , i ))
};defined in: integerSimplificationRules.key Line: 816 Offset :4leq_to_geq {
\find ( leq ( i , i0 ))
\replacewith ( geq ( i0 , i ))
};defined in: integerSimplificationRules.key Line: 821 Offset :4geq_to_leq {
\find ( geq ( i , i0 ))
\replacewith ( leq ( i0 , i ))
};defined in: integerSimplificationRules.key Line: 826 Offset :4double_unary_minus_literal {
\find ( Z ( neglit ( neglit ( iz ))))
\replacewith ( Z ( iz ))
\heuristics (simplify_literals )
\displayname "double_unary_minus"
};defined in: integerSimplificationRules.key Line: 836 Offset :4charLiteral_to_int {
\find ( C ( iz ))
\replacewith ( Z ( iz ))
\heuristics (charLiteral_to_intLiteral )
};defined in: integerSimplificationRules.key Line: 844 Offset :4add_literals {
\find ( add ( Z ( iz ), Z ( jz )))
\replacewith ( #add ( Z ( iz ), Z ( jz )))
\heuristics (simplify_literals )
};defined in: integerSimplificationRules.key Line: 850 Offset :4sub_literals {
\find ( sub ( Z ( iz ), Z ( jz )))
\replacewith ( #sub ( Z ( iz ), Z ( jz )))
\heuristics (simplify_literals )
};defined in: integerSimplificationRules.key Line: 857 Offset :4mul_literals {
\find ( mul ( Z ( iz ), Z ( jz )))
\replacewith ( #mul ( Z ( iz ), Z ( jz )))
\heuristics (simplify_literals )
};defined in: integerSimplificationRules.key Line: 864 Offset :4div_literals {
\find ( div ( Z ( iz ), Z ( jz )))
\replacewith ( #div ( Z ( iz ), Z ( jz )))
\heuristics (simplify_literals )
};defined in: integerSimplificationRules.key Line: 871 Offset :4less_literals {
\find ( lt ( Z ( iz ), Z ( jz )))
\replacewith ( #less ( Z ( iz ), Z ( jz )))
\heuristics (simplify_literals )
};defined in: integerSimplificationRules.key Line: 878 Offset :4greater_literals {
\find ( gt ( Z ( iz ), Z ( jz )))
\replacewith ( #greater ( Z ( iz ), Z ( jz )))
\heuristics (simplify_literals )
};defined in: integerSimplificationRules.key Line: 885 Offset :4leq_literals {
\find ( leq ( Z ( iz ), Z ( jz )))
\replacewith ( #leq ( Z ( iz ), Z ( jz )))
\heuristics (simplify_literals )
};defined in: integerSimplificationRules.key Line: 892 Offset :4qeq_literals {
\find ( geq ( Z ( iz ), Z ( jz )))
\replacewith ( #geq ( Z ( iz ), Z ( jz )))
\heuristics (simplify_literals )
};defined in: integerSimplificationRules.key Line: 899 Offset :4equal_literals {
\find ( Z ( iz )= Z ( jz ))
\replacewith ( #eq ( Z ( iz ), Z ( jz )))
\heuristics (simplify_literals )
};defined in: integerSimplificationRules.key Line: 906 Offset :4neg_literal {
\find ( neg ( Z ( iz )))
\replacewith ( Z ( neglit ( iz )))
\heuristics (simplify_literals )
};defined in: integerSimplificationRules.key Line: 913 Offset :4pow_literals {
\find ( pow ( Z ( iz ), Z ( jz )))
\replacewith ( #pow ( Z ( iz ), Z ( jz )))
\heuristics (simplify_literals , nonDuplicateAppCheckEq )
};defined in: integerSimplificationRules.key Line: 919 Offset :4multiply_2_inEq0 {
\assumes ( multFacLeft <= multFacRight ==> )
\find ( multLeft <= multRight ==> )
\add ( multLeft * multFacLeft >= - multRight * multFacRight + multRight * multFacLeft + multLeft * multFacRight ==> )
\heuristics (inEqSimp_nonLin , inEqSimp_nonLin_multiply )
};defined in: integerSimplificationRules.key Line: 951 Offset :4multiply_2_inEq1 {
\assumes ( multFacLeft >= multFacRight ==> )
\find ( multLeft <= multRight ==> )
\add ( multLeft * multFacLeft <= - multRight * multFacRight + multRight * multFacLeft + multLeft * multFacRight ==> )
\heuristics (inEqSimp_nonLin , inEqSimp_nonLin_multiply )
};defined in: integerSimplificationRules.key Line: 962 Offset :4multiply_2_inEq2 {
\assumes ( multFacLeft <= multFacRight ==> )
\find ( multLeft >= multRight ==> )
\add ( multLeft * multFacLeft <= - multRight * multFacRight + multRight * multFacLeft + multLeft * multFacRight ==> )
\heuristics (inEqSimp_nonLin , inEqSimp_nonLin_multiply )
};defined in: integerSimplificationRules.key Line: 973 Offset :4multiply_2_inEq3 {
\assumes ( multFacLeft >= multFacRight ==> )
\find ( multLeft >= multRight ==> )
\add ( multLeft * multFacLeft >= - multRight * multFacRight + multRight * multFacLeft + multLeft * multFacRight ==> )
\heuristics (inEqSimp_nonLin , inEqSimp_nonLin_multiply )
};defined in: integerSimplificationRules.key Line: 984 Offset :4divide_inEq0 {
\assumes ( divX >= divXBoundPos ==> )
\find ( divProd <= divProdBoundNonNeg ==> )
\add ( divProd = divX * divY -> divXBoundPos >= 1 -> divProdBoundNonNeg >= 0 -> divY <= divProdBoundNonNeg / divXBoundPos ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_divide )
};defined in: integerSimplificationRules.key Line: 995 Offset :4divide_inEq1 {
\assumes ( divX >= divXBoundNonNeg ==> )
\find ( divProd <= divProdBoundNeg ==> )
\add ( divProd = divX * divY -> divXBoundNonNeg >= 0 -> divProdBoundNeg <= - 1 -> divY <= - 1 ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_neg )
};defined in: integerSimplificationRules.key Line: 1006 Offset :4divide_inEq2 {
\assumes ( divX >= divXBoundPos ==> )
\find ( divProd >= divProdBoundNonPos ==> )
\add ( divProd = divX * divY -> divXBoundPos >= 1 -> divProdBoundNonPos <= 0 -> divY >= ( divProdBoundNonPos + divXBoundPos - 1 )/ divXBoundPos ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_divide )
};defined in: integerSimplificationRules.key Line: 1017 Offset :4divide_inEq3 {
\assumes ( divX >= divXBoundNonNeg ==> )
\find ( divProd >= divProdBoundPos ==> )
\add ( divProd = divX * divY -> divXBoundNonNeg >= 0 -> divProdBoundPos >= 1 -> divY >= 1 ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_pos )
};defined in: integerSimplificationRules.key Line: 1029 Offset :4divide_inEq4 {
\assumes ( divX <= divXBoundNeg ==> )
\find ( divProd >= divProdBoundNonPos ==> )
\add ( divProd = divX * divY -> divXBoundNeg <= - 1 -> divProdBoundNonPos <= 0 -> divY <= divProdBoundNonPos / divXBoundNeg ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_divide )
};defined in: integerSimplificationRules.key Line: 1040 Offset :4divide_inEq5 {
\assumes ( divX <= divXBoundNonPos ==> )
\find ( divProd >= divProdBoundPos ==> )
\add ( divProd = divX * divY -> divXBoundNonPos <= 0 -> divProdBoundPos >= 1 -> divY <= - 1 ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_neg )
};defined in: integerSimplificationRules.key Line: 1051 Offset :4divide_inEq6 {
\assumes ( divX <= divXBoundNeg ==> )
\find ( divProd <= divProdBoundNonNeg ==> )
\add ( divProd = divX * divY -> divXBoundNeg <= - 1 -> divProdBoundNonNeg >= 0 -> divY >= divProdBoundNonNeg / divXBoundNeg ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_divide )
};defined in: integerSimplificationRules.key Line: 1062 Offset :4divide_inEq7 {
\assumes ( divX <= divXBoundNonPos ==> )
\find ( divProd <= divProdBoundNeg ==> )
\add ( divProd = divX * divY -> divXBoundNonPos <= 0 -> divProdBoundNeg <= - 1 -> divY >= 1 ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_pos )
};defined in: integerSimplificationRules.key Line: 1073 Offset :4divide_eq0 {
\assumes ( divX >= divXBoundPos ==> )
\find ( divProd = divProdBoundNonNeg ==> )
\add ( divProd = divX * divY -> divXBoundPos >= 1 -> divProdBoundNonNeg >= 0 -> divY <= divProdBoundNonNeg / divXBoundPos ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_divide )
};defined in: integerSimplificationRules.key Line: 1084 Offset :4divide_eq1 {
\assumes ( divX >= divXBoundNonNeg ==> )
\find ( divProd = divProdBoundNeg ==> )
\add ( divProd = divX * divY -> divXBoundNonNeg >= 0 -> divProdBoundNeg <= - 1 -> divY <= - 1 ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_neg )
};defined in: integerSimplificationRules.key Line: 1095 Offset :4divide_eq2 {
\assumes ( divX >= divXBoundPos ==> )
\find ( divProd = divProdBoundNonPos ==> )
\add ( divProd = divX * divY -> divXBoundPos >= 1 -> divProdBoundNonPos <= 0 -> divY >= ( divProdBoundNonPos + divXBoundPos - 1 )/ divXBoundPos ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_divide )
};defined in: integerSimplificationRules.key Line: 1106 Offset :4divide_eq3 {
\assumes ( divX >= divXBoundNonNeg ==> )
\find ( divProd = divProdBoundPos ==> )
\add ( divProd = divX * divY -> divXBoundNonNeg >= 0 -> divProdBoundPos >= 1 -> divY >= 1 ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_pos )
};defined in: integerSimplificationRules.key Line: 1118 Offset :4divide_eq4 {
\assumes ( divX <= divXBoundNeg ==> )
\find ( divProd = divProdBoundNonPos ==> )
\add ( divProd = divX * divY -> divXBoundNeg <= - 1 -> divProdBoundNonPos <= 0 -> divY <= divProdBoundNonPos / divXBoundNeg ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_divide )
};defined in: integerSimplificationRules.key Line: 1129 Offset :4divide_eq5 {
\assumes ( divX <= divXBoundNonPos ==> )
\find ( divProd = divProdBoundPos ==> )
\add ( divProd = divX * divY -> divXBoundNonPos <= 0 -> divProdBoundPos >= 1 -> divY <= - 1 ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_neg )
};defined in: integerSimplificationRules.key Line: 1140 Offset :4divide_eq6 {
\assumes ( divX <= divXBoundNeg ==> )
\find ( divProd = divProdBoundNonNeg ==> )
\add ( divProd = divX * divY -> divXBoundNeg <= - 1 -> divProdBoundNonNeg >= 0 -> divY >= divProdBoundNonNeg / divXBoundNeg ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_divide )
};defined in: integerSimplificationRules.key Line: 1151 Offset :4divide_eq7 {
\assumes ( divX <= divXBoundNonPos ==> )
\find ( divProd = divProdBoundNeg ==> )
\add ( divProd = divX * divY -> divXBoundNonPos <= 0 -> divProdBoundNeg <= - 1 -> divY >= 1 ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonLin_pos )
};defined in: integerSimplificationRules.key Line: 1162 Offset :4auto_int_induction_geqZero {
\find ( ==> \forall uSub ; b )
\varcond "Base Case" : \replacewith ( ==> {\subst uSub ; 0 } b );
"Step Case (positive)" : \replacewith ( ==> ( ( geq ( sk , 0 )& {\subst uSub ; sk } b )-> {\subst uSub ; sk + 1 } b ));
"Step Case (negative)" : \replacewith ( ==> ( ( leq ( sk , 0 )& {\subst uSub ; sk } b )-> {\subst uSub ; sk - 1 } b ))
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1198 Offset :4auto_int_induction_geq_1 {
\find ( ==> \forall uSub ; ( t <= uSub -> b ))
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t } b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 0 )& {\subst uSub ; t + sk } b )-> #ExpandQueries ( {\subst uSub ; t + ( sk + 1 )} b , true )))
\heuristics (auto_induction , induction_var )
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1214 Offset :4auto_int_induction_geq_2 {
\find ( ==> \forall uSub ; ( t > uSub | b ))
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t } b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 0 )& {\subst uSub ; t + sk } b )-> #ExpandQueries ( {\subst uSub ; t + ( sk + 1 )} b , true )))
\heuristics (auto_induction , induction_var )
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1226 Offset :4auto_int_induction_geq_3 {
\find ( ==> \forall uSub ; ( uSub < t | b ))
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t } b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 0 )& {\subst uSub ; t + sk } b )-> #ExpandQueries ( {\subst uSub ; t + ( sk + 1 )} b , true )))
\heuristics (auto_induction , induction_var )
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1238 Offset :4auto_int_induction_geq_5 {
\find ( ==> \forall uSub ; ( ( t > uSub | psi )| b ))
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t } ( psi | b ), true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 0 )& {\subst uSub ; t + sk } ( psi | b ))-> #ExpandQueries ( {\subst uSub ; t + ( sk + 1 )} ( psi | b ), true )))
\heuristics (auto_induction , induction_var )
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1252 Offset :4auto_int_induction_geq_6 {
\find ( ==> \forall uSub ; ( ( uSub < t | psi )| b ))
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t } ( psi | b ), true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 0 )& {\subst uSub ; t + sk } ( psi | b ))-> #ExpandQueries ( {\subst uSub ; t + ( sk + 1 )} ( psi | b ), true )))
\heuristics (auto_induction , induction_var )
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1264 Offset :4auto_int_induction_gt_1 {
\find ( ==> \forall uSub ; ( t < uSub -> b ))
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t + 1 } b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 1 )& {\subst uSub ; t + sk } b )-> #ExpandQueries ( {\subst uSub ; t + ( sk + 1 )} b , true )))
\heuristics (auto_induction , induction_var )
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1278 Offset :4auto_int_induction_gt_2 {
\find ( ==> \forall uSub ; ( t >= uSub | b ))
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t + 1 } b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 1 )& {\subst uSub ; t + sk } b )-> #ExpandQueries ( {\subst uSub ; t + ( sk + 1 )} b , true )))
\heuristics (auto_induction , induction_var )
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1290 Offset :4auto_int_induction_gt_3 {
\find ( ==> \forall uSub ; ( uSub <= t | b ))
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t + 1 } b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 1 )& {\subst uSub ; t + sk } b )-> #ExpandQueries ( {\subst uSub ; t + ( sk + 1 )} b , true )))
\heuristics (auto_induction , induction_var )
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1302 Offset :4auto_int_induction_gt_5 {
\find ( ==> \forall uSub ; ( ( t >= uSub | psi )| b ))
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t + 1 } ( psi | b ), true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 1 )& {\subst uSub ; t + sk } ( psi | b ))-> #ExpandQueries ( {\subst uSub ; t + ( sk + 1 )} ( psi | b ), true )))
\heuristics (auto_induction , induction_var )
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1316 Offset :4auto_int_induction_gt_6 {
\find ( ==> \forall uSub ; ( ( uSub <= t | psi )| b ))
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t + 1 } ( psi | b ), true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 1 )& {\subst uSub ; t + sk } ( psi | b ))-> #ExpandQueries ( {\subst uSub ; t + ( sk + 1 )} ( psi | b ), true )))
\heuristics (auto_induction , induction_var )
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1328 Offset :4autoInduct_Lemma {
\find ( ==> ( \forall uSub ; b )& phi )
\varcond "Base Case" : \replacewith ( ==> {\subst uSub ; 0 } b );
"Step Case (positive)" : \replacewith ( ==> ( ( geq ( sk , 0 )& {\subst uSub ; sk } b )-> {\subst uSub ; sk + 1 } b ));
"Step Case (negative)" : \replacewith ( ==> ( ( leq ( sk , 0 )& {\subst uSub ; sk } b )-> {\subst uSub ; sk - 1 } b ));
"Use Case" : \replacewith ( \forall uSub ; b ==> phi )
};defined in: integerSimplificationRules.key Line: 1346 Offset :4autoInductGEQ_Lemma_1 {
\find ( ==> ( \forall uSub ; ( t <= uSub -> b ))& phi )
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t } b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 0 )& {\subst uSub ; t + sk } b )-> #ExpandQueries ( {\subst uSub ; t + ( sk + 1 )} b , true )));
"Use Case" : \replacewith ( \forall uSub ; ( t <= uSub -> b )==> phi )
\heuristics (auto_induction_lemma , induction_var )
\displayname "auto_induction_lemma"
};defined in: integerSimplificationRules.key Line: 1363 Offset :4autoInductGEQ_Lemma_2 {
\find ( ==> ( \forall uSub ; ( t > uSub | b ))& phi )
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t } b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 0 )& {\subst uSub ; t + sk } b )-> #ExpandQueries ( {\subst uSub ; ( t + ( sk + 1 ))} b , true )));
"Use Case" : \replacewith ( \forall uSub ; ( t <= uSub -> b )==> phi )
\heuristics (auto_induction_lemma , induction_var )
\displayname "auto_induction_lemma"
};defined in: integerSimplificationRules.key Line: 1377 Offset :4autoInductGEQ_Lemma_3 {
\find ( ==> ( \forall uSub ; ( uSub < t | b ))& phi )
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t } b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 0 )& {\subst uSub ; t + sk } b )-> #ExpandQueries ( {\subst uSub ; ( t + ( sk + 1 ))} b , true )));
"Use Case" : \replacewith ( \forall uSub ; ( t <= uSub -> b )==> phi )
\heuristics (auto_induction_lemma , induction_var )
\displayname "auto_induction_lemma"
};defined in: integerSimplificationRules.key Line: 1391 Offset :4autoInductGEQ_Lemma_5 {
\find ( ==> ( \forall uSub ; ( ( t > uSub | psi )| b ))& phi )
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t } ( psi | b ), true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 0 )& {\subst uSub ; t + sk } ( psi | b ))-> #ExpandQueries ( {\subst uSub ; ( t + ( sk + 1 ))} ( psi | b ), true )));
"Use Case" : \replacewith ( \forall uSub ; ( t <= uSub -> ( psi | b ))==> phi )
\heuristics (auto_induction_lemma , induction_var )
\displayname "auto_induction_lemma"
};defined in: integerSimplificationRules.key Line: 1407 Offset :4autoInductGEQ_Lemma_6 {
\find ( ==> ( \forall uSub ; ( ( uSub < t | psi )| b ))& phi )
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t } ( psi | b ), true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 0 )& {\subst uSub ; t + sk } ( psi | b ))-> #ExpandQueries ( {\subst uSub ; ( t + ( sk + 1 ))} ( psi | b ), true )));
"Use Case" : \replacewith ( \forall uSub ; ( t <= uSub -> ( psi | b ))==> phi )
\heuristics (auto_induction_lemma , induction_var )
\displayname "auto_induction_lemma"
};defined in: integerSimplificationRules.key Line: 1421 Offset :4autoInductGT_Lemma_1 {
\find ( ==> ( \forall uSub ; ( t < uSub -> b ))& phi )
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t + 1 } b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 1 )& {\subst uSub ; t + sk } b )-> #ExpandQueries ( {\subst uSub ; ( t + ( sk + 1 ))} b , true )));
"Use Case" : \replacewith ( \forall uSub ; ( t < uSub -> b )==> phi )
\heuristics (auto_induction_lemma , induction_var )
\displayname "auto_induction_lemma"
};defined in: integerSimplificationRules.key Line: 1438 Offset :4autoInductGT_Lemma_2 {
\find ( ==> ( \forall uSub ; ( t >= uSub | b ))& phi )
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t + 1 } b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 1 )& {\subst uSub ; t + sk } b )-> #ExpandQueries ( {\subst uSub ; ( t + ( sk + 1 ))} b , true )));
"Use Case" : \replacewith ( \forall uSub ; ( t < uSub -> b )==> phi )
\heuristics (auto_induction_lemma , induction_var )
\displayname "auto_induction_lemma"
};defined in: integerSimplificationRules.key Line: 1452 Offset :4autoInductGT_Lemma_3 {
\find ( ==> ( \forall uSub ; ( uSub <= t | b ))& phi )
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t + 1 } b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 1 )& {\subst uSub ; t + sk } b )-> #ExpandQueries ( {\subst uSub ; ( t + ( sk + 1 ))} b , true )));
"Use Case" : \replacewith ( \forall uSub ; ( t < uSub -> b )==> phi )
\heuristics (auto_induction_lemma , induction_var )
\displayname "auto_induction_lemma"
};defined in: integerSimplificationRules.key Line: 1466 Offset :4autoInductGT_Lemma_5 {
\find ( ==> ( \forall uSub ; ( ( t >= uSub | psi )| b ))& phi )
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t + 1 } ( psi | b ), true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 1 )& {\subst uSub ; t + sk } ( psi | b ))-> #ExpandQueries ( {\subst uSub ; ( t + ( sk + 1 ))} ( psi | b ), true )));
"Use Case" : \replacewith ( \forall uSub ; ( t < uSub -> ( psi | b ))==> phi )
\heuristics (auto_induction_lemma )
\displayname "auto_induction_lemma"
};defined in: integerSimplificationRules.key Line: 1482 Offset :4autoInductGT_Lemma_6 {
\find ( ==> ( \forall uSub ; ( ( uSub <= t | psi )| b ))& phi )
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t + 1 } ( psi | b ), true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 1 )& {\subst uSub ; t + sk } ( psi | b ))-> #ExpandQueries ( {\subst uSub ; ( t + ( sk + 1 ))} ( psi | b ), true )));
"Use Case" : \replacewith ( \forall uSub ; ( t < uSub -> ( psi | b ))==> phi )
\heuristics (auto_induction_lemma , induction_var )
\displayname "auto_induction_lemma"
};defined in: integerSimplificationRules.key Line: 1496 Offset :4auto_int_induction_geqZeroLeft {
\find ( \exists uSub ; b ==> )
\varcond "Base Case" : \replacewith ( ==> {\subst uSub ; 0 } ! b );
"Step Case (positive)" : \replacewith ( ==> ( ( geq ( sk , 0 )& {\subst uSub ; sk } ! b )-> {\subst uSub ; ( sk + 1 )} ! b ));
"Step Case (negative)" : \replacewith ( ==> ( ( leq ( sk , 0 )& {\subst uSub ; sk } ! b )-> {\subst uSub ; ( sk - 1 )} ! b ))
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1516 Offset :4auto_int_induction_geq_Left1 {
\find ( \exists uSub ; ( t <= uSub & b )==> )
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t } ! b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 0 )& {\subst uSub ; t + sk } ! b )-> #ExpandQueries ( {\subst uSub ; ( t + ( sk + 1 ))} ! b , true )))
\heuristics (auto_induction , induction_var )
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1531 Offset :4auto_int_induction_geq_Left2 {
\find ( \exists uSub ; ( uSub >= t & b )==> )
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t } ! b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 0 )& {\subst uSub ; t + sk } ! b )-> #ExpandQueries ( {\subst uSub ; ( t + ( sk + 1 ))} ! b , true )))
\heuristics (auto_induction , induction_var )
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1543 Offset :4auto_int_induction_gt_Left1 {
\find ( \exists uSub ; ( t < uSub & b )==> )
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t + 1 } ! b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 1 )& {\subst uSub ; t + sk } ! b )-> #ExpandQueries ( {\subst uSub ; ( t + ( sk + 1 ))} ! b , true )))
\heuristics (auto_induction , induction_var )
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1556 Offset :4auto_int_induction_gt_Left2 {
\find ( \exists uSub ; ( uSub > t & b )==> )
\varcond "Base Case" : \replacewith ( ==> #ExpandQueries ( {\subst uSub ; t + 1 } ! b , true ));
"Step Case" : \replacewith ( ==> ( ( geq ( sk , 1 )& {\subst uSub ; t + sk } ! b )-> #ExpandQueries ( {\subst uSub ; ( t + ( sk + 1 ))} ! b , true )))
\heuristics (auto_induction , induction_var )
\displayname "auto_induction"
};defined in: integerSimplificationRules.key Line: 1568 Offset :4splitEquation {
\find ( splitEqLeft = splitEqRight )
\replacewith ( splitEqLeft >= splitEqRight & splitEqLeft <= splitEqRight )
};defined in: integerSimplificationRules.key Line: 1593 Offset :4splitEquationSucc {
\find ( ==> splitEqLeft = splitEqRight )
\replacewith ( ==> splitEqLeft >= splitEqRight );
\replacewith ( ==> splitEqLeft <= splitEqRight )
\heuristics (inEqSimp_nonLin , inEqSimp_split_eq , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1598 Offset :4polySimp_elimSub {
\find ( sub ( i , i0 ))
\replacewith ( add ( i , mul ( i0 , - 1 )))
\heuristics (polySimp_expand , polySimp_elimSubNeg )
};defined in: integerSimplificationRules.key Line: 1612 Offset :4polySimp_elimNeg {
\find ( neg ( i ))
\replacewith ( mul ( i , - 1 ))
\heuristics (polySimp_expand , polySimp_elimSubNeg )
};defined in: integerSimplificationRules.key Line: 1618 Offset :4polySimp_elimOne {
\find ( mul ( i , 1 ))
\replacewith ( i )
\heuristics (polySimp_expand , polySimp_elimOneRight )
};defined in: integerSimplificationRules.key Line: 1624 Offset :4polySimp_elimOneLeft0 {
\find ( mul ( 1 , i ))
\replacewith ( i )
\heuristics (polySimp_expand , polySimp_elimOneLeft )
};defined in: integerSimplificationRules.key Line: 1630 Offset :4polySimp_elimOneLeft1 {
\find ( mul ( mul ( i0 , 1 ), i ))
\replacewith ( mul ( i0 , i ))
\heuristics (polySimp_expand , polySimp_elimOneLeft )
};defined in: integerSimplificationRules.key Line: 1636 Offset :4polySimp_homoEq {
\find ( homoLeft = homoRight )
\replacewith ( add ( homoRight , mul ( homoLeft , - 1 ))= 0 )
\heuristics (polySimp_expand , polySimp_homo , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1642 Offset :4polySimp_rightDist {
\find ( mul ( distCoeff , add ( distSummand0 , distSummand1 )))
\replacewith ( add ( mul ( distCoeff , distSummand0 ), mul ( distSummand1 , distCoeff )))
\heuristics (polySimp_expand , polySimp_dist )
};defined in: integerSimplificationRules.key Line: 1648 Offset :4polySimp_addAssoc {
\find ( add ( addAssocPoly0 , add ( addAssocPoly1 , addAssocMono )))
\replacewith ( add ( add ( addAssocPoly0 , addAssocPoly1 ), addAssocMono ))
\heuristics (polySimp_expand , polySimp_addAssoc )
};defined in: integerSimplificationRules.key Line: 1655 Offset :4polySimp_mulAssoc {
\find ( mul ( mulAssocMono0 , mul ( mulAssocMono1 , mulAssocAtom )))
\replacewith ( mul ( mul ( mulAssocMono0 , mulAssocMono1 ), mulAssocAtom ))
\heuristics (polySimp_expand , polySimp_mulAssoc )
};defined in: integerSimplificationRules.key Line: 1661 Offset :4polySimp_addComm0 {
\find ( add ( commLeft , commRight ))
\replacewith ( add ( commRight , commLeft ))
\heuristics (polySimp_expand , polySimp_addOrder )
};defined in: integerSimplificationRules.key Line: 1667 Offset :4polySimp_addComm1 {
\find ( add ( add ( i0 , commLeft ), commRight ))
\replacewith ( add ( add ( i0 , commRight ), commLeft ))
\heuristics (polySimp_expand , polySimp_addOrder )
};defined in: integerSimplificationRules.key Line: 1673 Offset :4polySimp_mulComm0 {
\find ( mul ( commLeft , commRight ))
\replacewith ( mul ( commRight , commLeft ))
\heuristics (polySimp_expand , polySimp_mulOrder )
};defined in: integerSimplificationRules.key Line: 1679 Offset :4polySimp_mulComm1 {
\find ( mul ( mul ( i0 , commLeft ), commRight ))
\replacewith ( mul ( mul ( i0 , commRight ), commLeft ))
\heuristics (polySimp_expand , polySimp_mulOrder )
};defined in: integerSimplificationRules.key Line: 1685 Offset :4polySimp_addLiterals {
\find ( add ( add ( i , Z ( iz )), Z ( jz )))
\replacewith ( add ( i , #add ( Z ( iz ), Z ( jz ))))
\heuristics (simplify_literals )
};defined in: integerSimplificationRules.key Line: 1691 Offset :4polySimp_mulLiterals {
\find ( mul ( mul ( i , Z ( iz )), Z ( jz )))
\replacewith ( mul ( i , #mul ( Z ( iz ), Z ( jz ))))
\heuristics (simplify_literals )
};defined in: integerSimplificationRules.key Line: 1697 Offset :4polySimp_pullOutFactor0 {
\find ( add ( mul ( pullOutCommon , pullOutLeft ), mul ( pullOutCommon , pullOutRight )))
\replacewith ( mul ( pullOutCommon , add ( pullOutLeft , pullOutRight )))
\heuristics (polySimp_expand , polySimp_pullOutFactor )
};defined in: integerSimplificationRules.key Line: 1703 Offset :4polySimp_pullOutFactor1 {
\find ( add ( pullOutCommon , mul ( pullOutCommon , pullOutRight )))
\replacewith ( mul ( pullOutCommon , add ( 1 , pullOutRight )))
\heuristics (polySimp_expand , polySimp_pullOutFactor )
};defined in: integerSimplificationRules.key Line: 1711 Offset :4polySimp_pullOutFactor2 {
\find ( add ( mul ( pullOutCommon , pullOutLeft ), pullOutCommon ))
\replacewith ( mul ( pullOutCommon , add ( pullOutLeft , 1 )))
\heuristics (polySimp_expand , polySimp_pullOutFactor )
};defined in: integerSimplificationRules.key Line: 1719 Offset :4polySimp_pullOutFactor3 {
\find ( add ( pullOutCommon , pullOutCommon ))
\replacewith ( mul ( pullOutCommon , 2 ))
\heuristics (polySimp_expand , polySimp_pullOutFactor )
};defined in: integerSimplificationRules.key Line: 1727 Offset :4polySimp_pullOutFactor0b {
\find ( add ( add ( i0 , mul ( pullOutCommon , pullOutLeft )), mul ( pullOutCommon , pullOutRight )))
\replacewith ( add ( i0 , mul ( pullOutCommon , add ( pullOutLeft , pullOutRight ))))
\heuristics (polySimp_expand , polySimp_pullOutFactor )
};defined in: integerSimplificationRules.key Line: 1733 Offset :4polySimp_pullOutFactor1b {
\find ( add ( add ( i0 , pullOutCommon ), mul ( pullOutCommon , pullOutRight )))
\replacewith ( add ( i0 , mul ( pullOutCommon , add ( 1 , pullOutRight ))))
\heuristics (polySimp_expand , polySimp_pullOutFactor )
};defined in: integerSimplificationRules.key Line: 1741 Offset :4polySimp_pullOutFactor2b {
\find ( add ( add ( i0 , mul ( pullOutCommon , pullOutLeft )), pullOutCommon ))
\replacewith ( add ( i0 , mul ( pullOutCommon , add ( pullOutLeft , 1 ))))
\heuristics (polySimp_expand , polySimp_pullOutFactor )
};defined in: integerSimplificationRules.key Line: 1749 Offset :4polySimp_pullOutFactor3b {
\find ( add ( add ( i0 , pullOutCommon ), pullOutCommon ))
\replacewith ( add ( i0 , mul ( pullOutCommon , 2 )))
\heuristics (polySimp_expand , polySimp_pullOutFactor )
};defined in: integerSimplificationRules.key Line: 1757 Offset :4polySimp_invertEq {
\find ( invertLeft = invertRight )
\replacewith ( invertLeft * ( - 1 )= invertRight * ( - 1 ))
\heuristics (polySimp_directEquations , polySimp_normalise )
};defined in: integerSimplificationRules.key Line: 1763 Offset :4polySimp_sepPosMonomial {
\find ( add ( sepResidue , sepPosMono )= 0 )
\replacewith ( sepPosMono = mul ( sepResidue , - 1 ))
\heuristics (polySimp_directEquations , polySimp_balance , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1769 Offset :4polySimp_sepNegMonomial {
\find ( add ( sepResidue , sepNegMono )= 0 )
\replacewith ( mul ( sepNegMono , - 1 )= sepResidue )
\heuristics (polySimp_directEquations , polySimp_balance )
};defined in: integerSimplificationRules.key Line: 1775 Offset :4apply_eq_monomials {
\assumes ( applyEqDivisor = i0 ==> )
\find ( applyEqDividend )
\sameUpdateLevel
\replacewith ( #divideMonomials ( applyEqDividend , applyEqDivisor )* ( i0 + applyEqDivisor * - 1 )+ applyEqDividend )
\heuristics (polySimp_applyEq , apply_equations , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1781 Offset :4apply_eq_monomials_rigid {
\assumes ( applyEqDivisorr = i0r ==> )
\find ( applyEqDividend )
\replacewith ( #divideMonomials ( applyEqDividend , applyEqDivisorr )* ( i0r + applyEqDivisorr * - 1 )+ applyEqDividend )
\heuristics (polySimp_applyEqRigid , apply_equations , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1791 Offset :4apply_eq_pseudo_eq {
\assumes ( aePseudoLeft * aePseudoLeftCoeff = aePseudoRight ==> )
\find ( aePseudoTargetLeft = aePseudoTargetRight )
\sameUpdateLevel
\replacewith ( \if ( aePseudoTargetLeft = aePseudoLeft * aePseudoTargetFactor & aePseudoLeftCoeff != 0 )\then ( aePseudoRight * aePseudoTargetFactor = aePseudoTargetRight * aePseudoLeftCoeff )\else ( aePseudoTargetLeft = aePseudoTargetRight ))
\heuristics (polySimp_leftNonUnit , polySimp_applyEqPseudo , notHumanReadable , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1800 Offset :4apply_eq_pseudo_leq {
\assumes ( aePseudoLeft * aePseudoLeftCoeff = aePseudoRight ==> )
\find ( aePseudoTargetLeft <= aePseudoTargetRight )
\sameUpdateLevel
\replacewith ( \if ( aePseudoTargetLeft = aePseudoLeft * aePseudoTargetFactor & aePseudoLeftCoeff > 0 )\then ( aePseudoRight * aePseudoTargetFactor <= aePseudoTargetRight * aePseudoLeftCoeff )\else ( aePseudoTargetLeft <= aePseudoTargetRight ))
\heuristics (polySimp_leftNonUnit , polySimp_applyEqPseudo , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1812 Offset :4apply_eq_pseudo_geq {
\assumes ( aePseudoLeft * aePseudoLeftCoeff = aePseudoRight ==> )
\find ( aePseudoTargetLeft >= aePseudoTargetRight )
\sameUpdateLevel
\replacewith ( \if ( aePseudoTargetLeft = aePseudoLeft * aePseudoTargetFactor & aePseudoLeftCoeff > 0 )\then ( aePseudoRight * aePseudoTargetFactor >= aePseudoTargetRight * aePseudoLeftCoeff )\else ( aePseudoTargetLeft >= aePseudoTargetRight ))
\heuristics (polySimp_leftNonUnit , polySimp_applyEqPseudo , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1824 Offset :4polySimp_critPair {
\assumes ( cpLeft1 = cpRight1 ==> )
\find ( cpLeft2 = cpRight2 ==> )
\add ( #divideLCRMonomials ( cpLeft2 , cpLeft1 )* ( - 1 * cpRight1 + cpLeft1 )+ #divideLCRMonomials ( cpLeft1 , cpLeft2 )* ( cpRight2 + - 1 * cpLeft2 )= 0 ==> )
\heuristics (polySimp_saturate , polySimp_critPair , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1836 Offset :4inEqSimp_ltRight {
\find ( ==> i < i0 )
\replacewith ( ( - 1 )* i0 + i >= 0 ==> )
\heuristics (inEqSimp_expand , inEqSimp_moveLeft , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1856 Offset :4inEqSimp_gtRight {
\find ( ==> i > i0 )
\replacewith ( ( - 1 )* i0 + i <= 0 ==> )
\heuristics (inEqSimp_expand , inEqSimp_moveLeft , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1862 Offset :4inEqSimp_leqRight {
\find ( ==> i <= i0 )
\replacewith ( ( - 1 )+ ( - 1 )* i0 + i >= 0 ==> )
\heuristics (inEqSimp_expand , inEqSimp_moveLeft , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1868 Offset :4inEqSimp_geqRight {
\find ( ==> i >= i0 )
\replacewith ( 1 + ( - 1 )* i0 + i <= 0 ==> )
\heuristics (inEqSimp_expand , inEqSimp_moveLeft , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1874 Offset :4inEqSimp_ltToLeq {
\find ( i < i0 )
\replacewith ( 1 + ( - 1 )* i0 + i <= 0 )
\heuristics (inEqSimp_expand , inEqSimp_makeNonStrict , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1880 Offset :4inEqSimp_gtToGeq {
\find ( i > i0 )
\replacewith ( ( - 1 )+ ( - 1 )* i0 + i >= 0 )
\heuristics (inEqSimp_expand , inEqSimp_makeNonStrict , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1886 Offset :4inEqSimp_commuteLeq {
\find ( commLeft <= commRight )
\replacewith ( commRight >= commLeft )
\heuristics (inEqSimp_expand , inEqSimp_commute )
};defined in: integerSimplificationRules.key Line: 1892 Offset :4inEqSimp_commuteGeq {
\find ( commLeft >= commRight )
\replacewith ( commRight <= commLeft )
\heuristics (inEqSimp_expand , inEqSimp_commute )
};defined in: integerSimplificationRules.key Line: 1898 Offset :4inEqSimp_homoInEq0 {
\find ( homoLeft <= homoRight )
\replacewith ( add ( homoRight , mul ( homoLeft , - 1 ))>= 0 )
\heuristics (inEqSimp_expand , inEqSimp_homo , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1904 Offset :4inEqSimp_homoInEq1 {
\find ( homoLeft >= homoRight )
\replacewith ( add ( homoRight , mul ( homoLeft , - 1 ))<= 0 )
\heuristics (inEqSimp_expand , inEqSimp_homo , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1910 Offset :4inEqSimp_invertInEq0 {
\find ( invertLeft <= invertRight )
\replacewith ( invertLeft * ( - 1 )>= invertRight * ( - 1 ))
\heuristics (inEqSimp_directInEquations , inEqSimp_normalise , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1916 Offset :4inEqSimp_invertInEq1 {
\find ( invertLeft >= invertRight )
\replacewith ( invertLeft * ( - 1 )<= invertRight * ( - 1 ))
\heuristics (inEqSimp_directInEquations , inEqSimp_normalise , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1922 Offset :4inEqSimp_sepPosMonomial0 {
\find ( add ( sepResidue , sepPosMono )<= 0 )
\replacewith ( sepPosMono <= mul ( sepResidue , - 1 ))
\heuristics (inEqSimp_directInEquations , inEqSimp_balance , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1928 Offset :4inEqSimp_sepNegMonomial0 {
\find ( add ( sepResidue , sepNegMono )<= 0 )
\replacewith ( mul ( sepNegMono , - 1 )>= sepResidue )
\heuristics (inEqSimp_directInEquations , inEqSimp_balance , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1934 Offset :4inEqSimp_sepPosMonomial1 {
\find ( add ( sepResidue , sepPosMono )>= 0 )
\replacewith ( sepPosMono >= mul ( sepResidue , - 1 ))
\heuristics (inEqSimp_directInEquations , inEqSimp_balance , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1940 Offset :4inEqSimp_sepNegMonomial1 {
\find ( add ( sepResidue , sepNegMono )>= 0 )
\replacewith ( mul ( sepNegMono , - 1 )<= sepResidue )
\heuristics (inEqSimp_directInEquations , inEqSimp_balance , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1946 Offset :4inEqSimp_antiSymm {
\assumes ( i <= i0 ==> )
\find ( i >= i0 ==> )
\add ( i = i0 ==> )
\heuristics (inEqSimp_saturate , inEqSimp_antiSymm )
};defined in: integerSimplificationRules.key Line: 1952 Offset :4inEqSimp_exactShadow0 {
\assumes ( mul ( esLeft , esCoeff1 )<= esRight1 ==> )
\find ( mul ( esLeft , esCoeff2 )>= esRight2 ==> )
\add ( ( esCoeff1 > 0 & esCoeff2 > 0 )-> ( - 1 )* mul ( esCoeff1 , esRight2 )+ mul ( esCoeff2 , esRight1 )>= 0 ==> )
\heuristics (inEqSimp_saturate , inEqSimp_exactShadow , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1959 Offset :4inEqSimp_exactShadow1 {
\assumes ( esLeft <= esRight1 ==> )
\find ( mul ( esLeft , esCoeff2 )>= esRight2 ==> )
\add ( ( esCoeff2 > 0 )-> ( - 1 )* esRight2 + mul ( esCoeff2 , esRight1 )>= 0 ==> )
\heuristics (inEqSimp_saturate , inEqSimp_exactShadow , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1970 Offset :4inEqSimp_exactShadow2 {
\assumes ( mul ( esLeft , esCoeff1 )<= esRight1 ==> )
\find ( esLeft >= esRight2 ==> )
\add ( ( esCoeff1 > 0 )-> ( - 1 )* mul ( esCoeff1 , esRight2 )+ esRight1 >= 0 ==> )
\heuristics (inEqSimp_saturate , inEqSimp_exactShadow , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1980 Offset :4inEqSimp_exactShadow3 {
\assumes ( esLeft <= esRight1 ==> )
\find ( esLeft >= esRight2 ==> )
\add ( ( - 1 )* esRight2 + esRight1 >= 0 ==> )
\heuristics (inEqSimp_saturate , inEqSimp_exactShadow , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1990 Offset :4inEqSimp_subsumption0 {
\assumes ( subsumLeft <= subsumRightSmaller ==> )
\find ( subsumLeft <= subsumRightBigger )
\sameUpdateLevel
\replacewith ( subsumRightSmaller <= subsumRightBigger | subsumLeft <= subsumRightBigger )
\heuristics (inEqSimp_propagation , inEqSimp_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 1997 Offset :4inEqSimp_subsumption1 {
\assumes ( subsumLeft >= subsumRightBigger ==> )
\find ( subsumLeft >= subsumRightSmaller )
\sameUpdateLevel
\replacewith ( subsumRightSmaller <= subsumRightBigger | subsumLeft >= subsumRightSmaller )
\heuristics (inEqSimp_propagation , inEqSimp_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2006 Offset :4inEqSimp_subsumption2 {
\assumes ( subsumLeft * subsumCoeffSmaller <= subsumRightSmaller ==> )
\find ( subsumLeft * subsumCoeffBigger <= subsumRightBigger )
\sameUpdateLevel
\replacewith ( ( subsumCoeffSmaller > 0 & subsumCoeffBigger > 0 & subsumCoeffBigger * subsumRightSmaller <= subsumCoeffSmaller * subsumRightBigger )| subsumLeft * subsumCoeffBigger <= subsumRightBigger )
\heuristics (inEqSimp_propagation , inEqSimp_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2015 Offset :4inEqSimp_subsumption4 {
\assumes ( subsumLeft <= subsumRightSmaller ==> )
\find ( subsumLeft * subsumCoeffBigger <= subsumRightBigger )
\sameUpdateLevel
\replacewith ( ( subsumCoeffBigger > 0 & subsumCoeffBigger * subsumRightSmaller <= subsumRightBigger )| subsumLeft * subsumCoeffBigger <= subsumRightBigger )
\heuristics (inEqSimp_propagation , inEqSimp_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2027 Offset :4inEqSimp_subsumption5 {
\assumes ( subsumLeft * subsumCoeffBigger >= subsumRightBigger ==> )
\find ( subsumLeft * subsumCoeffSmaller >= subsumRightSmaller )
\sameUpdateLevel
\replacewith ( ( subsumCoeffSmaller > 0 & subsumCoeffBigger > 0 & subsumCoeffBigger * subsumRightSmaller <= subsumCoeffSmaller * subsumRightBigger )| subsumLeft * subsumCoeffSmaller >= subsumRightSmaller )
\heuristics (inEqSimp_propagation , inEqSimp_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2038 Offset :4inEqSimp_subsumption6 {
\assumes ( subsumLeft >= subsumRightBigger ==> )
\find ( subsumLeft * subsumCoeffSmaller >= subsumRightSmaller )
\sameUpdateLevel
\replacewith ( ( subsumCoeffSmaller > 0 & subsumRightSmaller <= subsumCoeffSmaller * subsumRightBigger )| subsumLeft * subsumCoeffSmaller >= subsumRightSmaller )
\heuristics (inEqSimp_propagation , inEqSimp_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2050 Offset :4inEqSimp_contradInEq0 {
\assumes ( contradLeft <= contradRightSmaller ==> )
\find ( contradLeft >= contradRightBigger )
\sameUpdateLevel
\replacewith ( contradRightSmaller >= contradRightBigger & contradLeft >= contradRightBigger )
\heuristics (inEqSimp_propagation , inEqSimp_contradInEqs , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2061 Offset :4inEqSimp_contradInEq1 {
\assumes ( contradLeft >= contradRightBigger ==> )
\find ( contradLeft <= contradRightSmaller )
\sameUpdateLevel
\replacewith ( contradRightSmaller >= contradRightBigger & contradLeft <= contradRightSmaller )
\heuristics (inEqSimp_propagation , inEqSimp_contradInEqs , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2070 Offset :4inEqSimp_contradInEq2 {
\assumes ( contradLeft * contradCoeffSmaller <= contradRightSmaller ==> )
\find ( contradLeft * contradCoeffBigger >= contradRightBigger )
\sameUpdateLevel
\replacewith ( ( contradCoeffSmaller > 0 -> contradCoeffBigger > 0 -> contradCoeffBigger * contradRightSmaller >= contradCoeffSmaller * contradRightBigger )& contradLeft * contradCoeffBigger >= contradRightBigger )
\heuristics (inEqSimp_propagation , inEqSimp_contradInEqs , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2079 Offset :4inEqSimp_contradInEq3 {
\assumes ( contradLeft <= contradRightSmaller ==> )
\find ( contradLeft * contradCoeffBigger >= contradRightBigger )
\sameUpdateLevel
\replacewith ( ( contradCoeffBigger > 0 -> contradCoeffBigger * contradRightSmaller >= contradRightBigger )& contradLeft * contradCoeffBigger >= contradRightBigger )
\heuristics (inEqSimp_propagation , inEqSimp_contradInEqs , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2091 Offset :4inEqSimp_contradInEq4 {
\assumes ( contradLeft * contradCoeffBigger >= contradRightBigger ==> )
\find ( contradLeft * contradCoeffSmaller <= contradRightSmaller )
\sameUpdateLevel
\replacewith ( ( contradCoeffSmaller > 0 -> contradCoeffBigger > 0 -> contradCoeffBigger * contradRightSmaller >= contradCoeffSmaller * contradRightBigger )& contradLeft * contradCoeffSmaller <= contradRightSmaller )
\heuristics (inEqSimp_propagation , inEqSimp_contradInEqs , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2102 Offset :4inEqSimp_contradInEq5 {
\assumes ( contradLeft >= contradRightBigger ==> )
\find ( contradLeft * contradCoeffSmaller <= contradRightSmaller )
\sameUpdateLevel
\replacewith ( ( contradCoeffSmaller > 0 -> contradRightSmaller >= contradCoeffSmaller * contradRightBigger )& contradLeft * contradCoeffSmaller <= contradRightSmaller )
\heuristics (inEqSimp_propagation , inEqSimp_contradInEqs , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2114 Offset :4inEqSimp_strengthen0 {
\assumes ( ==> strengthenLeft = strengthenRight )
\find ( strengthenLeft <= strengthenRight ==> )
\replacewith ( strengthenLeft <= - 1 + strengthenRight ==> )
\heuristics (inEqSimp_propagation , inEqSimp_strengthen , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2125 Offset :4inEqSimp_strengthen1 {
\assumes ( ==> strengthenLeft = strengthenRight )
\find ( strengthenLeft >= strengthenRight ==> )
\replacewith ( strengthenLeft >= 1 + strengthenRight ==> )
\heuristics (inEqSimp_propagation , inEqSimp_strengthen , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2132 Offset :4inEqSimp_contradEq3 {
\assumes ( contradLeft <= contradRightSmaller ==> )
\find ( contradLeft = contradRightBigger )
\sameUpdateLevel
\replacewith ( contradRightSmaller + ( - 1 )* contradRightBigger >= 0 & contradLeft = contradRightBigger )
\heuristics (inEqSimp_propagation , inEqSimp_contradEqs , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2139 Offset :4inEqSimp_contradEq7 {
\assumes ( contradLeft >= contradRightBigger ==> )
\find ( contradLeft = contradRightSmaller )
\sameUpdateLevel
\replacewith ( contradRightBigger + ( - 1 )* contradRightSmaller <= 0 & contradLeft = contradRightSmaller )
\heuristics (inEqSimp_propagation , inEqSimp_contradEqs , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2148 Offset :4\lemma irrflConcrete1 {
\find ( i < i ==> )
\replacewith ( false ==> )
\heuristics (concrete )
};defined in: integerSimplificationRules.key Line: 2157 Offset :4\lemma irrflConcrete2 {
\find ( i > i ==> )
\replacewith ( false ==> )
\heuristics (concrete )
};defined in: integerSimplificationRules.key Line: 2163 Offset :4inEqSimp_notLeq {
\find ( ! ( i <= i0 ))
\replacewith ( ( - 1 )+ ( - 1 )* i0 + i >= 0 )
\heuristics (inEqSimp_forNormalisation , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2201 Offset :4inEqSimp_notGeq {
\find ( ! ( i >= i0 ))
\replacewith ( 1 + ( - 1 )* i0 + i <= 0 )
\heuristics (inEqSimp_forNormalisation , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2207 Offset :4inEqSimp_and_antiSymm0 {
\find ( i <= i0 & i >= i0 )
\replacewith ( i = i0 )
\heuristics (inEqSimp_forNormalisation )
};defined in: integerSimplificationRules.key Line: 2213 Offset :4inEqSimp_and_antiSymm1 {
\find ( ( b & i <= i0 )& i >= i0 )
\replacewith ( b & i = i0 )
\heuristics (inEqSimp_forNormalisation )
};defined in: integerSimplificationRules.key Line: 2219 Offset :4inEqSimp_and_contradInEq0 {
\find ( contradLeft <= contradRightSmaller & contradLeft >= contradRightBigger )
\replacewith ( ( contradLeft <= contradRightSmaller & contradLeft >= contradRightBigger )& contradRightSmaller >= contradRightBigger )
\heuristics (inEqSimp_forNormalisation , inEqSimp_and_contradInEqs , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2225 Offset :4inEqSimp_and_contradInEq1 {
\find ( ( b & contradLeft <= contradRightSmaller )& contradLeft >= contradRightBigger )
\replacewith ( ( ( b & contradLeft <= contradRightSmaller )& contradLeft >= contradRightBigger )& contradRightSmaller >= contradRightBigger )
\heuristics (inEqSimp_forNormalisation , inEqSimp_and_contradInEqs , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2236 Offset :4inEqSimp_and_strengthen0 {
\find ( strengthenLeft <= strengthenRight & strengthenLeft != strengthenRight )
\replacewith ( strengthenLeft <= - 1 + strengthenRight )
\heuristics (inEqSimp_forNormalisation , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2247 Offset :4inEqSimp_and_strengthen1 {
\find ( strengthenLeft >= strengthenRight & strengthenLeft != strengthenRight )
\replacewith ( strengthenLeft >= 1 + strengthenRight )
\heuristics (inEqSimp_forNormalisation , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2255 Offset :4inEqSimp_and_strengthen2 {
\find ( ( b & strengthenLeft <= strengthenRight )& strengthenLeft != strengthenRight )
\replacewith ( b & strengthenLeft <= - 1 + strengthenRight )
\heuristics (inEqSimp_forNormalisation , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2262 Offset :4inEqSimp_and_strengthen3 {
\find ( ( b & strengthenLeft >= strengthenRight )& strengthenLeft != strengthenRight )
\replacewith ( b & strengthenLeft >= 1 + strengthenRight )
\heuristics (inEqSimp_forNormalisation , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2270 Offset :4inEqSimp_and_subsumption0 {
\find ( subsumLeft <= subsumRightSmaller & subsumLeft <= subsumRightBigger )
\replacewith ( subsumLeft <= subsumRightSmaller & ( subsumRightSmaller <= subsumRightBigger | subsumLeft <= subsumRightBigger ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_andOr_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2277 Offset :4inEqSimp_and_subsumption1 {
\find ( ( b & subsumLeft <= subsumRightSmaller )& subsumLeft <= subsumRightBigger )
\replacewith ( ( b & subsumLeft <= subsumRightSmaller )& ( subsumRightSmaller <= subsumRightBigger | subsumLeft <= subsumRightBigger ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_andOr_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2287 Offset :4inEqSimp_and_subsumption2 {
\find ( subsumLeft >= subsumRightSmaller & subsumLeft >= subsumRightBigger )
\replacewith ( ( subsumRightSmaller <= subsumRightBigger | subsumLeft >= subsumRightSmaller )& subsumLeft >= subsumRightBigger )
\heuristics (inEqSimp_forNormalisation , inEqSimp_andOr_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2297 Offset :4inEqSimp_and_subsumption3 {
\find ( ( b & subsumLeft >= subsumRightSmaller )& subsumLeft >= subsumRightBigger )
\replacewith ( ( b & ( subsumRightSmaller <= subsumRightBigger | subsumLeft >= subsumRightSmaller ))& subsumLeft >= subsumRightBigger )
\heuristics (inEqSimp_forNormalisation , inEqSimp_andOr_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2307 Offset :4inEqSimp_and_subsumption4 {
\find ( subsumLeft <= subsumRightSmaller & subsumLeft != subsumRightBigger )
\replacewith ( subsumLeft <= subsumRightSmaller & ( subsumRightSmaller < subsumRightBigger | subsumLeft != subsumRightBigger ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_and_subsumptionEq , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2317 Offset :4inEqSimp_and_subsumption5 {
\find ( ( b & subsumLeft <= subsumRightSmaller )& subsumLeft != subsumRightBigger )
\replacewith ( ( b & subsumLeft <= subsumRightSmaller )& ( subsumRightSmaller < subsumRightBigger | subsumLeft != subsumRightBigger ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_and_subsumptionEq , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2327 Offset :4inEqSimp_and_subsumption6 {
\find ( subsumLeft >= subsumRightBigger & subsumLeft != subsumRightSmaller )
\replacewith ( subsumLeft >= subsumRightBigger & ( subsumRightSmaller < subsumRightBigger | subsumLeft != subsumRightSmaller ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_and_subsumptionEq , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2337 Offset :4inEqSimp_and_subsumption7 {
\find ( ( b & subsumLeft >= subsumRightBigger )& subsumLeft != subsumRightSmaller )
\replacewith ( ( b & subsumLeft >= subsumRightBigger )& ( subsumRightSmaller < subsumRightBigger | subsumLeft != subsumRightSmaller ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_and_subsumptionEq , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2347 Offset :4inEqSimp_or_antiSymm0 {
\find ( antiSymmLeft <= antiSymmRightSmaller | antiSymmLeft >= antiSymmRightBigger )
\replacewith ( \if ( 2 + antiSymmRightSmaller = antiSymmRightBigger )\then ( antiSymmLeft != 1 + antiSymmRightSmaller )\else ( antiSymmLeft <= antiSymmRightSmaller | antiSymmLeft >= antiSymmRightBigger ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_or_antiSymm , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2357 Offset :4inEqSimp_or_antiSymm1 {
\find ( ( b | antiSymmLeft <= antiSymmRightSmaller )| antiSymmLeft >= antiSymmRightBigger )
\replacewith ( b | \if ( 2 + antiSymmRightSmaller = antiSymmRightBigger )\then ( antiSymmLeft != 1 + antiSymmRightSmaller )\else ( antiSymmLeft <= antiSymmRightSmaller | antiSymmLeft >= antiSymmRightBigger ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_or_antiSymm , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2368 Offset :4inEqSimp_or_tautInEq0 {
\find ( tautLeft <= tautRightBigger | tautLeft >= tautRightSmaller )
\replacewith ( ( tautLeft <= tautRightBigger | tautLeft >= tautRightSmaller )| tautRightBigger >= ( - 1 )+ tautRightSmaller )
\heuristics (inEqSimp_forNormalisation , inEqSimp_or_tautInEqs , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2380 Offset :4inEqSimp_or_tautInEq1 {
\find ( ( b | tautLeft <= tautRightBigger )| tautLeft >= tautRightSmaller )
\replacewith ( ( ( b | tautLeft <= tautRightBigger )| tautLeft >= tautRightSmaller )| tautRightBigger >= ( - 1 )+ tautRightSmaller )
\heuristics (inEqSimp_forNormalisation , inEqSimp_or_tautInEqs , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2389 Offset :4inEqSimp_or_tautInEq2 {
\find ( tautLeft >= tautRightSmaller | tautLeft <= tautRightBigger )
\replacewith ( ( tautLeft >= tautRightSmaller | tautLeft <= tautRightBigger )| tautRightBigger >= ( - 1 )+ tautRightSmaller )
\heuristics (inEqSimp_forNormalisation , inEqSimp_or_tautInEqs , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2398 Offset :4inEqSimp_or_tautInEq3 {
\find ( ( b | tautLeft >= tautRightSmaller )| tautLeft <= tautRightBigger )
\replacewith ( ( ( b | tautLeft >= tautRightSmaller )| tautLeft <= tautRightBigger )| tautRightBigger >= ( - 1 )+ tautRightSmaller )
\heuristics (inEqSimp_forNormalisation , inEqSimp_or_tautInEqs , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2407 Offset :4inEqSimp_or_weaken0 {
\find ( weakenLeft <= weakenRightSmaller | weakenLeft = weakenRightBigger )
\replacewith ( \if ( weakenRightBigger = 1 + weakenRightSmaller )\then ( weakenLeft <= weakenRightBigger )\else ( weakenLeft <= weakenRightSmaller | weakenLeft = weakenRightBigger ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_or_weaken , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2416 Offset :4inEqSimp_or_weaken1 {
\find ( weakenLeft = weakenRightSmaller | weakenLeft >= weakenRightBigger )
\replacewith ( \if ( weakenRightBigger = 1 + weakenRightSmaller )\then ( weakenLeft >= weakenRightSmaller )\else ( weakenLeft = weakenRightSmaller | weakenLeft >= weakenRightBigger ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_or_weaken , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2426 Offset :4inEqSimp_or_weaken2 {
\find ( ( b | weakenLeft <= weakenRightSmaller )| weakenLeft = weakenRightBigger )
\replacewith ( b | \if ( weakenRightBigger = 1 + weakenRightSmaller )\then ( weakenLeft <= weakenRightBigger )\else ( weakenLeft <= weakenRightSmaller | weakenLeft = weakenRightBigger ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_or_weaken , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2436 Offset :4inEqSimp_or_weaken3 {
\find ( ( b | weakenLeft = weakenRightSmaller )| weakenLeft >= weakenRightBigger )
\replacewith ( b | \if ( weakenRightBigger = 1 + weakenRightSmaller )\then ( weakenLeft >= weakenRightSmaller )\else ( weakenLeft = weakenRightSmaller | weakenLeft >= weakenRightBigger ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_or_weaken , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2447 Offset :4inEqSimp_or_subsumption0 {
\find ( subsumLeft <= subsumRightSmaller | subsumLeft <= subsumRightBigger )
\replacewith ( ( subsumRightSmaller >= subsumRightBigger & subsumLeft <= subsumRightSmaller )| subsumLeft <= subsumRightBigger )
\heuristics (inEqSimp_forNormalisation , inEqSimp_andOr_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2458 Offset :4inEqSimp_or_subsumption1 {
\find ( ( b | subsumLeft <= subsumRightSmaller )| subsumLeft <= subsumRightBigger )
\replacewith ( ( b | ( subsumRightSmaller >= subsumRightBigger & subsumLeft <= subsumRightSmaller ))| subsumLeft <= subsumRightBigger )
\heuristics (inEqSimp_forNormalisation , inEqSimp_andOr_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2469 Offset :4inEqSimp_or_subsumption2 {
\find ( subsumLeft >= subsumRightSmaller | subsumLeft >= subsumRightBigger )
\replacewith ( subsumLeft >= subsumRightSmaller | ( subsumRightSmaller >= subsumRightBigger & subsumLeft >= subsumRightBigger ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_andOr_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2480 Offset :4inEqSimp_or_subsumption3 {
\find ( ( b | subsumLeft >= subsumRightSmaller )| subsumLeft >= subsumRightBigger )
\replacewith ( ( b | subsumLeft >= subsumRightSmaller )| ( subsumRightSmaller >= subsumRightBigger & subsumLeft >= subsumRightBigger ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_andOr_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2491 Offset :4inEqSimp_or_subsumption4 {
\find ( subsumLeft = subsumRightSmaller | subsumLeft <= subsumRightBigger )
\replacewith ( ( subsumRightSmaller > subsumRightBigger & subsumLeft = subsumRightSmaller )| subsumLeft <= subsumRightBigger )
\heuristics (inEqSimp_forNormalisation , inEqSimp_andOr_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2502 Offset :4inEqSimp_or_subsumption5 {
\find ( ( b | subsumLeft = subsumRightSmaller )| subsumLeft <= subsumRightBigger )
\replacewith ( ( b | ( subsumRightSmaller > subsumRightBigger & subsumLeft = subsumRightSmaller ))| subsumLeft <= subsumRightBigger )
\heuristics (inEqSimp_forNormalisation , inEqSimp_andOr_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2513 Offset :4inEqSimp_or_subsumption6 {
\find ( subsumLeft >= subsumRightSmaller | subsumLeft = subsumRightBigger )
\replacewith ( subsumLeft >= subsumRightSmaller | ( subsumRightSmaller > subsumRightBigger & subsumLeft = subsumRightBigger ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_andOr_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2524 Offset :4inEqSimp_or_subsumption7 {
\find ( ( b | subsumLeft >= subsumRightSmaller )| subsumLeft = subsumRightBigger )
\replacewith ( ( b | subsumLeft >= subsumRightSmaller )| ( subsumRightSmaller > subsumRightBigger & subsumLeft = subsumRightBigger ))
\heuristics (inEqSimp_forNormalisation , inEqSimp_andOr_subsumption , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2535 Offset :4applyEq_and_int0 {
\find ( applyEqLeft >= applyEqOther & applyEqLeft = applyEqRight )
\replacewith ( applyEqRight >= applyEqOther & applyEqLeft = applyEqRight )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2546 Offset :4applyEq_and_int1 {
\find ( ( b & applyEqLeft >= applyEqOther )& applyEqLeft = applyEqRight )
\replacewith ( ( b & applyEqRight >= applyEqOther )& applyEqLeft = applyEqRight )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2554 Offset :4applyEq_and_int2 {
\find ( applyEqLeft <= applyEqOther & applyEqLeft = applyEqRight )
\replacewith ( applyEqRight <= applyEqOther & applyEqLeft = applyEqRight )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2562 Offset :4applyEq_and_int3 {
\find ( ( b & applyEqLeft <= applyEqOther )& applyEqLeft = applyEqRight )
\replacewith ( ( b & applyEqRight <= applyEqOther )& applyEqLeft = applyEqRight )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2570 Offset :4applyEq_and_int4 {
\find ( applyEqLeft = applyEqRight & applyEqLeft >= applyEqOther )
\replacewith ( applyEqLeft = applyEqRight & applyEqRight >= applyEqOther )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2578 Offset :4applyEq_and_int5 {
\find ( ( b & applyEqLeft = applyEqRight )& applyEqLeft >= applyEqOther )
\replacewith ( ( b & applyEqLeft = applyEqRight )& applyEqRight >= applyEqOther )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2586 Offset :4applyEq_and_int6 {
\find ( applyEqLeft = applyEqRight & applyEqLeft <= applyEqOther )
\replacewith ( applyEqLeft = applyEqRight & applyEqRight <= applyEqOther )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2594 Offset :4applyEq_and_int7 {
\find ( ( b & applyEqLeft = applyEqRight )& applyEqLeft <= applyEqOther )
\replacewith ( ( b & applyEqLeft = applyEqRight )& applyEqRight <= applyEqOther )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2602 Offset :4applyEq_or_int0 {
\find ( applyEqLeft >= applyEqOther | applyEqLeft != applyEqRight )
\replacewith ( applyEqRight >= applyEqOther | applyEqLeft != applyEqRight )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2610 Offset :4applyEq_or_int1 {
\find ( ( b | applyEqLeft >= applyEqOther )| applyEqLeft != applyEqRight )
\replacewith ( ( b | applyEqRight >= applyEqOther )| applyEqLeft != applyEqRight )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2618 Offset :4applyEq_or_int2 {
\find ( applyEqLeft <= applyEqOther | applyEqLeft != applyEqRight )
\replacewith ( applyEqRight <= applyEqOther | applyEqLeft != applyEqRight )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2626 Offset :4applyEq_or_int3 {
\find ( ( b | applyEqLeft <= applyEqOther )| applyEqLeft != applyEqRight )
\replacewith ( ( b | applyEqRight <= applyEqOther )| applyEqLeft != applyEqRight )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2634 Offset :4applyEq_or_int4 {
\find ( applyEqLeft != applyEqRight | applyEqLeft >= applyEqOther )
\replacewith ( applyEqLeft != applyEqRight | applyEqRight >= applyEqOther )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2642 Offset :4applyEq_or_int5 {
\find ( ( b | applyEqLeft != applyEqRight )| applyEqLeft >= applyEqOther )
\replacewith ( ( b | applyEqLeft != applyEqRight )| applyEqRight >= applyEqOther )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2650 Offset :4applyEq_or_int6 {
\find ( applyEqLeft != applyEqRight | applyEqLeft <= applyEqOther )
\replacewith ( applyEqLeft != applyEqRight | applyEqRight <= applyEqOther )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2658 Offset :4applyEq_or_int7 {
\find ( ( b | applyEqLeft != applyEqRight )| applyEqLeft <= applyEqOther )
\replacewith ( ( b | applyEqLeft != applyEqRight )| applyEqRight <= applyEqOther )
\heuristics (apply_equations_andOr )
};defined in: integerSimplificationRules.key Line: 2666 Offset :4cancel_equation {
\schemaVar \term int eqLeft , eqRight , Fac ;
\find ( eqLeft * Fac = eqRight * Fac )
\replacewith ( eqLeft = eqRight );
\add ( ==> Fac != 0 )
\heuristics (simplify_enlarging )
};defined in: integerSimplificationRules.key Line: 2682 Offset :4divide_equation {
\find ( elimGcdLeft = elimGcdRight )
\replacewith ( \if ( elimGcd >= 1 & elimGcdLeft % elimGcd = 0 & elimGcdRight % elimGcd <= ( - 1 )+ elimGcd )\then ( elimGcdRight % elimGcd = 0 & div ( elimGcdLeft , elimGcd )= div ( elimGcdRight , elimGcd ))\else ( elimGcdLeft = elimGcdRight ))
};defined in: integerSimplificationRules.key Line: 2690 Offset :4divide_leq {
\find ( elimGcdLeft <= elimGcdRight )
\replacewith ( \if ( elimGcd >= 1 & elimGcdLeft % elimGcd = 0 & elimGcdRight % elimGcd <= ( - 1 )+ elimGcd )\then ( div ( elimGcdLeft , elimGcd )<= div ( elimGcdRight , elimGcd ))\else ( elimGcdLeft <= elimGcdRight ))
};defined in: integerSimplificationRules.key Line: 2700 Offset :4divide_geq {
\find ( elimGcdLeft >= elimGcdRight )
\replacewith ( \if ( elimGcd >= 1 & elimGcdLeft % elimGcd = 0 & elimGcdRight % elimGcd <= ( - 1 )+ elimGcd )\then ( div ( elimGcdLeft , elimGcd )>= 1 + div ( ( - 1 )+ elimGcdRight , elimGcd ))\else ( elimGcdLeft >= elimGcdRight ))
};defined in: integerSimplificationRules.key Line: 2709 Offset :4elimGcdEq {
\find ( elimGcdLeft = elimGcdRight )
\replacewith ( \if ( elimGcdLeftDiv * elimGcd = elimGcdLeft & elimGcdRight + ( elimGcd * ( - 1 ))* elimGcdRightDiv <= ( - 1 )+ elimGcd & elimGcdRight + ( elimGcd * ( - 1 ))* elimGcdRightDiv >= 0 )\then ( elimGcdRight + ( elimGcd * ( - 1 ))* elimGcdRightDiv = 0 & elimGcdLeftDiv = elimGcdRightDiv )\else ( elimGcdLeft = elimGcdRight ))
\heuristics (polySimp_pullOutGcd , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2719 Offset :4elimGcdLeq {
\find ( elimGcdLeft <= elimGcdRight )
\replacewith ( \if ( 1 - elimGcd + ( elimGcd * ( - 1 ))* elimGcdRightDiv + elimGcdRight + elimGcdLeftDiv * elimGcd + elimGcdLeft * ( - 1 )<= 0 & ( elimGcd * ( - 1 ))* elimGcdRightDiv + elimGcdRight + elimGcdLeftDiv * elimGcd + elimGcdLeft * ( - 1 )>= 0 )\then ( elimGcdLeftDiv <= elimGcdRightDiv )\else ( elimGcdLeft <= elimGcdRight ))
\heuristics (inEqSimp_pullOutGcd , inEqSimp_pullOutGcd_leq , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2732 Offset :4elimGcdGeq {
\find ( elimGcdLeft >= elimGcdRight )
\replacewith ( \if ( elimGcd - 1 + ( elimGcd * ( - 1 ))* elimGcdRightDiv + elimGcdRight + elimGcdLeftDiv * elimGcd + elimGcdLeft * ( - 1 )>= 0 & ( elimGcd * ( - 1 ))* elimGcdRightDiv + elimGcdRight + elimGcdLeftDiv * elimGcd + elimGcdLeft * ( - 1 )<= 0 )\then ( elimGcdLeftDiv >= elimGcdRightDiv )\else ( elimGcdLeft >= elimGcdRight ))
\heuristics (inEqSimp_pullOutGcd , inEqSimp_pullOutGcd_geq , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2746 Offset :4elimGcdLeq_antec {
\find ( elimGcdLeft <= elimGcdRight ==> )
\replacewith ( elimGcd <= 0 | - elimGcd + ( elimGcd * ( - 1 ))* elimGcdRightDiv + elimGcdRight + elimGcdLeftDiv * elimGcd + elimGcdLeft * ( - 1 )>= 0 | elimGcdLeftDiv <= elimGcdRightDiv ==> )
\heuristics (inEqSimp_pullOutGcd , inEqSimp_pullOutGcd_leq , inEqSimp_pullOutGcd_antec , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2760 Offset :4elimGcdGeq_antec {
\find ( elimGcdLeft >= elimGcdRight ==> )
\replacewith ( elimGcd <= 0 | elimGcd + ( elimGcd * ( - 1 ))* elimGcdRightDiv + elimGcdRight + elimGcdLeftDiv * elimGcd + elimGcdLeft * ( - 1 )<= 0 | elimGcdLeftDiv >= elimGcdRightDiv ==> )
\heuristics (inEqSimp_pullOutGcd , inEqSimp_pullOutGcd_geq , inEqSimp_pullOutGcd_antec , notHumanReadable )
};defined in: integerSimplificationRules.key Line: 2771 Offset :4sign_case_distinction {
"#signCasesLeft is negative" : \add ( signCasesLeft <= - 1 ==> );
"#signCasesLeft is zero" : \add ( signCasesLeft = 0 ==> );
"#signCasesLeft is positive" : \add ( signCasesLeft >= 1 ==> )
\heuristics (inEqSimp_signCases )
};defined in: integerSimplificationRules.key Line: 2789 Offset :4add_non_neg_square {
\add ( squareFac * squareFac >= 0 ==> )
\heuristics (inEqSimp_special_nonLin , inEqSimp_nonNegSquares )
};defined in: integerSimplificationRules.key Line: 2803 Offset :4\lemma moduloIntIsInInt {
\find ( inInt ( moduloInt ( t )))
\replacewith ( true )
\heuristics (concrete )
};defined in: integerSimplificationRules.key Line: 2818 Offset :4\lemma moduloLongIsInLong {
\find ( inLong ( moduloLong ( t )))
\replacewith ( true )
\heuristics (concrete )
};defined in: integerSimplificationRules.key Line: 2826 Offset :4\lemma moduloShortIsInShort {
\find ( inShort ( moduloShort ( t )))
\replacewith ( true )
\heuristics (concrete )
};defined in: integerSimplificationRules.key Line: 2834 Offset :4\lemma moduloByteIsInByte {
\find ( inByte ( moduloByte ( t )))
\replacewith ( true )
\heuristics (concrete )
};defined in: integerSimplificationRules.key Line: 2842 Offset :4\lemma moduloCharIsInChar {
\find ( inChar ( moduloChar ( t )))
\replacewith ( true )
\heuristics (concrete )
};defined in: integerSimplificationRules.key Line: 2850 Offset :4newSym_eq {
\find ( newSymLeft * newSymLeftCoeff = newSymRight ==> )
\varcond \add ( newSymLeft = l + newSymDef ==> )
\heuristics (polySimp_leftNonUnit , polySimp_newSym , polySimp_newSmallSym )
};defined in: integerSimplificationRules.key Line: 2865 Offset :4