Module logarithm

This file contains proofs related to integer logarithms. 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/Logarithm.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

lemma_log0

lemma_log_is_ordered

lemma_log_nonnegative

lemma_log_pow

lemma_log_s

log