Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] valuation v_2 operator ?

Email Gateway (Aug 22 2022 at 17:01):

From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Isabelle users,

I'd like to ask if there already exists a definition/formalization of
the
valuation v_2 (2-order valuation operator) and its properties in the
library ?
i.e. of v_2 a = Max A where "A = {k∈ ℕ . 2^k dvd a } " ?
(see https://en.wikipedia.org/wiki/Singly_and_doubly_even#Definitions)

Many thanks in advance!
Angeliki

Last updated: Apr 26 2024 at 16:20 UTC