intPow.key

Taclets

No choice condition specified

powDef

powDef  {
\schemaVar   \variables int   i ;
\find (                    pow   (                   base ,                    exp ))
\varcond   \replacewith (                   \if (                   exp >=          0 )\then (                   bprod  {   i ; } (                   0 ,                    exp ,                    base ))\else (                   undefinedPow   (                   base ,                    exp )))

};

defined in: intPow.key Line: 15 Offset :4

powConcrete0

\lemma  powConcrete0  {
\find (                    pow   (                   base ,                    0 ))
  \replacewith (                    1 )
\heuristics  (simplify )

};

defined in: intPow.key Line: 27 Offset :4

powConcrete1

\lemma  powConcrete1  {
\find (                    pow   (                   base ,                    1 ))
  \replacewith (                    base )
\heuristics  (simplify )

};

defined in: intPow.key Line: 36 Offset :4

powSplitFactor

\lemma  powSplitFactor  {
\find (                    pow   (                   base ,                    exp ))
  \replacewith (                   \if (                   exp >=          0 )\then (                  \if (                   exp >=          1 )\then (                   base *        pow   (                   base ,                    exp -         1 ))\else (                   1 ))\else (                   undefinedPow   (                   base ,                    exp )))

};

defined in: intPow.key Line: 45 Offset :4

powAdd

\lemma  powAdd  {
\find (                    pow   (                   base ,                    exp +         exp_2 ))
  \replacewith (                   \if (                   exp >=          0 &             exp_2 >=          0 )\then (                   pow   (                   base ,                    exp )*        pow   (                   base ,                    exp_2 ))\else (                   pow   (                   base ,                    exp +         exp_2 )))

};

defined in: intPow.key Line: 59 Offset :4

powMono

\lemma  powMono  {
\find (                    pow   (                   base ,                    exp )<=          pow   (                   base ,                    exp_2 ))
  \add (                     exp >=          0 &             exp_2 >=          exp &             base >=          1 ->                pow   (                   base ,                    exp )<=          pow   (                   base ,                    exp_2 )==>  )

};

defined in: intPow.key Line: 69 Offset :4

powMonoConcrete

\lemma  powMonoConcrete  {
\find (                    pow   (                   base ,                    exp_2 )<=      -       1 +         pow   (                   base ,                    exp )==>  )
  \add (  ==>                     exp >=          0 &             exp_2 >=          exp &             base >=          1 )
\heuristics  (simplify )

};

defined in: intPow.key Line: 78 Offset :4

powMonoConcreteRight

\lemma  powMonoConcreteRight  {
\find ( ==>                     pow   (                   base ,                    exp )<=          pow   (                   base ,                    exp_2 ))
  \add (  ==>                     exp >=          0 &             exp_2 >=          exp &             base >=          1 )
\heuristics  (concrete )

};

defined in: intPow.key Line: 87 Offset :4

powPositive

\lemma  powPositive  {
\find (                    pow   (                   base ,                    exp ))
  \add (                     exp >=          0 &             base >=          1 ->                pow   (                   base ,                    exp )>=          1 ==>  )

};

defined in: intPow.key Line: 96 Offset :4

powPositiveConcrete

\lemma  powPositiveConcrete  {
\find (                    pow   (                   base ,                    exp )<=      -       1 ==>  )
  \add (  ==>                     exp >=          0 &             base >=          1 )
\heuristics  (simplify )

};

defined in: intPow.key Line: 105 Offset :4

powGeq1Concrete

\lemma  powGeq1Concrete  {
\find (                    pow   (                   base ,                    exp )<=          0 ==>  )
  \add (  ==>                     exp >=          0 &             base >=          1 )
\heuristics  (simplify )

};

defined in: intPow.key Line: 114 Offset :4

pow2InIntLower

\lemma  pow2InIntLower  {
\find (                    pow   (                   2 ,                    exp )<=      -       2147483649 ==>  )
  \add (  ==>                     exp >=          0 )
\heuristics  (simplify )

};

defined in: intPow.key Line: 123 Offset :4

pow2InIntUpper

\lemma  pow2InIntUpper  {
\find (                    pow   (                   2 ,                    exp )>=          2147483648 ==>  )
  \add (  ==>                     exp >=          0 &             exp <=          30 )
\heuristics  (simplify )

};

defined in: intPow.key Line: 132 Offset :4

logDefinition

logDefinition  {
\find (                    log   (                   base ,                    x ))
  \replacewith (                   \if (                   x >=          1 &             base >          1 )\then (                  \if (                   x <          base )\then (                   0 )\else (                   1 +         log   (                   base ,                    x /       base )))\else (                   undefinedLog   (                   base ,                    x )))

};

defined in: intPow.key Line: 141 Offset :4

logSelfConcrete

\lemma  logSelfConcrete  {
\find (                    log   (                   base ,                    base ))
  \replacewith (                   \if (                   base >          1 )\then (                   1 )\else (                   undefinedLog   (                   base ,                    base )))
\heuristics  (simplify )

};

defined in: intPow.key Line: 154 Offset :4

log1Concrete

\lemma  log1Concrete  {
\find (                    log   (                   base ,                    1 ))
  \replacewith (                   \if (                   base >          1 )\then (                   0 )\else (                   undefinedLog   (                   base ,                    1 )))
\heuristics  (simplify )

};

defined in: intPow.key Line: 161 Offset :4

logProduct

\lemma  logProduct  {
\find (                    log   (                   base ,                    x *        base ))
  \add (                     x >=          1 &             base >          1 ->                log   (                   base ,                    x *        base )=           log   (                   base ,                    x )+         1 ==>  )

};

