jdiv_axiom_inline {
\find ( jdiv ( divNum , divDenom ))
\replacewith ( \if ( divNum >= 0 )\then ( div ( divNum , divDenom ))\else ( div ( divNum * ( - 1 ), divDenom )* ( - 1 )))
\heuristics (defOps_jdiv_inline , notHumanReadable )
};defined in: intDiv.key Line: 22 Offset :4jdiv_axiom {
\find ( jdiv ( divNum , divDenom ))
\sameUpdateLevel
\add ( jdiv ( divNum , divDenom )= \if ( divNum >= 0 )\then ( div ( divNum , divDenom ))\else ( div ( divNum * ( - 1 ), divDenom )* ( - 1 ))==> )
\heuristics (defOps_jdiv , notHumanReadable )
};defined in: intDiv.key Line: 30 Offset :4div_axiom {
\find ( div ( divNum , divDenom ))
\sameUpdateLevel
\varcond \add ( divDenom = 0 | ( div ( divNum , divDenom )= quotient & mul ( quotient , divDenom )<= divNum & \if ( divDenom >= 0 )\then ( mul ( quotient , divDenom )>= 1 + divNum + ( - 1 )* divDenom )\else ( mul ( quotient , divDenom )>= 1 + divNum + divDenom ))==> )
\heuristics (defOps_div , polySimp_newSmallSym , notHumanReadable )
};defined in: intDiv.key Line: 40 Offset :4\lemma div_unique1 {
\schemaVar \variables int a , cnom , x , y ;
\find ( div ( divNum , divDenom ))
\add ( \forall a ; \forall cnom ; \forall x ; \forall y ; ( ( cnom > 0 & x * cnom <= a & y * cnom <= a & x * cnom >= 1 + a - cnom & y * cnom >= 1 + a - cnom )-> x = y )==> )
};defined in: intDiv.key Line: 54 Offset :4\lemma div_unique2 {
\schemaVar \variables int a , cnom , x , y ;
\find ( div ( divNum , divDenom ))
\add ( \forall a ; \forall cnom ; \forall x ; \forall y ; ( ( cnom < 0 & x * cnom <= a & y * cnom <= a & x * cnom >= 1 + a + cnom & y * cnom >= 1 + a + cnom )-> x = y )==> )
};defined in: intDiv.key Line: 63 Offset :4\lemma div_exists {
\schemaVar \variables int a , cnom , qu , rm ;
\find ( div ( divNum , divDenom ))
\add ( \forall cnom ; ( cnom != 0 -> \forall a ; \exists qu ; \exists rm ; ( a = qu * cnom + rm & 0 <= rm & \if ( cnom >= 0 )\then ( mul ( qu , cnom )>= 1 + a + ( - 1 )* cnom & rm < cnom )\else ( mul ( qu , cnom )>= 1 + a + cnom & rm < - cnom )))==> )
};defined in: intDiv.key Line: 72 Offset :4\lemma div_one {
\find ( div ( divNum , 1 ))
\replacewith ( divNum )
\heuristics (concrete )
};defined in: intDiv.key Line: 83 Offset :4\lemma jdiv_one {
\find ( jdiv ( divNum , 1 ))
\replacewith ( divNum )
\heuristics (concrete )
};defined in: intDiv.key Line: 89 Offset :4\lemma div_zero {
\find ( div ( 0 , divDenom ))
\replacewith ( 0 );
\add ( ==> divDenom != 0 )
\heuristics (simplify_enlarging )
};defined in: intDiv.key Line: 96 Offset :4\lemma div_cancel1 {
\find ( div ( divNum * divDenom , divDenom ))
\replacewith ( divNum );
\add ( ==> divDenom != 0 )
\heuristics (simplify_enlarging )
};defined in: intDiv.key Line: 139 Offset :4\lemma div_cancel2 {
\find ( div ( divDenom * divNum , divDenom ))
\replacewith ( divNum );
\add ( ==> divDenom != 0 )
\heuristics (simplify_enlarging )
};defined in: intDiv.key Line: 147 Offset :4\lemma divAddMultDenom {
\schemaVar \term int coef ;
\find ( div ( divNum + coef * divDenom , divDenom ))
\replacewith ( div ( divNum , divDenom )+ coef );
\add ( ==> divDenom != 0 )
\heuristics (simplify_enlarging )
};defined in: intDiv.key Line: 155 Offset :4\lemma divMinus {
\find ( div ( - divNum , divDenom ))
\replacewith ( \if ( div ( divNum , divDenom )* divDenom = divNum )\then ( - div ( divNum , divDenom ))\else ( \if ( divDenom > 0 )\then ( - div ( divNum , divDenom )- 1 )\else ( - div ( divNum , divDenom )+ 1 )));
\add ( ==> divDenom != 0 )
};defined in: intDiv.key Line: 164 Offset :4\lemma divMinusDenom {
\find ( div ( divNum , - divDenom ))
\replacewith ( - div ( divNum , divDenom ));
\add ( ==> divDenom != 0 )
\heuristics (simplify_enlarging )
};defined in: intDiv.key Line: 175 Offset :4\lemma divIncreasingPos {
\schemaVar \variables int divNum1 , divNum2 , divDenom1 ;
\add ( \forall divDenom1 ; ( \forall divNum1 ; ( \forall divNum2 ; ( divDenom1 > 0 & divNum1 <= divNum2 -> div ( divNum1 , divDenom1 )<= div ( divNum2 , divDenom1 ))))==> )
};defined in: intDiv.key Line: 211 Offset :4\lemma divIncreasingNeg {
\schemaVar \variables int divNum1 , divNum2 , divDenom1 ;
\add ( \forall divDenom1 ; ( \forall divNum1 ; ( \forall divNum2 ; ( divDenom1 < 0 & divNum1 <= divNum2 -> div ( divNum1 , divDenom1 )>= div ( divNum2 , divDenom1 ))))==> )
};defined in: intDiv.key Line: 220 Offset :4\lemma jdiv_zero {
\find ( jdiv ( 0 , divDenom ))
\replacewith ( 0 );
\add ( ==> divDenom != 0 )
\heuristics (simplify_enlarging )
};defined in: intDiv.key Line: 229 Offset :4\lemma jdivPulloutMinusDenom {
\find ( jdiv ( divNum , - divDenom ))
\replacewith ( - jdiv ( divNum , divDenom ));
\add ( ==> divDenom != 0 )
\heuristics (simplify_enlarging )
};defined in: intDiv.key Line: 244 Offset :4\lemma jdiv_uniquePosPos {
\schemaVar \variables int a , cnom , x , y ;
\find ( jdiv ( divNum , divDenom ))
\add ( \forall a ; \forall cnom ; \forall x ; \forall y ; ( ( a >= 0 & cnom > 0 & x * cnom <= a & y * cnom <= a & ( x + 1 )* cnom > a & ( y + 1 )* cnom > a )-> x = y )==> )
};defined in: intDiv.key Line: 252 Offset :4\lemma jdiv_uniquePosNeg {
\schemaVar \variables int a , cnom , x , y ;
\find ( jdiv ( divNum , divDenom ))
\add ( \forall a ; \forall cnom ; \forall x ; \forall y ; ( ( a >= 0 & cnom < 0 & x * cnom <= a & y * cnom <= a & ( x - 1 )* cnom > a & ( y - 1 )* cnom > a )-> x = y )==> )
};defined in: intDiv.key Line: 261 Offset :4\lemma jdiv_uniqueNegPos {
\schemaVar \variables int a , cnom , x , y ;
\find ( jdiv ( divNum , divDenom ))
\add ( \forall a ; \forall cnom ; \forall x ; \forall y ; ( ( a < 0 & cnom > 0 & x * cnom >= a & y * cnom >= a & ( x - 1 )* cnom < a & ( y - 1 )* cnom < a )-> x = y )==> )
};defined in: intDiv.key Line: 270 Offset :4\lemma jdiv_uniqueNegNeg {
\schemaVar \variables int a , cnom , x , y ;
\find ( jdiv ( divNum , divDenom ))
\add ( \forall a ; \forall cnom ; \forall x ; \forall y ; ( ( a < 0 & cnom < 0 & x * cnom >= a & y * cnom >= a & ( x + 1 )* cnom < a & ( y + 1 )* cnom < a )-> x = y )==> )
};defined in: intDiv.key Line: 279 Offset :4\lemma jdivMultDenom1 {
\schemaVar \term int cfac ;
\find ( jdiv ( divDenom * cfac , divDenom ))
\replacewith ( cfac );
\add ( ==> divDenom != 0 )
\heuristics (simplify_enlarging )
};defined in: intDiv.key Line: 288 Offset :4\lemma jdivMultDenom2 {
\schemaVar \term int cfac ;
\find ( jdiv ( cfac * divDenom , divDenom ))
\replacewith ( cfac );
\add ( ==> divDenom != 0 )
};defined in: intDiv.key Line: 297 Offset :4jmod_axiom {
\find ( jmod ( divNum , divDenom ))
\replacewith ( divNum + jdiv ( divNum , divDenom )* ( - 1 )* divDenom )
\heuristics (defOps_mod , notHumanReadable )
};defined in: intDiv.key Line: 305 Offset :4mod_axiom {
\find ( mod ( divNum , divDenom ))
\replacewith ( divNum + ( divNum / divDenom )* ( - 1 )* divDenom )
\heuristics (defOps_mod , notHumanReadable )
};defined in: intDiv.key Line: 311 Offset :4\lemma jmodNumZero {
\find ( jmod ( 0 , divDenom ))
\replacewith ( 0 )
\heuristics (concrete )
};defined in: intDiv.key Line: 355 Offset :4\lemma jmodUnique1 {
\schemaVar \variables int a , deb , cmod , x ;
\add ( \forall a ; ( \forall deb ; ( \forall cmod ; ( ( a >= 0 & deb != 0 & 0 <= cmod & ( cmod < \if ( deb > 0 )\then ( deb )\else ( - deb ))& \exists x ; ( a = deb * x + cmod ))-> cmod = jmod ( a , deb ))))==> )
};defined in: intDiv.key Line: 376 Offset :4\lemma jmodUnique2 {
\schemaVar \variables int a , deb , cmod , x ;
\add ( \forall a ; ( \forall deb ; ( \forall cmod ; ( ( a <= 0 & deb != 0 & ( - cmod < \if ( deb > 0 )\then ( deb )\else ( - deb ))& cmod <= 0 & \exists x ; ( a = deb * x + cmod ))-> cmod = jmod ( a , deb ))))==> )
};defined in: intDiv.key Line: 390 Offset :4\lemma jmodDivisibleRep {
\schemaVar \term int D , A ;
\find ( jmod ( D * A , D ))
\replacewith ( 0 );
\add ( ==> D != 0 )
\heuristics (simplify_enlarging )
};defined in: intDiv.key Line: 431 Offset :4\lemma jdivAddMultDenom {
\schemaVar \variables int N , D , A ;
\add ( \forall N ; ( \forall D ; ( \forall A ; ( D != 0 -> ( jdiv ( N + A * D , D )= ( \if ( N = jdiv ( N , D )* D )\then ( jdiv ( N , D )+ A )\else ( \if ( N != jdiv ( N , D )* D & ( N >= 0 <-> N + D * A >= 0 ))\then ( jdiv ( N , D )+ A )\else ( \if ( N != jdiv ( N , D )* D & ( N >= 0 <-> N + D * A < 0 )& ( D > 0 <-> N + D * A < 0 ))\then ( jdiv ( N , D )+ A + 1 )\else ( jdiv ( N , D )+ A - 1 ))))))))==> )
};defined in: intDiv.key Line: 440 Offset :4\lemma jmodAddMultDenomZero {
\schemaVar \term int N , D , A ;
\find ( jmod ( N + A * D , D )= 0 )
\sameUpdateLevel
\replacewith ( jmod ( N , D )= 0 );
\add ( ==> D != 0 )
\heuristics (simplify_enlarging )
};defined in: intDiv.key Line: 466 Offset :4polyDiv_pullOut {
\find ( divNum / divDenom )
\replacewith ( \if ( divDenom = 0 )\then ( divNum / 0 )\else ( ( divNum + polyDivCoeff * ( - 1 )* divDenom )/ divDenom + polyDivCoeff ))
\heuristics (polyDivision , defOps_divModPullOut , notHumanReadable )
};defined in: intDiv.key Line: 476 Offset :4\lemma polyDiv_zero {
\find ( 0 / divDenom )
\replacewith ( \if ( divDenom = 0 )\then ( 0 / 0 )\else ( 0 ))
\heuristics (polyDivision )
};defined in: intDiv.key Line: 485 Offset :4polyMod_pullOut {
\find ( divNum % divDenom )
\replacewith ( ( divNum + polyDivCoeff * ( - 1 )* divDenom )% divDenom )
\heuristics (polyDivision , defOps_divModPullOut , notHumanReadable )
};defined in: intDiv.key Line: 494 Offset :4polyMod_zero {
\find ( 0 % divDenom )
\replacewith ( 0 )
\heuristics (polyDivision , concrete )
};defined in: intDiv.key Line: 501 Offset :4mod_homoEq {
\schemaVar \term int modNumLeft , modNumRight , modDenom ;
\find ( modNumLeft % modDenom = modNumRight % modDenom )
\replacewith ( ( modNumLeft - modNumRight )% modDenom = 0 )
\heuristics (defOps_modHomoEq , notHumanReadable )
};defined in: intDiv.key Line: 516 Offset :4