precOfInt {
\schemaVar \term int a ;
\schemaVar \term int b ;
\find ( prec ( a , b ))
\replacewith ( 0 <= a & a < b )
\heuristics (simplify )
};defined in: precRules.key Line: 7 Offset :4precOfIntPair {
\schemaVar \term int a ;
\schemaVar \term int b ;
\schemaVar \term any x ;
\find ( prec ( a , pair ( b , x )))
\replacewith ( 0 <= a & a <= b )
\heuristics (simplify )
};defined in: precRules.key Line: 18 Offset :4precOfPairInt {
\schemaVar \term int a ;
\schemaVar \term int b ;
\schemaVar \term any x ;
\find ( prec ( pair ( a , x ), b ))
\replacewith ( 0 <= a & a < b )
\heuristics (simplify )
};defined in: precRules.key Line: 30 Offset :4precOfPair {
\schemaVar \term any a1 ;
\schemaVar \term any a2 ;
\schemaVar \term any b1 ;
\schemaVar \term any b2 ;
\find ( prec ( pair ( a1 , b1 ), pair ( a2 , b2 )))
\replacewith ( prec ( a1 , a2 )| ( a1 = a2 & prec ( b1 , b2 )))
\heuristics (simplify )
};defined in: precRules.key Line: 42 Offset :4precOfSeq {
\schemaVar \term Seq s1 ;
\schemaVar \term Seq s2 ;
\schemaVar \variables int iv , jv ;
\find ( prec ( s1 , s2 ))
\varcond \replacewith ( seqLen ( s1 )= seqLen ( s2 )& \exists iv ; ( 0 <= iv & iv < seqLen ( s1 )& prec ( any :: seqGet ( s1 , iv ), any :: seqGet ( s2 , iv ))& \forall jv ; ( 0 <= jv & jv < iv -> any :: seqGet ( s1 , jv )= any :: seqGet ( s2 , jv )))| seqLen ( s1 )< seqLen ( s2 ))
};defined in: precRules.key Line: 56 Offset :4measuredByCheck {
\schemaVar \term any c , m ;
\assumes ( measuredBy ( m )==> )
\find ( measuredByCheck ( c ))
\sameUpdateLevel
\replacewith ( prec ( c , m ))
\heuristics (simplify )
};defined in: precRules.key Line: 76 Offset :4measuredByCheckEmpty {
\schemaVar \term any c ;
\assumes ( measuredByEmpty ==> )
\find ( measuredByCheck ( c ))
\sameUpdateLevel
\replacewith ( true )
\heuristics (simplify )
};defined in: precRules.key Line: 85 Offset :4