Expand description
This file contains proofs related to exponentiation. These are part of the math standard library.
It’s based on the following file from the Dafny math standard library:
Source/DafnyStandardLibraries/src/Std/Arithmetic/Power.dfy.
That file has the following copyright notice:
/*******************************************************************************
- Original: Copyright (c) Microsoft Corporation
- SPDX-License-Identifier: MIT
- Modifications and Extensions: Copyright by the contributors to the Dafny Project
- SPDX-License-Identifier: MIT *******************************************************************************/
Functions§
- group_
pow_ properties - lemma0_
pow - lemma1_
pow - lemma_
pow0 - lemma_
pow1 - lemma_
pow_ adds - lemma_
pow_ distributes - lemma_
pow_ division_ inequality - lemma_
pow_ increases - lemma_
pow_ increases_ converse - lemma_
pow_ mod - lemma_
pow_ mod_ noop - lemma_
pow_ multiplies - lemma_
pow_ positive - lemma_
pow_ strictly_ increases - lemma_
pow_ strictly_ increases_ converse - lemma_
pow_ sub_ add_ cancel - lemma_
pow_ subtracts - lemma_
pull_ out_ pows - lemma_
square_ is_ pow2 - pow