defined in: intPow.key Line: 168 Offset :4

logTimesBaseConcrete

\lemma  logTimesBaseConcrete  {
\find (                    log   (                   base ,                    x *        base ))
  \replacewith (                   \if (                   x >=          1 &             base >          1 )\then (                   log   (                   base ,                    x )+         1 )\else (                   undefinedLog   (                   base ,                    x *        base )))
\heuristics  (simplify )

};

defined in: intPow.key Line: 176 Offset :4

logProdIdentity

\lemma  logProdIdentity  {
\schemaVar   \variables int   i ;
\find (                    log   (                   base ,                    bprod  {   i ; } (                   0 ,                    exp ,                    base )))
\varcond   \add (                     exp >=          0 &             base >          1 ->                log   (                   base ,                    bprod  {   i ; } (                   0 ,                    exp ,                    base ))=           exp ==>  )

};

defined in: intPow.key Line: 199 Offset :4

logProdIdentityConcrete

\lemma  logProdIdentityConcrete  {
\schemaVar   \variables int   i ;
\find (                    log   (                   base ,                    bprod  {   i ; } (                   0 ,                    exp ,                    base )))
\varcond   \replacewith (                   \if (                   base >          1 )\then (                  \if (                   exp <          0 )\then (                   0 )\else (                   exp ))\else (                   undefinedLog   (                   base ,                    bprod  {   i ; } (                   0 ,                    exp ,                    base ))))
\heuristics  (simplify )

};

defined in: intPow.key Line: 209 Offset :4

logPowIdentity

\lemma  logPowIdentity  {
\schemaVar   \variables int   i ;
\find (                    log   (                   base ,                    x ))
\varcond   \add (                     base >          1 ->      \forall    i ;            (                   i >=          0 ->                log   (                   base ,                    pow   (                   base ,                    i ))=           i )==>  )

};

defined in: intPow.key Line: 226 Offset :4

logPowIdentityConcrete

\lemma  logPowIdentityConcrete  {
\find (                    log   (                   base ,                    pow   (                   base ,                    exp )))
  \replacewith (                   \if (                   base >          1 )\then (                  \if (                   exp >=          0 )\then (                   exp )\else (                   log   (                   base ,                    undefinedPow   (                   base ,                    exp ))))\else (                   undefinedLog   (                   base ,                    pow   (                   base ,                    exp ))))
\heuristics  (simplify )

};

defined in: intPow.key Line: 236 Offset :4

logPositive

\lemma  logPositive  {
\find (                    log   (                   base ,                    x ))
  \add (                     base >          1 &             x >=          1 ->                log   (                   base ,                    x )>=          0 ==>  )

};

defined in: intPow.key Line: 251 Offset :4

logPositiveConcrete

\lemma  logPositiveConcrete  {
\find (                    log   (                   base ,                    x )<=      -       1 ==>  )
  \add (  ==>                     base >          1 &             x >=          1 )
\heuristics  (simplify )

};

defined in: intPow.key Line: 259 Offset :4

logMono

\lemma  logMono  {
\find (                    log   (                   base ,                    x )<=          log   (                   base ,                    x_2 ))
  \add (                     x >=          1 &             x_2 >=          x &             base >          1 ->                log   (                   base ,                    x )<=          log   (                   base ,                    x_2 )==>  )

};

defined in: intPow.key Line: 268 Offset :4

logMonoConcrete

\lemma  logMonoConcrete  {
\find (                    log   (                   base ,                    x_2 )<=      -       1 +         log   (                   base ,                    x )==>  )
  \add (  ==>                     x >=          1 &             x_2 >=          x &             base >          1 )
\heuristics  (simplify )

};

defined in: intPow.key Line: 277 Offset :4

powLogLess

\lemma  powLogLess  {
\find (                    pow   (                   base ,                    log   (                   base ,                    exp )))
  \add (                     exp >=          1 &             base >          1 ->                pow   (                   base ,                    log   (                   base ,                    exp ))<=          exp ==>  )

};

defined in: intPow.key Line: 286 Offset :4

powLogMore2

\lemma  powLogMore2  {
\find (                    pow   (                   base ,                    log   (                   base ,                    x )))
  \add (                     base =           2 &             x >=          1 ->                x -         pow   (                   base ,                    log   (                   base ,                    x ))<          pow   (                   base ,                    log   (                   base ,                    x ))==>  )

};

defined in: intPow.key Line: 296 Offset :4

logLessThanPow

\lemma  logLessThanPow  {
\find (                    log   (                   base ,                    x )<          exp )
  \add (                     base >          1 &             x >=          1 &             x <          pow   (                   base ,                    exp )&             exp >=          1 ->                log   (                   base ,                    x )<          exp ==>  )

};

defined in: intPow.key Line: 304 Offset :4

logLessThanPowConcrete

\lemma  logLessThanPowConcrete  {
\find ( ==>                     log   (                   base ,                    x )<          exp )
  \add (  ==>                     base >          1 &             x >=          1 &             x <          pow   (                   base ,                    exp )&             exp >=          1 )
\heuristics  (simplify )

};

defined in: intPow.key Line: 312 Offset :4

logSqueeze

\lemma  logSqueeze  {
\find (                    log   (                   base ,                    x )=           exp )
  \add (                     base >          1 &             x >=          1 &             x >=          pow   (                   base ,                    exp )&             x <          pow   (                   base ,                    exp +         1 )&             exp >=          0 ->                log   (                   base ,                    x )=           exp ==>  )

};

defined in: intPow.key Line: 321 Offset :4

KeY Logic Documentation

Defined symbols in the KeY System

Overview