Module power2

This file contains proofs related to powers of 2. 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/Power2.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

lemma2_to64

lemma2_to64_rest

lemma_pow2

lemma_pow2_adds

lemma_pow2_pos

lemma_pow2_strictly_increases

lemma_pow2_subtracts

lemma_pow2_unfold

pow2