precRules.key

Taclets

No choice condition specified

precOfInt

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 :4

precOfIntPair

precOfIntPair  {
\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 :4

precOfPairInt

precOfPairInt  {
\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 :4

precOfPair

precOfPair  {
\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 :4

precOfSeq

precOfSeq  {
\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   (                    seqGet  <[ any ]>   (                    s1 ,                    iv ) ,                    seqGet  <[ any ]>   (                    s2 ,                    iv ) ) &   \forall    jv ;            (                    0 <=          jv &             jv <          iv ->                seqGet  <[ any ]>   (                    s1 ,                    jv ) =           seqGet  <[ any ]>   (                    s2 ,                    jv ) ) ) |              seqLen   (                    s1 ) <          seqLen   (                    s2 ) ) 

};

defined in: precRules.key Line: 56 Offset :4

measuredByCheck

measuredByCheck  {
\schemaVar   \term any   c ,  m ;
\assumes (                     measuredBy   (                    m ) ==>  )
\find (                    measuredByCheck   (                    c ) )
  \replacewith (                     prec   (                    c ,                    m ) ) 
\heuristics  (simplify )

};

defined in: precRules.key Line: 76 Offset :4

KeY Logic Documentation

Defined symbols in the KeY System

Overview