binaryOrNeutralRight {
\schemaVar \term int left ;
\find ( binaryOr ( left , 0 ))
\replacewith ( left )
\heuristics (concrete )
};defined in: binaryLemmas.key Line: 7 Offset :4binaryOrNeutralLeft {
\schemaVar \term int right ;
\find ( binaryOr ( 0 , right ))
\replacewith ( right )
\heuristics (concrete )
};defined in: binaryLemmas.key Line: 16 Offset :4binaryOrSign {
\schemaVar \term int left , right ;
\find ( binaryOr ( left , right ))
\sameUpdateLevel
\add ( \if ( left >= 0 & right >= 0 )\then ( 1 )\else ( - 1 )* binaryOr ( left , right )>= 0 ==> )
\heuristics (userTaclets1 )
};defined in: binaryLemmas.key Line: 25 Offset :4binaryOrInInt {
\schemaVar \term int left , right ;
\find ( binaryOr ( left , right ))
\sameUpdateLevel
\add ( ( inRangeInt ( left )& inRangeInt ( right ))-> inRangeInt ( binaryOr ( left , right ))==> )
\heuristics (userTaclets1 )
};defined in: binaryLemmas.key Line: 34 Offset :4binaryOrGte {
\schemaVar \term int left , right ;
\find ( binaryOr ( left , right ))
\sameUpdateLevel
\add ( ( left >= 0 & right >= 0 )-> ( binaryOr ( left , right )>= left & binaryOr ( left , right )>= right & binaryOr ( left , right )<= 2 * \if ( left > right )\then ( left )\else ( right ))==> )
\heuristics (userTaclets1 )
};defined in: binaryLemmas.key Line: 43 Offset :4orJintInInt {
\schemaVar \term int left , right ;
\find ( orJint ( left , right ))
\sameUpdateLevel
\add ( inRangeInt ( orJint ( left , right ))==> )
\heuristics (userTaclets1 )
};defined in: binaryLemmas.key Line: 56 Offset :4binaryAndZeroRight {
\schemaVar \term int left ;
\find ( binaryAnd ( left , 0 ))
\replacewith ( 0 )
\heuristics (concrete )
};defined in: binaryLemmas.key Line: 67 Offset :4binaryAndZeroLeft {
\schemaVar \term int right ;
\find ( binaryAnd ( 0 , right ))
\replacewith ( 0 )
\heuristics (concrete )
};defined in: binaryLemmas.key Line: 74 Offset :4binaryAndSymm {
\schemaVar \term int left , right ;
\find ( binaryAnd ( left , right ))
\replacewith ( binaryAnd ( right , left ))
};defined in: binaryLemmas.key Line: 81 Offset :4binaryAndOne {
\schemaVar \term int left ;
\find ( binaryAnd ( left , 1 ))
\replacewith ( \if ( left % 2 = 0 )\then ( 0 )\else ( 1 ))
\heuristics (simplify_enlarging )
};defined in: binaryLemmas.key Line: 87 Offset :4binaryAnd_literals {
\schemaVar \term numbers iz , jz ;
\find ( binaryAnd ( Z ( iz ), Z ( jz )))
\replacewith ( #BinaryAnd ( Z ( iz ), Z ( jz )))
\heuristics (simplify_literals )
\displayname "binary_AND"
};defined in: binaryLemmas.key Line: 99 Offset :4binaryOr_literals {
\schemaVar \term numbers iz , jz ;
\find ( binaryOr ( Z ( iz ), Z ( jz )))
\replacewith ( #BinaryOr ( Z ( iz ), Z ( jz )))
\heuristics (simplify_literals )
\displayname "binary_OR"
};defined in: binaryLemmas.key Line: 109 Offset :4binaryXOr_literals {
\schemaVar \term numbers iz , jz ;
\find ( binaryXOr ( Z ( iz ), Z ( jz )))
\replacewith ( #BinaryXOr ( Z ( iz ), Z ( jz )))
\heuristics (simplify_literals )
\displayname "binary_XOR"
};defined in: binaryLemmas.key Line: 119 Offset :4shiftright_literals {
\schemaVar \term numbers iz , jz ;
\find ( shiftright ( Z ( iz ), Z ( jz )))
\replacewith ( #ShiftRight ( Z ( iz ), Z ( jz )))
\heuristics (simplify_literals )
\displayname "shift"
};defined in: binaryLemmas.key Line: 131 Offset :4shiftleft_literals {
\schemaVar \term numbers iz , jz ;
\find ( shiftleft ( Z ( iz ), Z ( jz )))
\replacewith ( #ShiftLeft ( Z ( iz ), Z ( jz )))
\heuristics (simplify_literals )
\displayname "shift"
};defined in: binaryLemmas.key Line: 141 Offset :4