Round-six κ development, definitions part 9
DefinitionIntMul_Kappa_R6_Defs9complexity-theoryinteger-multiplicationkappa-improvement
Definition bundle IntMul_Kappa_R6_Defs9 of the round-six κ-improvement development. It collects the definitions (data types, parameter maps, network and program structures, and the few lemmas that these definitions need) of the Lean modules Solutions.R6ChkPack, Solutions.R6ChkF2, Solutions.R6ChkConst, Solutions.R6ChkBitBase, Solutions.R6ChkBitDag, Solutions.R6ChkCx, extracted by skeleton subtraction from the source files with their namespaces, variable declarations and opens unchanged.
The theorems about these objects are published as separate platform nodes that import this bundle.
Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).
Definition code
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.
import Mathlib
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
section
-- Source module: Solutions.R6ChkPack
/-!
# Packed bit-vector kernels for reflective certificate checking (round six)
Kernel-friendly primitives on `ℕ` (every operation is a single GMP-accelerated kernel step:
`Nat.land`, `Nat.xor`, `Nat.mul`, `Nat.shiftLeft`, `Nat.shiftRight`, ...), with their bit-level
specifications.
* `row X i`: the `i`-th 32-bit field of `X` (a list of `F₂` vectors packed with stride 32).
* `pkf s f k = Σ_{i<k} f i · 2^{s i}`, `testBit_pkf`: bits of packed sums.
* `fold32`: five xor-shifts; bit `p` of `fold32 x` is the parity of bits `p, …, p+31` of `x`.
* `dotsP A B`: **all 24 × 24 inner products over `F₂` in 16 big-number operations**: for
`A, B < 2^768` (at most 24 rows each), bit `800 j + 32 i` of `dotsP A B` is the parity of
`row A j &&& row B i` (`dotsP_spec`).
* `tgt o k`: the target pattern with ones exactly at `(j, o + j)`, `j < k` (`testBit_tgt`).
Definitions use the `Nat.*` functions directly (not the `HAnd`/`HMul` notation) because kernel
reduction through the notation instances is about four times slower.
-/
namespace R6Chk
/-! ## Notation bridges (all `rfl`) -/
/-! ## Packed sums -/
/-- `pkf s f k = Σ_{i<k} f i · 2^{s i}`. -/
def pkf (s : ℕ) (f : ℕ → ℕ) : ℕ → ℕ
| 0 => 0
| k + 1 => pkf s f k + 2 ^ (s * k) * f k
/-! ## Rows -/
/-- The `i`-th 32-bit field of `X`. -/
def row (X i : ℕ) : ℕ := (X >>> (32 * i)) % 2 ^ 32
/-! ## Parity and the xor-shift fold -/
/-- `parB f k = f 0 xor ⋯ xor f (k-1)`. -/
def parB (f : ℕ → Bool) : ℕ → Bool
| 0 => false
| k + 1 => xor (parB f k) (f k)
/-- One xor-shift. -/
def xs (x k : ℕ) : ℕ := Nat.xor x (Nat.shiftRight x k)
/-- Five xor-shifts: windowed parity over 32 bits. -/
def fold32 (x : ℕ) : ℕ := xs (xs (xs (xs (xs x 1) 2) 4) 8) 16
/-! ## All inner products of two 24-row lists -/
/-- `Σ_{j<24} 2^{768 j}`. -/
def R1 : ℕ := pkf 768 (fun _ => 1) 24
/-- `Σ_{j<24} (2^32 - 1) 2^{800 j}`. -/
def M1 : ℕ := pkf 800 (fun _ => 2 ^ 32 - 1) 24
/-- `Σ_{i<25} 2^{32 i}`. -/
def R2 : ℕ := pkf 32 (fun _ => 1) 25
/-- `Σ_{j<24} 2^{800 j}`. -/
def R3 : ℕ := pkf 800 (fun _ => 1) 24
/-- Ones at `800 j + 32 i`, `i, j < 24`. -/
def LOW : ℕ := pkf 800 (fun _ => pkf 32 (fun _ => 1) 24) 24
/-- **All inner products**: bit `800 j + 32 i` is `⟨row A j, row B i⟩` over `F₂`. The constants
are passed as arguments so that the kernel sees literals (see `dotsP_eq`). -/
def dotsK (r1 m1 r2 r3 low A B : ℕ) : ℕ :=
Nat.land (fold32 (Nat.land (Nat.mul (Nat.land (Nat.mul A r1) m1) r2) (Nat.mul B r3))) low
/-- The specification form. -/
def dotsP (A B : ℕ) : ℕ := dotsK R1 M1 R2 R3 LOW A B
/-! ## Target patterns -/
/-- `2^{832} - 1`. -/
def C832 : ℕ := 2 ^ 832 - 1
/-- Ones at `800 j + 32 (o + j)` for `j < k`. -/
def tgt (o k : ℕ) : ℕ :=
Nat.shiftLeft (Nat.div (Nat.sub (Nat.shiftLeft 1 (Nat.mul 832 k)) 1) C832) (Nat.mul 32 o)
/-! ## Range check: fields below `2^n` -/
/-- Ones at bits `n … 31` of each of 48 fields. -/
def BADf (n : ℕ) : ℕ := pkf 32 (fun _ => (2 ^ (32 - n) - 1) * 2 ^ n) 48
end R6Chk
end
section
-- Source module: Solutions.R6ChkF2
/-!
# `F₂` linear algebra from packed certificates
Semantics: `vr n X i : Fin n → ZMod 2` is row `i` of the packed number `X` (bit `t` of the
32-bit field `i`). Certificates are lists of rows; all checks are `dotsP` products compared with
target patterns (`R6ChkPack`).
* `dot_of_dotsP`: a `dotsP` equation gives every inner product `vr A j ⬝ᵥ vr B i`.
* `indep_of_dual`: rows with a dual family (`e_j ⬝ v_i = δ`) are independent.
* `mem_iff_of_cert` (label certificate): `B` (`k` rows), `H` (`n-k` rows) with
`H Bᵀ = 0`, `H Eᵀ = I`, `D Hᵀ = 0`, `D Bᵀ = I` ⟹ `span B = ker H`, `dim = k`, nondegenerate.
* `pair_of_cert` (edge certificate): `U ⊆ V`, a dual of `U`, and an orthonormal basis `R`
of the residual (`R ⊥ U`, `R ⊆ V`, `|R| = dim V − |U|`) ⟹ `span U` nondegenerate of dim `|U|`,
and `U = V` or a norm-one `w ∈ V` orthogonal to `U` exists.
-/
namespace R6Chk
open Matrix Module
/-! ## Vectors -/
/-- `true ↦ 1`, `false ↦ 0`. -/
def b2z (b : Bool) : ZMod 2 := if b then 1 else 0
/-- Bit vector of `x` in `F₂^n`. -/
def bv (n x : ℕ) : Fin n → ZMod 2 := fun i => b2z (x.testBit i)
/-- Row `i` of a packed list, as a vector of `F₂^n`. -/
def vr (n X i : ℕ) : Fin n → ZMod 2 := bv n (row X i)
/-! ## Linear algebra over `F₂` -/
section LA
variable {n : ℕ}
/-- Span of the first `k` rows. -/
def spanF {k : ℕ} (v : Fin k → (Fin n → ZMod 2)) : Submodule (ZMod 2) (Fin n → ZMod 2) := Submodule.span (ZMod 2) (Set.range v)
/-- Nondegeneracy (standard dot product) of a subspace. -/
def NondegF (S : Submodule (ZMod 2) (Fin n → ZMod 2)) : Prop := ∀ x ∈ S, (∀ y ∈ S, x ⬝ᵥ y = 0) → x = 0
end LA
end R6Chk
end
section
-- Source module: Solutions.R6ChkConst
/-!
# Literal constants for the packed kernels
The constants of `R6ChkPack` as numeric literals (so that kernel reduction never recomputes them),
each proved equal to its definition by one kernel evaluation.
-/
namespace R6Chk
def R1L : ℕ := 0x1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001
def M1L : ℕ := 0xffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffff
def R2L : ℕ := 0x1000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001
def R3L : ℕ := 0x10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001
def LOWL : ℕ := 0x100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000000000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000000000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000000000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000000000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000000000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000000000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000000000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000000000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000000000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000000000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000000000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000000000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000000000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000000000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000000000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000000000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000000000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000000000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000000000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000000000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000000000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000000000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000000000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001000000010000000100000001
def C832L : ℕ := 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
def BAD24L : ℕ := 0xff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000ff000000
def BAD23L : ℕ := 0xff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000ff800000
/-- `dotsP` with literal constants. -/
def dotsF (A B : ℕ) : ℕ := dotsK R1L M1L R2L R3L LOWL A B
/-- `tgt` with the literal constant. -/
def tgtF (o k : ℕ) : ℕ :=
Nat.shiftLeft (Nat.div (Nat.sub (Nat.shiftLeft 1 (Nat.mul 832 k)) 1) C832L) (Nat.mul 32 o)
end R6Chk
end
section
-- Source module: Solutions.R6ChkBitBase
/-!
# Bit round six (h = 23): support trees and triple tables
* `BT`: a binary tree of numbers; `btGet t d i` follows the low `d` bits of `i` (most significant
first). Node supports (bitmasks over the 1771 triples of `Fin 23`) are stored 16 per leaf in
1792-bit fields (`R6BitDataSup*`), read by `fieldOf`.
* `TRIPL`: row `i` (32-bit field) is the bitmask of the `i`-th triple (lexicographic order);
`STARL`: field `c` (1792 bits) is `star c`, the set of triples containing `c`;
`UMT0..3`: field `b` of `UMTj` is the set of triples meeting the 6-bit chunk `b` of points
`6j, …, 6j+5` (so `um P` = triples meeting `P` is four lookups).
* Table facts are proved by one kernel evaluation each (`star_spec`, `umt_spec`).
-/
namespace R6Chk.Bit
open R6Chk
/-- Bit `i` of `x`, by kernel-accelerated operations. -/
def tb (x i : ℕ) : Bool := Nat.beq (Nat.land (Nat.shiftRight x i) 1) 1
/-- Field `i` of width `w`. -/
def fieldOf (X w i : ℕ) : ℕ := Nat.land (Nat.shiftRight X (Nat.mul w i)) (Nat.sub (Nat.shiftLeft 1 w) 1)
def TRIPL : ℕ := 0x700000006800000058000000380000006400000054000000340000004c0000002c0000001c0000006200000052000000320000004a0000002a0000001a0000004600000026000000160000000e0000006100000051000000310000004900000029000000190000004500000025000000150000000d0000004300000023000000130000000b000000070000006080000050800000308000004880000028800000188000004480000024800000148000000c8000004280000022800000128000000a800000068000004180000021800000118000000980000005800000038000006040000050400000304000004840000028400000184000004440000024400000144000000c4000004240000022400000124000000a4000000640000041400000214000001140000009400000054000000340000040c0000020c0000010c0000008c0000004c0000002c0000001c000006020000050200000302000004820000028200000182000004420000024200000142000000c2000004220000022200000122000000a2000000620000041200000212000001120000009200000052000000320000040a0000020a0000010a0000008a0000004a0000002a0000001a000004060000020600000106000000860000004600000026000000160000000e000006010000050100000301000004810000028100000181000004410000024100000141000000c1000004210000022100000121000000a10000006100000411000002110000011100000091000000510000003100000409000002090000010900000089000000490000002900000019000004050000020500000105000000850000004500000025000000150000000d000004030000020300000103000000830000004300000023000000130000000b00000007000006008000050080000300800004808000028080000180800004408000024080000140800000c0800004208000022080000120800000a08000006080000410800002108000011080000090800000508000003080000408800002088000010880000088800000488000002880000018800004048000020480000104800000848000004480000024800000148000000c800004028000020280000102800000828000004280000022800000128000000a8000000680000401800002018000010180000081800000418000002180000011800000098000000580000003800006004000050040000300400004804000028040000180400004404000024040000140400000c0400004204000022040000120400000a04000006040000410400002104000011040000090400000504000003040000408400002084000010840000088400000484000002840000018400004044000020440000104400000844000004440000024400000144000000c400004024000020240000102400000824000004240000022400000124000000a400000064000040140000201400001014000008140000041400000214000001140000009400000054000000340000400c0000200c0000100c0000080c0000040c0000020c0000010c0000008c0000004c0000002c0000001c00006002000050020000300200004802000028020000180200004402000024020000140200000c0200004202000022020000120200000a02000006020000410200002102000011020000090200000502000003020000408200002082000010820000088200000482000002820000018200004042000020420000104200000842000004420000024200000142000000c200004022000020220000102200000822000004220000022200000122000000a200000062000040120000201200001012000008120000041200000212000001120000009200000052000000320000400a0000200a0000100a0000080a0000040a0000020a0000010a0000008a0000004a0000002a0000001a00004006000020060000100600000806000004060000020600000106000000860000004600000026000000160000000e00006001000050010000300100004801000028010000180100004401000024010000140100000c0100004201000022010000120100000a01000006010000410100002101000011010000090100000501000003010000408100002081000010810000088100000481000002810000018100004041000020410000104100000841000004410000024100000141000000c100004021000020210000102100000821000004210000022100000121000000a10000006100004011000020110000101100000811000004110000021100000111000000910000005100000031000040090000200900001009000008090000040900000209000001090000008900000049000000290000001900004005000020050000100500000805000004050000020500000105000000850000004500000025000000150000000d00004003000020030000100300000803000004030000020300000103000000830000004300000023000000130000000b0000000700006000800050008000300080004800800028008000180080004400800024008000140080000c0080004200800022008000120080000a00800006008000410080002100800011008000090080000500800003008000408080002080800010808000088080000480800002808000018080004040800020408000104080000840800004408000024080000140800000c080004020800020208000102080000820800004208000022080000120800000a08000006080004010800020108000101080000810800004108000021080000110800000908000005080000030800040088000200880001008800008088000040880000208800001088000008880000048800000288000001880004004800020048000100480000804800004048000020480000104800000848000004480000024800000148000000c80004002800020028000100280000802800004028000020280000102800000828000004280000022800000128000000a80000006800040018000200180001001800008018000040180000201800001018000008180000041800000218000001180000009800000058000000380006000400050004000300040004800400028004000180040004400400024004000140040000c0040004200400022004000120040000a00400006004000410040002100400011004000090040000500400003004000408040002080400010804000088040000480400002804000018040004040400020404000104040000840400004404000024040000140400000c040004020400020204000102040000820400004204000022040000120400000a04000006040004010400020104000101040000810400004104000021040000110400000904000005040000030400040084000200840001008400008084000040840000208400001084000008840000048400000284000001840004004400020044000100440000804400004044000020440000104400000844000004440000024400000144000000c40004002400020024000100240000802400004024000020240000102400000824000004240000022400000124000000a40000006400040014000200140001001400008014000040140000201400001014000008140000041400000214000001140000009400000054000000340004000c0002000c0001000c0000800c0000400c0000200c0000100c0000080c0000040c0000020c0000010c0000008c0000004c0000002c0000001c0006000200050002000300020004800200028002000180020004400200024002000140020000c0020004200200022002000120020000a00200006002000410020002100200011002000090020000500200003002000408020002080200010802000088020000480200002802000018020004040200020402000104020000840200004402000024020000140200000c020004020200020202000102020000820200004202000022020000120200000a02000006020004010200020102000101020000810200004102000021020000110200000902000005020000030200040082000200820001008200008082000040820000208200001082000008820000048200000282000001820004004200020042000100420000804200004042000020420000104200000842000004420000024200000142000000c20004002200020022000100220000802200004022000020220000102200000822000004220000022200000122000000a20000006200040012000200120001001200008012000040120000201200001012000008120000041200000212000001120000009200000052000000320004000a0002000a0001000a0000800a0000400a0000200a0000100a0000080a0000040a0000020a0000010a0000008a0000004a0000002a0000001a0004000600020006000100060000800600004006000020060000100600000806000004060000020600000106000000860000004600000026000000160000000e0006000100050001000300010004800100028001000180010004400100024001000140010000c0010004200100022001000120010000a00100006001000410010002100100011001000090010000500100003001000408010002080100010801000088010000480100002801000018010004040100020401000104010000840100004401000024010000140100000c010004020100020201000102010000820100004201000022010000120100000a01000006010004010100020101000101010000810100004101000021010000110100000901000005010000030100040081000200810001008100008081000040810000208100001081000008810000048100000281000001810004004100020041000100410000804100004041000020410000104100000841000004410000024100000141000000c10004002100020021000100210000802100004021000020210000102100000821000004210000022100000121000000a10000006100040011000200110001001100008011000040110000201100001011000008110000041100000211000001110000009100000051000000310004000900020009000100090000800900004009000020090000100900000809000004090000020900000109000000890000004900000029000000190004000500020005000100050000800500004005000020050000100500000805000004050000020500000105000000850000004500000025000000150000000d0004000300020003000100030000800300004003000020030000100300000803000004030000020300000103000000830000004300000023000000130000000b000000070006000080050000800300008004800080028000800180008004400080024000800140008000c0008004200080022000800120008000a00080006000800410008002100080011000800090008000500080003000800408008002080080010800800088008000480080002800800018008004040080020400800104008000840080004400800024008000140080000c008004020080020200800102008000820080004200800022008000120080000a00800006008004010080020100800101008000810080004100800021008000110080000900800005008000030080040080800200808001008080008080800040808000208080001080800008808000048080000280800001808004004080020040800100408000804080004040800020408000104080000840800004408000024080000140800000c08004002080020020800100208000802080004020800020208000102080000820800004208000022080000120800000a08000006080040010800200108001001080008010800040108000201080001010800008108000041080000210800001108000009080000050800000308004000880020008800100088000800880004008800020088000100880000808800004088000020880000108800000888000004880000028800000188004000480020004800100048000800480004004800020048000100480000804800004048000020480000104800000848000004480000024800000148000000c8004000280020002800100028000800280004002800020028000100280000802800004028000020280000102800000828000004280000022800000128000000a800000068004000180020001800100018000800180004001800020018000100180000801800004018000020180000101800000818000004180000021800000118000000980000005800000038006000040050000400300004004800040028000400180004004400040024000400140004000c0004004200040022000400120004000a00040006000400410004002100040011000400090004000500040003000400408004002080040010800400088004000480040002800400018004004040040020400400104004000840040004400400024004000140040000c004004020040020200400102004000820040004200400022004000120040000a00400006004004010040020100400101004000810040004100400021004000110040000900400005004000030040040080400200804001008040008080400040804000208040001080400008804000048040000280400001804004004040020040400100404000804040004040400020404000104040000840400004404000024040000140400000c04004002040020020400100204000802040004020400020204000102040000820400004204000022040000120400000a04000006040040010400200104001001040008010400040104000201040001010400008104000041040000210400001104000009040000050400000304004000840020008400100084000800840004008400020084000100840000808400004084000020840000108400000884000004840000028400000184004000440020004400100044000800440004004400020044000100440000804400004044000020440000104400000844000004440000024400000144000000c4004000240020002400100024000800240004002400020024000100240000802400004024000020240000102400000824000004240000022400000124000000a4000000640040001400200014001000140008001400040014000200140001001400008014000040140000201400001014000008140000041400000214000001140000009400000054000000340040000c0020000c0010000c0008000c0004000c0002000c0001000c0000800c0000400c0000200c0000100c0000080c0000040c0000020c0000010c0000008c0000004c0000002c0000001c006000020050000200300002004800020028000200180002004400020024000200140002000c0002004200020022000200120002000a00020006000200410002002100020011000200090002000500020003000200408002002080020010800200088002000480020002800200018002004040020020400200104002000840020004400200024002000140020000c002004020020020200200102002000820020004200200022002000120020000a00200006002004010020020100200101002000810020004100200021002000110020000900200005002000030020040080200200802001008020008080200040802000208020001080200008802000048020000280200001802004004020020040200100402000804020004040200020402000104020000840200004402000024020000140200000c02004002020020020200100202000802020004020200020202000102020000820200004202000022020000120200000a02000006020040010200200102001001020008010200040102000201020001010200008102000041020000210200001102000009020000050200000302004000820020008200100082000800820004008200020082000100820000808200004082000020820000108200000882000004820000028200000182004000420020004200100042000800420004004200020042000100420000804200004042000020420000104200000842000004420000024200000142000000c2004000220020002200100022000800220004002200020022000100220000802200004022000020220000102200000822000004220000022200000122000000a2000000620040001200200012001000120008001200040012000200120001001200008012000040120000201200001012000008120000041200000212000001120000009200000052000000320040000a0020000a0010000a0008000a0004000a0002000a0001000a0000800a0000400a0000200a0000100a0000080a0000040a0000020a0000010a0000008a0000004a0000002a0000001a004000060020000600100006000800060004000600020006000100060000800600004006000020060000100600000806000004060000020600000106000000860000004600000026000000160000000e006000010050000100300001004800010028000100180001004400010024000100140001000c0001004200010022000100120001000a00010006000100410001002100010011000100090001000500010003000100408001002080010010800100088001000480010002800100018001004040010020400100104001000840010004400100024001000140010000c001004020010020200100102001000820010004200100022001000120010000a00100006001004010010020100100101001000810010004100100021001000110010000900100005001000030010040080100200801001008010008080100040801000208010001080100008801000048010000280100001801004004010020040100100401000804010004040100020401000104010000840100004401000024010000140100000c01004002010020020100100201000802010004020100020201000102010000820100004201000022010000120100000a01000006010040010100200101001001010008010100040101000201010001010100008101000041010000210100001101000009010000050100000301004000810020008100100081000800810004008100020081000100810000808100004081000020810000108100000881000004810000028100000181004000410020004100100041000800410004004100020041000100410000804100004041000020410000104100000841000004410000024100000141000000c1004000210020002100100021000800210004002100020021000100210000802100004021000020210000102100000821000004210000022100000121000000a10000006100400011002000110010001100080011000400110002001100010011000080110000401100002011000010110000081100000411000002110000011100000091000000510000003100400009002000090010000900080009000400090002000900010009000080090000400900002009000010090000080900000409000002090000010900000089000000490000002900000019004000050020000500100005000800050004000500020005000100050000800500004005000020050000100500000805000004050000020500000105000000850000004500000025000000150000000d004000030020000300100003000800030004000300020003000100030000800300004003000020030000100300000803000004030000020300000103000000830000004300000023000000130000000b00000007
def STARL : ℕ := 0x769a46910d22106910820691082040691082040403488410202010069108204040200801a44208101008020040069108204040200801001000d22104080804010020020010006910820404020080100100080020006910820404020080100100080020004000691082040402008010010008002000400040003488410202010040080080040010002000200010000691082040402008010010008002000400040002000080001a4420810100802004004002000800100010000800020000400006910820404020080100100080020004000400020000800010000100000000006d5525488a91085488410548841020548841020202a44208101008054884102020100401522104080804010020054884102020100400800800a91082040402008010010008005488410202010040080080040010005488410202010040080080040010002000548841020201004008008004001000200020002a4420810100802004004002000800100010000800054884102020100400800800400100020002000100004000152210408080401002002001000400080008000400010000200005488410202010040080080040010002000200010000400008000080000000005b2c93244648843244208324420810324420810101922104080804032442081010080200c91082040402008010032442081010080200400400648841020201004008008004003244208101008020040040020008003244208101008020040040020008001000324420810100802004004002000800100010001922104080804010020020010004000800080004000324420810100802004004002000800100010000800020000c91082040402008010010008002000400040002000080001000032442081010080200400400200080010001000080002000040000400000000038e388e221c4420e221040e22104080e221040808071108204040200e22104080804010038884102020100400800e2210408080401002002001c4420810100802004004002000e22104080804010020020010004000e221040808040100200200100040008000e22104080804010020020010004000800080007110820404020080100100080020004000400020000e221040808040100200200100040008000800040001000038884102020100400800800400100020002000100004000080000e221040808040100200200100040008000800040001000020000200000000007e0781e103c2101e108201e10820401e1082040400f0841020201001e10820404020080078420810100802004001e1082040402008010010003c2104080804010020020010001e10820404020080100100080020001e108204040200801001000800200040001e1082040402008010010008002000400040000f084102020100400800800400100020002000100001e108204040200801001000800200040004000200008000078420810100802004004002000800100010000800020000400001e108204040200801001000800200040004000200008000100001000000000001ff801f003e0801f041001f04102001f0410202000f8208101008001f0410202010040007c104080804010020001f0410202010040080080003e0820404020080100100080001f04102020100400800800400100001f041020201004008008004001000200001f0410202010040080080040010002000200000f820810100802004004002000800100010000800001f04102020100400800800400100020002000100004000007c104080804010020020010004000800080004000100002000001f04102020100400800800400100020002000100004000080000800000000000007fff0001f8000fc08000fc0810000fc0810100007e040808040000fc081010080200003f020404020080100000fc081010080200400400001f8102020100400800800400000fc0810100802004004002000800000fc08101008020040040020008001000000fc0810100802004004002000800100010000007e04080804010020020010004000800080004000000fc0810100802004004002000800100010000800020000003f020404020080100100080020004000400020000800010000000fc081010080200400400200080010001000080002000040000400000000000000000fffff800003f800003f80800003f8080800001fc040402000003f808080401000000fe020201004008000003f8080804010020020000007f0101008020040040020000003f80808040100200200100040000003f808080401002002001000400080000003f8080804010020020010004000800080000001fc04040200801001000800200040004000200000003f8080804010020020010004000800080004000100000000fe020201004008008004001000200020001000040000800000003f80808040100200200100040008000800040001000020000200000000000000000000007ffffff80000007f80000007f8040000003fc020100000007f804020080000001fe010080200400000007f804020080100100000000ff0080401002002001000000007f80402008010010008002000000007f804020080100100080020004000000007f8040200801001000800200040004000000003fc02010040080080040010002000200010000000007f8040200801001000800200040004000200008000000001fe010080200400400200080010001000080002000040000000007f8040200801001000800200040004000200008000100001000000000000000000000000000007ffffffff8000000007fc000000003fe008000000007fc01004000000001ff004010020000000007fc01004008008000000000ff8020080100100080000000007fc0100400800800400100000000007fc01004008008004001000200000000007fc010040080080040010002000200000000003fe00802004004002000800100010000800000000007fc010040080080040010002000200010000400000000001ff004010020020010004000800080004000100002000000000007fc0100400800800400100020002000100004000080000800000000000000000000000000000000000007ffffffffffc00000000001ff800000000003ff00200000000000ffc00801000000000003ff002004004000000000007fe004008008004000000000003ff0020040040020008000000000003ff00200400400200080010000000000003ff002004004002000800100010000000000001ff80100200200100040008000800040000000000003ff002004004002000800100010000800020000000000000ffc00801001000800200040004000200008000100000000000003ff0020040040020008001000100008000200004000040000000000000000000000000000000000000000000000003fffffffffffff80000000000000ffe00000000000003ff80080000000000000ffe00200200000000000001ffc00400400200000000000000ffe002002001000400000000000000ffe0020020010004000800000000000000ffe002002001000400080008000000000000007ff0010010008002000400040002000000000000000ffe002002001000400080008000400010000000000000003ff80080080040010002000200010000400008000000000000000ffe002002001000400080008000400010000200002000000000000000000000000000000000000000000000000000000000000007fffffffffffffffe00000000000000007ff80000000000000001ffe00100000000000000003ffc00200100000000000000001ffe001000800200000000000000001ffe0010008002000400000000000000001ffe00100080020004000400000000000000000fff0008004001000200020001000000000000000001ffe001000800200040004000200008000000000000000007ff80040020008001000100008000200004000000000000000001ffe0010008002000400040002000080001000010000000000000000000000000000000000000000000000000000000000000000000000000000001fffffffffffffffffff80000000000000000001fff00000000000000000003ffe00080000000000000000001fff000400100000000000000000001fff0004001000200000000000000000001fff00040010002000200000000000000000000fff8002000800100010000800000000000000000001fff000400100020002000100004000000000000000000007ffc0010004000800080004000100002000000000000000000001fff000400100020002000100004000080000800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffff00000000000000000000001fff80000000000000000000000fffc00080000000000000000000000fffc000800100000000000000000000000fffc00080010001000000000000000000000007ffe000400080008000400000000000000000000000fffc00080010001000080002000000000000000000000003fff0002000400040002000080001000000000000000000000000fffc000800100010000800020000400004000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffffffffffffffffffffff800000000000000000000000003fff800000000000000000000000003fff8000800000000000000000000000003fff80008000800000000000000000000000001fffc000400040002000000000000000000000000003fff80008000800040001000000000000000000000000000fffe0002000200010000400008000000000000000000000000003fff800080008000400010000200002000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffff8000000000000000000000000000007fff8000000000000000000000000000007fff80004000000000000000000000000000003fffc000200010000000000000000000000000000007fff80004000200008000000000000000000000000000001fffe0001000080002000040000000000000000000000000000007fff80004000200008000100001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc0000000000000000000000000000000003fffe000080000000000000000000000000000000007fffc0001000040000000000000000000000000000000001ffff0000400010000200000000000000000000000000000000007fffc0001000040000800008000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffc00000000000000000000000000000000000001ffff800000000000000000000000000000000000003ffff0000200000000000000000000000000000000000000ffffc000080001000000000000000000000000000000000000003ffff00002000040000400000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000003ffffffffffffffffffffffffffffffffffffffffff8000000000000000000000000000000000000000000ffffe0000000000000000000000000000000000000000003ffff800008000000000000000000000000000000000000000000ffffe0000200002000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffe000000000000000000000000000000000000000000000007ffff800000000000000000000000000000000000000000000001ffffe0000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001ffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000000000000000000000001fffff0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffff
def UMT0 : ℕ := 0x7ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0000000000000000000000000000000001ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0000000000000000000000000000000001ffffffffffffffffff80000000000000000000000000000000007fffffffffffffffffe0000f00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007ffffffffffffe0000ffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007ffffffffffffe0000000000000000000000000000000001fffffffffffff80003ffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007ffffffffffffe0000000000000000000000000000000001fffffffffffff8000380000000000000000000000000000000007ffffffffffffe0000e0000e00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc0000000000000000000000000000000003ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc0000000000000000000000000000000003ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007ffffffff00007ffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc0000000000000000000000000000000003fffffffffffffffffffffffffffffffffffffffffffffffffffffffe0000000000000000000000000000000001ffffffffc0001fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc0000000000000000000000000000000003fffffffffffffffffffffffffffffffffffffffffffffffffffffffe0000000000000000000000000000000001ffffffffc0001fffff80000000000000000000000000000000007ffffffff00007ffffe0000d00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc0000000000000000000000000000000003ffffffff80000000000000000000000000000000007ffffffff00007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc0000000000000000000000000000000003ffffffff80000000000000000000000000000000007ffffffff00007ffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007ffffffff000060000dfffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc0000000000000000000000000000000003ffffffff80000000000000000000000000000000007ffffffff000060000000000000000000000000000000001ffffffffc0001800037fffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc0000000000000000000000000000000003ffffffff80000000000000000000000000000000007ffffffff000060000000000000000000000000000000001ffffffffc00018000300000000000000000000000000000000007ffffffff000060000c0000c00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc0001fffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0000000000000000000000000000000001ffff00007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0000000000000000000000000000000001ffff00007fffffffff80000000000000000000000000000000007fffc0001fffffffffe0000b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc0001fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc0001fffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc0001ffffe0000bfffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc0001ffffe0000000000000000000000000000000001ffff00007ffff80002ffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc0001ffffe0000000000000000000000000000000001ffff00007ffff8000280000000000000000000000000000000007fffc0001ffffe0000a0000a00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc0000000000000000000000000000000003fffe0000ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc0000000000000000000000000000000003fffe0000ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc000100005ffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc0000000000000000000000000000000003fffe0000fffffffffffffffffffffffffffffffffffffffffffffffe0000000000000000000000000000000001ffff0000400017ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc0000000000000000000000000000000003fffe0000fffffffffffffffffffffffffffffffffffffffffffffffe0000000000000000000000000000000001ffff0000400017ffff80000000000000000000000000000000007fffc000100005ffffe0000900000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc0000000000000000000000000000000003fffe000080000000000000000000000000000000007fffc000100005ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc0000000000000000000000000000000003fffe000080000000000000000000000000000000007fffc000100005ffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc00010000400009fffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc0000000000000000000000000000000003fffe000080000000000000000000000000000000007fffc0001000040000000000000000000000000000000001ffff000040001000027fffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffff80000000000000000000000000000000007fffc0000000000000000000000000000000003fffe000080000000000000000000000000000000007fffc0001000040000000000000000000000000000000001ffff0000400010000200000000000000000000000000000000007fffc0001000040000800008000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff800000000000000000000000000000000000003fffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe00000000000000000000000000000000000000ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe00000000000000000000000000000000000000ffffffffffffff800000000000000000000000000000000000003fffffffffffffe00007000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff800000000000000000000000000000000000003fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff800000000000000000000000000000000000003fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff800000000000000000000000000000000000003ffffffffe00007fffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff800000000000000000000000000000000000003ffffffffe00000000000000000000000000000000000000fffffffff80001ffffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff800000000000000000000000000000000000003ffffffffe00000000000000000000000000000000000000fffffffff80001800000000000000000000000000000000000003ffffffffe0000600006000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffc00000000000000000000000000000000000001ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffc00000000000000000000000000000000000001ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff800000000000000000000000000000000000003ffff00003ffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffc00000000000000000000000000000000000001fffffffffffffffffffffffffffffffffffffffffffffffffffe00000000000000000000000000000000000000ffffc0000fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffc00000000000000000000000000000000000001fffffffffffffffffffffffffffffffffffffffffffffffffffe00000000000000000000000000000000000000ffffc0000fffff800000000000000000000000000000000000003ffff00003ffffe00005000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffc00000000000000000000000000000000000001ffff800000000000000000000000000000000000003ffff00003ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffc00000000000000000000000000000000000001ffff800000000000000000000000000000000000003ffff00003ffffffffffffffffffffffffffffffffffffffffffffffffffff800000000000000000000000000000000000003ffff0000200005fffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffc00000000000000000000000000000000000001ffff800000000000000000000000000000000000003ffff0000200000000000000000000000000000000000000ffffc0000800017fffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffc00000000000000000000000000000000000001ffff800000000000000000000000000000000000003ffff0000200000000000000000000000000000000000000ffffc000080001000000000000000000000000000000000000003ffff00002000040000400000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000003ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000003ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff8000000000000000000000000000000000000000000fffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0000000000000000000000000000000000000000003fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0000000000000000000000000000000000000000003fffffffff8000000000000000000000000000000000000000000fffffffffe0000300000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000003ffffffffffffffffffffffffffffffffffffffffff8000000000000000000000000000000000000000000fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000003ffffffffffffffffffffffffffffffffffffffffff8000000000000000000000000000000000000000000fffffffffffffffffffffffffffffffffffffffffffffffffffffffff8000000000000000000000000000000000000000000ffffe00003fffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000003ffffffffffffffffffffffffffffffffffffffffff8000000000000000000000000000000000000000000ffffe0000000000000000000000000000000000000000003ffff80000ffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000003ffffffffffffffffffffffffffffffffffffffffff8000000000000000000000000000000000000000000ffffe0000000000000000000000000000000000000000003ffff800008000000000000000000000000000000000000000000ffffe0000200002000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff800000000000000000000000000000000000000000000001ffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffe000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffe000000000000000000000000000000000000000000000007ffff800000000000000000000000000000000000000000000001ffffe0000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001ffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000000000000000000000000000000001fffff0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
def UMT1 : ℕ := 0x3ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000ffffffffffffffffffff80000000000000ffffffffffffffffffff800fc00000000000007fffffffffffffffffffc007e003f00000000000000ffffffffffffffffffff800fc007e001f800000000000003fffffffffffffffffffe003f001f8007e000fc00000000000000ffffffffffffffffffff800fc007e001f8003f0003f000000000000000000000000000000000000000000000003ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000ffffffffffffffff80000000000000ffffffffffffffff800f80000000000000ffffffffffffffff800f800f800000000000007fffffffffffffffc007c007c003e00000000000000ffffffffffffffff800f800f8007c001f000000000000003fffffffffffffffe003e003e001f0007c000f800000000000000ffffffffffffffff800f800f8007c001f0003e0003e000000000000000000000000000000000000000000000003ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000001ffffffffffffffffffffffffffffffffffffffffff80000000000000ffffffffffffc007ffff80000000000000ffffffffffffc007ffff800f400000000000007fffffffffffe003ffffc007a003d00000000000000ffffffffffffc007ffff800f4007a001e800000000000003ffffffffffff001ffffe003d001e8007a000f400000000000000ffffffffffffc007ffff800f4007a001e8003d0003d000000000000000000000000000000000000000000000003ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000001ffffffffffff80000000000000ffffffffffffc00780000000000000ffffffffffffc007800f00000000000000ffffffffffffc007800f000f000000000000007fffffffffffe003c00780078003c00000000000000ffffffffffffc007800f000f00078001e000000000000003ffffffffffff001e003c003c001e00078000f000000000000000ffffffffffffc007800f000f00078001e0003c0003c000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffffffffffffffffffffff80000000000000fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000fffffffff001ffffffff80000000000000fffffffff001ffffffff800ec00000000000007ffffffff800ffffffffc0076003b00000000000000fffffffff001ffffffff800ec0076001d800000000000003ffffffffc007fffffffe003b001d80076000ec00000000000000fffffffff001ffffffff800ec0076001d8003b0003b000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffffffffffffffffffffff80000000000000fffffffffffffffffffffffffffffffffff80000000000000fffffffff001ffff80000000000000fffffffff001ffff800e80000000000000fffffffff001ffff800e800e800000000000007ffffffff800ffffc00740074003a00000000000000fffffffff001ffff800e800e80074001d000000000000003ffffffffc007fffe003a003a001d00074000e800000000000000fffffffff001ffff800e800e80074001d0003a0003a000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffffffffffffffffffffff80000000000000fffffffff00000000000001ffffffffe003ffffffffffffffffffffffffffffff80000000000000fffffffff001c0077fff80000000000000fffffffff001c0077fff800e400000000000007ffffffff800e003bfffc0072003900000000000000fffffffff001c0077fff800e40072001c800000000000003ffffffffc007001dfffe0039001c80072000e400000000000000fffffffff001c0077fff800e40072001c8003900039000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffffffffffffffffffffff80000000000000fffffffff00000000000001ffffffffe00380000000000000fffffffff001c00700000000000000fffffffff001c007000e00000000000000fffffffff001c007000e000e000000000000007ffffffff800e003800700070003800000000000000fffffffff001c007000e000e00070001c000000000000003ffffffffc007001c00380038001c00070000e000000000000000fffffffff001c007000e000e00070001c0003800038000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffe00000000000003ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000fffffe003fffffffffff80000000000000fffffe003fffffffffff800dc00000000000007fffff001fffffffffffc006e003700000000000000fffffe003fffffffffff800dc006e001b800000000000003fffff800fffffffffffe0037001b8006e000dc00000000000000fffffe003fffffffffff800dc006e001b8003700037000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffe00000000000003ffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000fffffe003fffffff80000000000000fffffe003fffffff800d80000000000000fffffe003fffffff800d800d800000000000007fffff001fffffffc006c006c003600000000000000fffffe003fffffff800d800d8006c001b000000000000003fffff800fffffffe00360036001b0006c000d800000000000000fffffe003fffffff800d800d8006c001b0003600036000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffe00000000000003ffffffffffffffffffffffffffff00000000000001fffffc007fffffffffffffffffffffffffffffffff80000000000000fffffe003fffc006ffff80000000000000fffffe003fffc006ffff800d400000000000007fffff001fffe0037fffc006a003500000000000000fffffe003fffc006ffff800d4006a001a800000000000003fffff800ffff001bfffe0035001a8006a000d400000000000000fffffe003fffc006ffff800d4006a001a8003500035000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffe00000000000003ffffffffffffffffffffffffffff00000000000001fffffc007fff80000000000000fffffe003fffc00680000000000000fffffe003fffc006800d00000000000000fffffe003fffc006800d000d000000000000007fffff001fffe003400680068003400000000000000fffffe003fffc006800d000d00068001a000000000000003fffff800ffff001a00340034001a00068000d000000000000000fffffe003fffc006800d000d00068001a0003400034000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffe00000000000003fffff80000000000000fffffe003ffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000fffffe003001bfffffff80000000000000fffffe003001bfffffff800cc00000000000007fffff001800dfffffffc0066003300000000000000fffffe003001bfffffff800cc00660019800000000000003fffff800c006fffffffe0033001980066000cc00000000000000fffffe003001bfffffff800cc006600198003300033000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffe00000000000003fffff80000000000000fffffe003ffffffffffffffffffffffffff80000000000000fffffe003001bfff80000000000000fffffe003001bfff800c80000000000000fffffe003001bfff800c800c800000000000007fffff001800dfffc00640064003200000000000000fffffe003001bfff800c800c800640019000000000000003fffff800c006fffe00320032001900064000c800000000000000fffffe003001bfff800c800c8006400190003200032000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffe00000000000003fffff80000000000000fffffe00300000000000001fffffc0060037fffffffffffffffffffffffffffff80000000000000fffffe00300180067fff80000000000000fffffe00300180067fff800c400000000000007fffff001800c0033fffc0062003100000000000000fffffe00300180067fff800c400620018800000000000003fffff800c0060019fffe0031001880062000c400000000000000fffffe00300180067fff800c4006200188003100031000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffe00000000000003fffff80000000000000fffffe00300000000000001fffffc00600300000000000000fffffe003001800600000000000000fffffe0030018006000c00000000000000fffffe0030018006000c000c000000000000007fffff001800c003000600060003000000000000000fffffe0030018006000c000c000600018000000000000003fffff800c006001800300030001800060000c000000000000000fffffe0030018006000c000c0006000180003000030000000000000000000000000000000000000000000000003fffffffffffff80000000000000fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000ffe003ffffffffffffff80000000000000ffe003ffffffffffffff800bc00000000000007ff001ffffffffffffffc005e002f00000000000000ffe003ffffffffffffff800bc005e0017800000000000003ff800ffffffffffffffe002f00178005e000bc00000000000000ffe003ffffffffffffff800bc005e00178002f0002f000000000000000000000000000000000000000000000003fffffffffffff80000000000000fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000ffe003ffffffffff80000000000000ffe003ffffffffff800b80000000000000ffe003ffffffffff800b800b800000000000007ff001ffffffffffc005c005c002e00000000000000ffe003ffffffffff800b800b8005c0017000000000000003ff800ffffffffffe002e002e00170005c000b800000000000000ffe003ffffffffff800b800b8005c00170002e0002e000000000000000000000000000000000000000000000003fffffffffffff80000000000000fffffffffffffffffffffffffffffffffffffffffffff00000000000001ffc007ffffffffffffffffffffffffffffffffffff80000000000000ffe003ffffffc005ffff80000000000000ffe003ffffffc005ffff800b400000000000007ff001ffffffe002ffffc005a002d00000000000000ffe003ffffffc005ffff800b4005a0016800000000000003ff800fffffff0017fffe002d00168005a000b400000000000000ffe003ffffffc005ffff800b4005a00168002d0002d000000000000000000000000000000000000000000000003fffffffffffff80000000000000fffffffffffffffffffffffffffffffffffffffffffff00000000000001ffc007ffffff80000000000000ffe003ffffffc00580000000000000ffe003ffffffc005800b00000000000000ffe003ffffffc005800b000b000000000000007ff001ffffffe002c00580058002c00000000000000ffe003ffffffc005800b000b000580016000000000000003ff800fffffff0016002c002c001600058000b000000000000000ffe003ffffffc005800b000b0005800160002c0002c000000000000000000000000000000000000000000000003fffffffffffff80000000000000ffffffffffffffffffffff80000000000000ffe003fffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000ffe003fff0017fffffff80000000000000ffe003fff0017fffffff800ac00000000000007ff001fff800bfffffffc0056002b00000000000000ffe003fff0017fffffff800ac00560015800000000000003ff800fffc005fffffffe002b001580056000ac00000000000000ffe003fff0017fffffff800ac005600158002b0002b000000000000000000000000000000000000000000000003fffffffffffff80000000000000ffffffffffffffffffffff80000000000000ffe003fffffffffffffffffffffffffffff80000000000000ffe003fff0017fff80000000000000ffe003fff0017fff800a80000000000000ffe003fff0017fff800a800a800000000000007ff001fff800bfffc00540054002a00000000000000ffe003fff0017fff800a800a800540015000000000000003ff800fffc005fffe002a002a001500054000a800000000000000ffe003fff0017fff800a800a8005400150002a0002a000000000000000000000000000000000000000000000003fffffffffffff80000000000000ffffffffffffffffffffff80000000000000ffe003fff00000000000001ffc007ffe002ffffffffffffffffffffffffffffff80000000000000ffe003fff00140057fff80000000000000ffe003fff00140057fff800a400000000000007ff001fff800a002bfffc0052002900000000000000ffe003fff00140057fff800a400520014800000000000003ff800fffc0050015fffe0029001480052000a400000000000000ffe003fff00140057fff800a4005200148002900029000000000000000000000000000000000000000000000003fffffffffffff80000000000000ffffffffffffffffffffff80000000000000ffe003fff00000000000001ffc007ffe00280000000000000ffe003fff001400500000000000000ffe003fff0014005000a00000000000000ffe003fff0014005000a000a000000000000007ff001fff800a002800500050002800000000000000ffe003fff0014005000a000a000500014000000000000003ff800fffc005001400280028001400050000a000000000000000ffe003fff0014005000a000a0005000140002800028000000000000000000000000000000000000000000000003fffffffffffff80000000000000ffe00000000000003ff800fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000ffe002002fffffffffff80000000000000ffe002002fffffffffff8009c00000000000007ff0010017ffffffffffc004e002700000000000000ffe002002fffffffffff8009c004e0013800000000000003ff800800bffffffffffe002700138004e0009c00000000000000ffe002002fffffffffff8009c004e00138002700027000000000000000000000000000000000000000000000003fffffffffffff80000000000000ffe00000000000003ff800fffffffffffffffffffffffffffffffffffffffffffffffff80000000000000ffe002002fffffff80000000000000ffe002002fffffff800980000000000000ffe002002fffffff80098009800000000000007ff0010017ffffffc004c004c002600000000000000ffe002002fffffff800980098004c0013000000000000003ff800800bffffffe0026002600130004c0009800000000000000ffe002002fffffff800980098004c00130002600026000000000000000000000000000000000000000000000003fffffffffffff80000000000000ffe00000000000003ff800fffffffffffffffffffffff00000000000001ffc004005fffffffffffffffffffffffffffffffff80000000000000ffe002002fffc004ffff80000000000000ffe002002fffc004ffff8009400000000000007ff0010017ffe0027fffc004a002500000000000000ffe002002fffc004ffff80094004a0012800000000000003ff800800bfff0013fffe002500128004a0009400000000000000ffe002002fffc004ffff80094004a00128002500025000000000000000000000000000000000000000000000003fffffffffffff80000000000000ffe00000000000003ff800fffffffffffffffffffffff00000000000001ffc004005fff80000000000000ffe002002fffc00480000000000000ffe002002fffc004800900000000000000ffe002002fffc00480090009000000000000007ff0010017ffe002400480048002400000000000000ffe002002fffc00480090009000480012000000000000003ff800800bfff0012002400240012000480009000000000000000ffe002002fffc004800900090004800120002400024000000000000000000000000000000000000000000000003fffffffffffff80000000000000ffe00000000000003ff80080000000000000ffe002002ffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000ffe0020020013fffffff80000000000000ffe0020020013fffffff8008c00000000000007ff0010010009fffffffc0046002300000000000000ffe0020020013fffffff8008c00460011800000000000003ff8008008004fffffffe00230011800460008c00000000000000ffe0020020013fffffff8008c004600118002300023000000000000000000000000000000000000000000000003fffffffffffff80000000000000ffe00000000000003ff80080000000000000ffe002002ffffffffffffffffffffffffff80000000000000ffe0020020013fff80000000000000ffe0020020013fff800880000000000000ffe0020020013fff80088008800000000000007ff0010010009fffc00440044002200000000000000ffe0020020013fff80088008800440011000000000000003ff8008008004fffe002200220011000440008800000000000000ffe0020020013fff800880088004400110002200022000000000000000000000000000000000000000000000003fffffffffffff80000000000000ffe00000000000003ff80080000000000000ffe00200200000000000001ffc0040040027fffffffffffffffffffffffffffff80000000000000ffe00200200100047fff80000000000000ffe00200200100047fff8008400000000000007ff00100100080023fffc0042002100000000000000ffe00200200100047fff8008400420010800000000000003ff80080080040011fffe00210010800420008400000000000000ffe00200200100047fff80084004200108002100021000000000000000000000000000000000000000000000003fffffffffffff80000000000000ffe00000000000003ff80080000000000000ffe00200200000000000001ffc00400400200000000000000ffe002002001000400000000000000ffe0020020010004000800000000000000ffe002002001000400080008000000000000007ff0010010008002000400040002000000000000000ffe002002001000400080008000400010000000000000003ff80080080040010002000200010000400008000000000000000ffe002002001000400080008000400010000200002000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000001fffffffffffffffff80000000000000001fffffffffffffffff8007c0000000000000000fffffffffffffffffc003e001f00000000000000001fffffffffffffffff8007c003e000f800000000000000007ffffffffffffffffe001f000f8003e0007c00000000000000001fffffffffffffffff8007c003e000f8001f0001f00000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000001fffffffffffff80000000000000001fffffffffffff800780000000000000001fffffffffffff8007800780000000000000000fffffffffffffc003c003c001e00000000000000001fffffffffffff800780078003c000f000000000000000007ffffffffffffe001e001e000f0003c0007800000000000000001fffffffffffff800780078003c000f0001e0001e00000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000003fffffffffffffffffffffffffffffffffffffff80000000000000001fffffffffc003ffff80000000000000001fffffffffc003ffff800740000000000000000fffffffffe001ffffc003a001d00000000000000001fffffffffc003ffff80074003a000e800000000000000007fffffffff000ffffe001d000e8003a0007400000000000000001fffffffffc003ffff80074003a000e8001d0001d00000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000003fffffffff80000000000000001fffffffffc00380000000000000001fffffffffc003800700000000000000001fffffffffc0038007000700000000000000000fffffffffe001c00380038001c00000000000000001fffffffffc0038007000700038000e000000000000000007fffffffff000e001c001c000e000380007000000000000000001fffffffffc0038007000700038000e0001c0001c00000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffff80000000000000001ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000001ffffff000ffffffff80000000000000001ffffff000ffffffff8006c0000000000000000ffffff8007fffffffc0036001b00000000000000001ffffff000ffffffff8006c0036000d800000000000000007fffffc003fffffffe001b000d800360006c00000000000000001ffffff000ffffffff8006c0036000d8001b0001b00000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffff80000000000000001ffffffffffffffffffffffffffffffff80000000000000001ffffff000ffff80000000000000001ffffff000ffff800680000000000000001ffffff000ffff8006800680000000000000000ffffff8007fffc00340034001a00000000000000001ffffff000ffff8006800680034000d000000000000000007fffffc003fffe001a001a000d000340006800000000000000001ffffff000ffff8006800680034000d0001a0001a00000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffff80000000000000001ffffff00000000000000003fffffe001ffffffffffffffffffffffffffffff80000000000000001ffffff000c0037fff80000000000000001ffffff000c0037fff800640000000000000000ffffff8006001bfffc0032001900000000000000001ffffff000c0037fff800640032000c800000000000000007fffffc003000dfffe0019000c800320006400000000000000001ffffff000c0037fff800640032000c800190001900000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffffffffff80000000000000001ffffff00000000000000003fffffe00180000000000000001ffffff000c00300000000000000001ffffff000c003000600000000000000001ffffff000c0030006000600000000000000000ffffff8006001800300030001800000000000000001ffffff000c0030006000600030000c000000000000000007fffffc003000c00180018000c000300006000000000000000001ffffff000c0030006000600030000c000180001800000000000000000000000000000000000000000000000000000000000007fffffffffffffffe00000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000001ffe001fffffffffff80000000000000001ffe001fffffffffff8005c0000000000000000fff000fffffffffffc002e001700000000000000001ffe001fffffffffff8005c002e000b800000000000000007ff8007ffffffffffe0017000b8002e0005c00000000000000001ffe001fffffffffff8005c002e000b800170001700000000000000000000000000000000000000000000000000000000000007fffffffffffffffe00000000000000007fffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000001ffe001fffffff80000000000000001ffe001fffffff800580000000000000001ffe001fffffff8005800580000000000000000fff000fffffffc002c002c001600000000000000001ffe001fffffff800580058002c000b000000000000000007ff8007ffffffe00160016000b0002c0005800000000000000001ffe001fffffff800580058002c000b000160001600000000000000000000000000000000000000000000000000000000000007fffffffffffffffe00000000000000007fffffffffffffffffffffffff00000000000000003ffc003fffffffffffffffffffffffffffffffff80000000000000001ffe001fffc002ffff80000000000000001ffe001fffc002ffff800540000000000000000fff000fffe0017fffc002a001500000000000000001ffe001fffc002ffff80054002a000a800000000000000007ff8007fff000bfffe0015000a8002a0005400000000000000001ffe001fffc002ffff80054002a000a800150001500000000000000000000000000000000000000000000000000000000000007fffffffffffffffe00000000000000007fffffffffffffffffffffffff00000000000000003ffc003fff80000000000000001ffe001fffc00280000000000000001ffe001fffc002800500000000000000001ffe001fffc0028005000500000000000000000fff000fffe001400280028001400000000000000001ffe001fffc0028005000500028000a000000000000000007ff8007fff000a00140014000a000280005000000000000000001ffe001fffc0028005000500028000a000140001400000000000000000000000000000000000000000000000000000000000007fffffffffffffffe00000000000000007ff80000000000000001ffe001ffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000001ffe001000bfffffff80000000000000001ffe001000bfffffff8004c0000000000000000fff0008005fffffffc0026001300000000000000001ffe001000bfffffff8004c00260009800000000000000007ff8004002fffffffe00130009800260004c00000000000000001ffe001000bfffffff8004c00260009800130001300000000000000000000000000000000000000000000000000000000000007fffffffffffffffe00000000000000007ff80000000000000001ffe001ffffffffffffffffffffffffff80000000000000001ffe001000bfff80000000000000001ffe001000bfff800480000000000000001ffe001000bfff8004800480000000000000000fff0008005fffc00240024001200000000000000001ffe001000bfff80048004800240009000000000000000007ff8004002fffe001200120009000240004800000000000000001ffe001000bfff80048004800240009000120001200000000000000000000000000000000000000000000000000000000000007fffffffffffffffe00000000000000007ff80000000000000001ffe00100000000000000003ffc0020017fffffffffffffffffffffffffffff80000000000000001ffe00100080027fff80000000000000001ffe00100080027fff800440000000000000000fff00080040013fffc0022001100000000000000001ffe00100080027fff8004400220008800000000000000007ff80040020009fffe00110008800220004400000000000000001ffe00100080027fff8004400220008800110001100000000000000000000000000000000000000000000000000000000000007fffffffffffffffe00000000000000007ff80000000000000001ffe00100000000000000003ffc00200100000000000000001ffe001000800200000000000000001ffe0010008002000400000000000000001ffe00100080020004000400000000000000000fff0008004001000200020001000000000000000001ffe001000800200040004000200008000000000000000007ff80040020008001000100008000200004000000000000000001ffe0010008002000400040002000080001000010000000000000000000000000000000000000000000000000000000000000000000000000000001ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000001ffffffffffffff80000000000000000001ffffffffffffff8003c0000000000000000000ffffffffffffffc001e000f00000000000000000001ffffffffffffff8003c001e0007800000000000000000007fffffffffffffe000f00078001e0003c00000000000000000001ffffffffffffff8003c001e00078000f0000f000000000000000000000000000000000000000000000000000000000000000000000000000001ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000001ffffffffff80000000000000000001ffffffffff800380000000000000000001ffffffffff8003800380000000000000000000ffffffffffc001c001c000e00000000000000000001ffffffffff800380038001c0007000000000000000000007fffffffffe000e000e00070001c0003800000000000000000001ffffffffff800380038001c00070000e0000e000000000000000000000000000000000000000000000000000000000000000000000000000001ffffffffffffffffffffffffffffffffffffffffff00000000000000000003ffffffffffffffffffffffffffffffffffff80000000000000000001ffffffc001ffff80000000000000000001ffffffc001ffff800340000000000000000000ffffffe000ffffc001a000d00000000000000000001ffffffc001ffff80034001a0006800000000000000000007ffffff0007fffe000d00068001a0003400000000000000000001ffffffc001ffff80034001a00068000d0000d000000000000000000000000000000000000000000000000000000000000000000000000000001ffffffffffffffffffffffffffffffffffffffffff00000000000000000003ffffff80000000000000000001ffffffc00180000000000000000001ffffffc001800300000000000000000001ffffffc0018003000300000000000000000000ffffffe000c00180018000c00000000000000000001ffffffc00180030003000180006000000000000000000007ffffff0006000c000c0006000180003000000000000000000001ffffffc001800300030001800060000c0000c000000000000000000000000000000000000000000000000000000000000000000000000000001fffffffffffffffffff80000000000000000001fffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000001fff0007fffffff80000000000000000001fff0007fffffff8002c0000000000000000000fff8003fffffffc0016000b00000000000000000001fff0007fffffff8002c00160005800000000000000000007ffc001fffffffe000b0005800160002c00000000000000000001fff0007fffffff8002c001600058000b0000b000000000000000000000000000000000000000000000000000000000000000000000000000001fffffffffffffffffff80000000000000000001fffffffffffffffffffffffffffff80000000000000000001fff0007fff80000000000000000001fff0007fff800280000000000000000001fff0007fff8002800280000000000000000000fff8003fffc00140014000a00000000000000000001fff0007fff80028002800140005000000000000000000007ffc001fffe000a000a0005000140002800000000000000000001fff0007fff800280028001400050000a0000a000000000000000000000000000000000000000000000000000000000000000000000000000001fffffffffffffffffff80000000000000000001fff00000000000000000003ffe000ffffffffffffffffffffffffffffff80000000000000000001fff00040017fff80000000000000000001fff00040017fff800240000000000000000000fff8002000bfffc0012000900000000000000000001fff00040017fff8002400120004800000000000000000007ffc0010005fffe00090004800120002400000000000000000001fff00040017fff80024001200048000900009000000000000000000000000000000000000000000000000000000000000000000000000000001fffffffffffffffffff80000000000000000001fff00000000000000000003ffe00080000000000000000001fff000400100000000000000000001fff0004001000200000000000000000001fff00040010002000200000000000000000000fff8002000800100010000800000000000000000001fff000400100020002000100004000000000000000000007ffc0010004000800080004000100002000000000000000000001fff000400100020002000100004000080000800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000fffffffffff80000000000000000000000fffffffffff8001c00000000000000000000007ffffffffffc000e000700000000000000000000000fffffffffff8001c000e0003800000000000000000000003ffffffffffe000700038000e0001c00000000000000000000000fffffffffff8001c000e0003800070000700000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffffffffffffffffffffffffffffff80000000000000000000000fffffff80000000000000000000000fffffff800180000000000000000000000fffffff80018001800000000000000000000007ffffffc000c000c000600000000000000000000000fffffff800180018000c0003000000000000000000000003ffffffe0006000600030000c0001800000000000000000000000fffffff800180018000c0003000060000600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffff00000000000000000000001fffffffffffffffffffffffffffffffff80000000000000000000000fffc000ffff80000000000000000000000fffc000ffff8001400000000000000000000007ffe0007fffc000a000500000000000000000000000fffc000ffff80014000a0002800000000000000000000003fff0003fffe000500028000a0001400000000000000000000000fffc000ffff80014000a0002800050000500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007ffffffffffffffffffffff00000000000000000000001fff80000000000000000000000fffc00080000000000000000000000fffc000800100000000000000000000000fffc00080010001000000000000000000000007ffe000400080008000400000000000000000000000fffc00080010001000080002000000000000000000000003fff0002000400040002000080001000000000000000000000000fffc000800100010000800020000400004000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffffffffffffffffffffffffffffffffffffffffffffffffffff800000000000000000000000003fffffff800000000000000000000000003fffffff8000c00000000000000000000000001fffffffc00060003000000000000000000000000003fffffff8000c00060001800000000000000000000000000fffffffe00030001800060000c000000000000000000000000003fffffff8000c000600018000300003000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ffffffffffffffffffffffffff800000000000000000000000003fff800000000000000000000000003fff8000800000000000000000000000003fff80008000800000000000000000000000001fffc000400040002000000000000000000000000003fff80008000800040001000000000000000000000000000fffe0002000200010000400008000000000000000000000000003fff800080008000400010000200002000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffffffffffffffffffff8000000000000000000000000000007fff8000000000000000000000000000007fff80004000000000000000000000000000003fffc000200010000000000000000000000000000007fff80004000200008000000000000000000000000000001fffe0001000080002000040000000000000000000000000000007fff8000400020000800010000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
def UMT2 : ℕ := 0x1ffffffffffffffffffffffffffffffffffffffc00fffffffffff801fffffffffff07e007ffffffffffc1f83f001fffffffffff07e0fc0fc003ffffffffffe0fc1f81f80fc001fffffffffff07e0fc0fc07e01f8001fffffffffff07e0fc0fc07e01f803f0001fffffffffff07e0fc0fc07e01f803f003f0000fffffffffff83f07e07e03f00fc01f801f800fc0001fffffffffff07e0fc0fc07e01f803f003f001f8007e00007ffffffffffc1f83f03f01f807e00fc00fc007e001f8003f00001fffffffffff07e0fc0fc07e01f803f003f001f8007e000fc000fc0000000001fffffffffffffffffffffffffff801ffffffffc00ffffffffe0f801ffffffffc1f07c007ffffffff07c1f03e001ffffffffc1f07c0f80f8003ffffffff83e0f81f01f00f8001ffffffffc1f07c0f80f807c01f0001ffffffffc1f07c0f80f807c01f003e0001ffffffffc1f07c0f80f807c01f003e003e0000ffffffffe0f83e07c07c03e00f801f001f000f80001ffffffffc1f07c0f80f807c01f003e003e001f0007c00007ffffffff07c1f03e03e01f007c00f800f8007c001f0003e00001ffffffffc1f07c0f80f807c01f003e003e001f0007c000f8000f80000000001ffffffffffffffffff801fffffffffffffffffc00ffffffc1fff801ffffff83fff07a007fffffe0fffc1e83d001ffffff83fff07a0f40f4003ffffff07ffe0f41e81e80f4001ffffff83fff07a0f40f407a01e8001ffffff83fff07a0f40f407a01e803d0001ffffff83fff07a0f40f407a01e803d003d0000ffffffc1fff83d07a07a03d00f401e801e800f40001ffffff83fff07a0f40f407a01e803d003d001e8007a00007fffffe0fffc1e83d03d01e807a00f400f4007a001e8003d00001ffffff83fff07a0f40f407a01e803d003d001e8007a000f4000f40000000001ffffffffffffffffff801ffffff801ffffff83c00ffffffc1e0f001ffffff83c1e078007fffffe0f0781e03c001ffffff83c1e0780f00f0003ffffff0783c0f01e01e00f0001ffffff83c1e0780f00f007801e0001ffffff83c1e0780f00f007801e003c0001ffffff83c1e0780f00f007801e003c003c0000ffffffc1e0f03c07807803c00f001e001e000f00001ffffff83c1e0780f00f007801e003c003c001e0007800007fffffe0f0781e03c03c01e007800f000f00078001e0003c00001ffffff83c1e0780f00f007801e003c003c001e00078000f0000f00000000001fffffffffff801ffffffffffffffffffffffffc00ffffc1fffff801ffff83fffff076007fffe0fffffc1d83b001ffff83fffff0760ec0ec003ffff07ffffe0ec1d81d80ec001ffff83fffff0760ec0ec07601d8001ffff83fffff0760ec0ec07601d803b0001ffff83fffff0760ec0ec07601d803b003b0000ffffc1fffff83b07607603b00ec01d801d800ec0001ffff83fffff0760ec0ec07601d803b003b001d8007600007fffe0fffffc1d83b03b01d807600ec00ec0076001d8003b00001ffff83fffff0760ec0ec07601d803b003b001d80076000ec000ec0000000001fffffffffff801fffffffffffff801ffff83ffc00ffffc1ffe0e801ffff83ffc1d074007fffe0fff0741d03a001ffff83ffc1d0740e80e8003ffff07ff83a0e81d01d00e8001ffff83ffc1d0740e80e807401d0001ffff83ffc1d0740e80e807401d003a0001ffff83ffc1d0740e80e807401d003a003a0000ffffc1ffe0e83a07407403a00e801d001d000e80001ffff83ffc1d0740e80e807401d003a003a001d0007400007fffe0fff0741d03a03a01d007400e800e80074001d0003a00001ffff83ffc1d0740e80e807401d003a003a001d00074000e8000e80000000001fffffffffff801ffff801ffff83fffffffffffc00ffffc1c1dff801ffff8383bff072007fffe0e0effc1c839001ffff8383bff0720e40e4003ffff07077fe0e41c81c80e4001ffff8383bff0720e40e407201c8001ffff8383bff0720e40e407201c80390001ffff8383bff0720e40e407201c803900390000ffffc1c1dff83907207203900e401c801c800e40001ffff8383bff0720e40e407201c80390039001c8007200007fffe0e0effc1c83903901c807200e400e40072001c8003900001ffff8383bff0720e40e407201c80390039001c80072000e4000e40000000001fffffffffff801ffff801ffff83801ffff8383800ffffc1c1c0e001ffff838381c070007fffe0e0e0701c038001ffff838381c0700e00e0003ffff07070380e01c01c00e0001ffff838381c0700e00e007001c0001ffff838381c0700e00e007001c00380001ffff838381c0700e00e007001c003800380000ffffc1c1c0e03807007003800e001c001c000e00001ffff838381c0700e00e007001c00380038001c0007000007fffe0e0e0701c03803801c007000e000e00070001c0003800001ffff838381c0700e00e007001c00380038001c00070000e0000e00000000001ffffff003fffffffffffffffffffffffffffffc00ffe0fffffff801ffc1fffffff06e007ff07ffffffc1b837001ffc1fffffff06e0dc0dc003ff83ffffffe0dc1b81b80dc001ffc1fffffff06e0dc0dc06e01b8001ffc1fffffff06e0dc0dc06e01b80370001ffc1fffffff06e0dc0dc06e01b803700370000ffe0fffffff83706e06e03700dc01b801b800dc0001ffc1fffffff06e0dc0dc06e01b80370037001b8006e00007ff07ffffffc1b83703701b806e00dc00dc006e001b8003700001ffc1fffffff06e0dc0dc06e01b80370037001b8006e000dc000dc0000000001ffffff003ffffffffffffffffff801ffc1ffffc00ffe0ffffe0d801ffc1ffffc1b06c007ff07ffff06c1b036001ffc1ffffc1b06c0d80d8003ff83ffff8360d81b01b00d8001ffc1ffffc1b06c0d80d806c01b0001ffc1ffffc1b06c0d80d806c01b00360001ffc1ffffc1b06c0d80d806c01b003600360000ffe0ffffe0d83606c06c03600d801b001b000d80001ffc1ffffc1b06c0d80d806c01b00360036001b0006c00007ff07ffff06c1b03603601b006c00d800d8006c001b0003600001ffc1ffffc1b06c0d80d806c01b00360036001b0006c000d8000d80000000001ffffff003fffffffff801ffc1fffffffffffffc00ffe0ffc1bff801ffc1ff837ff06a007ff07fe0dffc1a835001ffc1ff837ff06a0d40d4003ff83ff06ffe0d41a81a80d4001ffc1ff837ff06a0d40d406a01a8001ffc1ff837ff06a0d40d406a01a80350001ffc1ff837ff06a0d40d406a01a803500350000ffe0ffc1bff83506a06a03500d401a801a800d40001ffc1ff837ff06a0d40d406a01a80350035001a8006a00007ff07fe0dffc1a83503501a806a00d400d4006a001a8003500001ffc1ff837ff06a0d40d406a01a80350035001a8006a000d4000d40000000001ffffff003fffffffff801ffc1ff801ffc1ff83400ffe0ffc1a0d001ffc1ff8341a068007ff07fe0d0681a034001ffc1ff8341a0680d00d0003ff83ff068340d01a01a00d0001ffc1ff8341a0680d00d006801a0001ffc1ff8341a0680d00d006801a00340001ffc1ff8341a0680d00d006801a003400340000ffe0ffc1a0d03406806803400d001a001a000d00001ffc1ff8341a0680d00d006801a00340034001a0006800007ff07fe0d0681a03403401a006800d000d00068001a0003400001ffc1ff8341a0680d00d006801a00340034001a00068000d0000d00000000001ffffff003ff801ffc1ffffffffffffffffffffc00ffe0c1bffff801ffc1837ffff066007ff060dffffc19833001ffc1837ffff0660cc0cc003ff8306ffffe0cc1981980cc001ffc1837ffff0660cc0cc0660198001ffc1837ffff0660cc0cc06601980330001ffc1837ffff0660cc0cc066019803300330000ffe0c1bffff83306606603300cc0198019800cc0001ffc1837ffff0660cc0cc0660198033003300198006600007ff060dffffc19833033019806600cc00cc006600198003300001ffc1837ffff0660cc0cc06601980330033001980066000cc000cc0000000001ffffff003ff801ffc1fffffffff801ffc1837fc00ffe0c1bfe0c801ffc1837fc19064007ff060dff06419032001ffc1837fc190640c80c8003ff8306ff8320c81901900c8001ffc1837fc190640c80c80640190001ffc1837fc190640c80c806401900320001ffc1837fc190640c80c8064019003200320000ffe0c1bfe0c83206406403200c80190019000c80001ffc1837fc190640c80c80640190032003200190006400007ff060dff06419032032019006400c800c8006400190003200001ffc1837fc190640c80c806401900320032001900064000c8000c80000000001ffffff003ff801ffc1801ffc1837ffffffffffc00ffe0c1819ff801ffc183033ff062007ff060c0cffc18831001ffc183033ff0620c40c4003ff8306067fe0c41881880c4001ffc183033ff0620c40c40620188001ffc183033ff0620c40c406201880310001ffc183033ff0620c40c4062018803100310000ffe0c1819ff83106206203100c40188018800c40001ffc183033ff0620c40c40620188031003100188006200007ff060c0cffc18831031018806200c400c4006200188003100001ffc183033ff0620c40c406201880310031001880062000c4000c40000000001ffffff003ff801ffc1801ffc183001ffc18303000ffe0c18180c001ffc18303018060007ff060c0c06018030001ffc183030180600c00c0003ff8306060300c01801800c0001ffc183030180600c00c00600180001ffc183030180600c00c006001800300001ffc183030180600c00c0060018003000300000ffe0c18180c03006006003000c00180018000c00001ffc183030180600c00c00600180030003000180006000007ff060c0c06018030030018006000c000c0006000180003000001ffc183030180600c00c006001800300030001800060000c0000c00000000001ff801fffffffffffffffffffffffffffffffffc00f83ffffffff801f07ffffffff05e007c1ffffffffc1782f001f07ffffffff05e0bc0bc003e0ffffffffe0bc1781780bc001f07ffffffff05e0bc0bc05e0178001f07ffffffff05e0bc0bc05e017802f0001f07ffffffff05e0bc0bc05e017802f002f0000f83ffffffff82f05e05e02f00bc0178017800bc0001f07ffffffff05e0bc0bc05e017802f002f00178005e00007c1ffffffffc1782f02f017805e00bc00bc005e00178002f00001f07ffffffff05e0bc0bc05e017802f002f00178005e000bc000bc0000000001ff801ffffffffffffffffffffff801f07fffffc00f83fffffe0b801f07fffffc1705c007c1ffffff05c1702e001f07fffffc1705c0b80b8003e0ffffff82e0b81701700b8001f07fffffc1705c0b80b805c0170001f07fffffc1705c0b80b805c017002e0001f07fffffc1705c0b80b805c017002e002e0000f83fffffe0b82e05c05c02e00b80170017000b80001f07fffffc1705c0b80b805c017002e002e00170005c00007c1ffffff05c1702e02e017005c00b800b8005c00170002e00001f07fffffc1705c0b80b805c017002e002e00170005c000b8000b80000000001ff801fffffffffffff801f07ffffffffffffffc00f83fffc17ff801f07fff82fff05a007c1fffe0bffc1682d001f07fff82fff05a0b40b4003e0ffff05ffe0b41681680b4001f07fff82fff05a0b40b405a0168001f07fff82fff05a0b40b405a016802d0001f07fff82fff05a0b40b405a016802d002d0000f83fffc17ff82d05a05a02d00b40168016800b40001f07fff82fff05a0b40b405a016802d002d00168005a00007c1fffe0bffc1682d02d016805a00b400b4005a00168002d00001f07fff82fff05a0b40b405a016802d002d00168005a000b4000b40000000001ff801fffffffffffff801f07fff801f07fff82c00f83fffc160b001f07fff82c16058007c1fffe0b0581602c001f07fff82c160580b00b0003e0ffff0582c0b01601600b0001f07fff82c160580b00b00580160001f07fff82c160580b00b0058016002c0001f07fff82c160580b00b0058016002c002c0000f83fffc160b02c05805802c00b00160016000b00001f07fff82c160580b00b0058016002c002c00160005800007c1fffe0b0581602c02c016005800b000b0005800160002c00001f07fff82c160580b00b0058016002c002c001600058000b0000b00000000001ff801ffffff801f07fffffffffffffffffffffc00f83fc17ffff801f07f82fffff056007c1fe0bffffc1582b001f07f82fffff0560ac0ac003e0ff05ffffe0ac1581580ac001f07f82fffff0560ac0ac0560158001f07f82fffff0560ac0ac056015802b0001f07f82fffff0560ac0ac056015802b002b0000f83fc17ffff82b05605602b00ac0158015800ac0001f07f82fffff0560ac0ac056015802b002b00158005600007c1fe0bffffc1582b02b015805600ac00ac005600158002b00001f07f82fffff0560ac0ac056015802b002b001580056000ac000ac0000000001ff801ffffff801f07ffffffffff801f07f82ffc00f83fc17fe0a801f07f82ffc15054007c1fe0bff0541502a001f07f82ffc150540a80a8003e0ff05ff82a0a81501500a8001f07f82ffc150540a80a80540150001f07f82ffc150540a80a8054015002a0001f07f82ffc150540a80a8054015002a002a0000f83fc17fe0a82a05405402a00a80150015000a80001f07f82ffc150540a80a8054015002a002a00150005400007c1fe0bff0541502a02a015005400a800a8005400150002a00001f07f82ffc150540a80a8054015002a002a001500054000a8000a80000000001ff801ffffff801f07f801f07f82fffffffffffc00f83fc1415ff801f07f8282bff052007c1fe0a0affc14829001f07f8282bff0520a40a4003e0ff05057fe0a41481480a4001f07f8282bff0520a40a40520148001f07f8282bff0520a40a405201480290001f07f8282bff0520a40a4052014802900290000f83fc1415ff82905205202900a40148014800a40001f07f8282bff0520a40a40520148029002900148005200007c1fe0a0affc14829029014805200a400a4005200148002900001f07f8282bff0520a40a405201480290029001480052000a4000a40000000001ff801ffffff801f07f801f07f82801f07f8282800f83fc14140a001f07f8282814050007c1fe0a0a05014028001f07f82828140500a00a0003e0ff05050280a01401400a0001f07f82828140500a00a00500140001f07f82828140500a00a005001400280001f07f82828140500a00a0050014002800280000f83fc14140a02805005002800a00140014000a00001f07f82828140500a00a00500140028002800140005000007c1fe0a0a05014028028014005000a000a0005000140002800001f07f82828140500a00a005001400280028001400050000a0000a00000000001ff801f003e0fffffffffffffffffffffffffffc00f820bffffff801f0417ffffff04e007c105ffffffc13827001f0417ffffff04e09c09c003e082ffffffe09c13813809c001f0417ffffff04e09c09c04e0138001f0417ffffff04e09c09c04e01380270001f0417ffffff04e09c09c04e013802700270000f820bffffff82704e04e027009c01380138009c0001f0417ffffff04e09c09c04e0138027002700138004e00007c105ffffffc13827027013804e009c009c004e00138002700001f0417ffffff04e09c09c04e0138027002700138004e0009c0009c0000000001ff801f003e0ffffffffffffffff801f0417fffc00f820bfffe09801f0417fffc1304c007c105ffff04c13026001f0417fffc1304c098098003e082ffff826098130130098001f0417fffc1304c09809804c0130001f0417fffc1304c09809804c01300260001f0417fffc1304c09809804c013002600260000f820bfffe0982604c04c02600980130013000980001f0417fffc1304c09809804c0130026002600130004c00007c105ffff04c13026026013004c00980098004c00130002600001f0417fffc1304c09809804c0130026002600130004c00098000980000000001ff801f003e0fffffff801f0417ffffffffffffc00f820bfc13ff801f0417f827ff04a007c105fe09ffc12825001f0417f827ff04a094094003e082ff04ffe094128128094001f0417f827ff04a09409404a0128001f0417f827ff04a09409404a01280250001f0417f827ff04a09409404a012802500250000f820bfc13ff82504a04a02500940128012800940001f0417f827ff04a09409404a0128025002500128004a00007c105fe09ffc12825025012804a00940094004a00128002500001f0417f827ff04a09409404a0128025002500128004a00094000940000000001ff801f003e0fffffff801f0417f801f0417f82400f820bfc1209001f0417f82412048007c105fe0904812024001f0417f82412048090090003e082ff04824090120120090001f0417f824120480900900480120001f0417f8241204809009004801200240001f0417f82412048090090048012002400240000f820bfc120902404804802400900120012000900001f0417f824120480900900480120024002400120004800007c105fe0904812024024012004800900090004800120002400001f0417f824120480900900480120024002400120004800090000900000000001ff801f003e0801f0417fffffffffffffffffffc00f820813ffff801f041027ffff046007c10409ffffc11823001f041027ffff04608c08c003e08204ffffe08c11811808c001f041027ffff04608c08c0460118001f041027ffff04608c08c04601180230001f041027ffff04608c08c046011802300230000f820813ffff823046046023008c01180118008c0001f041027ffff04608c08c0460118023002300118004600007c10409ffffc118230230118046008c008c004600118002300001f041027ffff04608c08c046011802300230011800460008c0008c0000000001ff801f003e0801f0417ffffffff801f041027fc00f820813fe08801f041027fc11044007c10409ff04411022001f041027fc11044088088003e08204ff822088110110088001f041027fc110440880880440110001f041027fc1104408808804401100220001f041027fc11044088088044011002200220000f820813fe0882204404402200880110011000880001f041027fc110440880880440110022002200110004400007c10409ff04411022022011004400880088004400110002200001f041027fc110440880880440110022002200110004400088000880000000001ff801f003e0801f041001f041027ffffffffffc00f82081011ff801f04102023ff042007c1040808ffc10821001f04102023ff042084084003e08204047fe084108108084001f04102023ff0420840840420108001f04102023ff04208408404201080210001f04102023ff042084084042010802100210000f82081011ff82104204202100840108010800840001f04102023ff0420840840420108021002100108004200007c1040808ffc10821021010804200840084004200108002100001f04102023ff0420840840420108021002100108004200084000840000000001ff801f003e0801f041001f04102001f0410202000f8208101008001f0410202010040007c104080804010020001f0410202010040080080003e0820404020080100100080001f04102020100400800800400100001f041020201004008008004001000200001f0410202010040080080040010002000200000f820810100802004004002000800100010000800001f04102020100400800800400100020002000100004000007c104080804010020020010004000800080004000100002000001f04102020100400800800400100020002000100004000080000800000000000007fffffffffffffffffffffffffffffffffffc0007fffffffff8000ffffffffff03e0003fffffffffc0f81f0000ffffffffff03e07c07c0001fffffffffe07c0f80f807c0000ffffffffff03e07c07c03e00f80000ffffffffff03e07c07c03e00f801f00000ffffffffff03e07c07c03e00f801f001f000007fffffffff81f03e03e01f007c00f800f8007c00000ffffffffff03e07c07c03e00f801f001f000f8003e000003fffffffffc0f81f01f00f803e007c007c003e000f8001f000000ffffffffff03e07c07c03e00f801f001f000f8003e0007c0007c0000000000007ffffffffffffffffffffffff8000fffffffc0007ffffffe078000fffffffc0f03c0003fffffff03c0f01e0000fffffffc0f03c0780780001fffffff81e0780f00f00780000fffffffc0f03c07807803c00f00000fffffffc0f03c07807803c00f001e00000fffffffc0f03c07807803c00f001e001e000007ffffffe0781e03c03c01e007800f000f0007800000fffffffc0f03c07807803c00f001e001e000f0003c000003fffffff03c0f01e01e00f003c00780078003c000f0001e000000fffffffc0f03c07807803c00f001e001e000f0003c00078000780000000000007fffffffffffffff8000ffffffffffffffffc0007ffffc0fff8000fffff81fff03a0003ffffe07ffc0e81d0000fffff81fff03a0740740001fffff03ffe0740e80e80740000fffff81fff03a07407403a00e80000fffff81fff03a07407403a00e801d00000fffff81fff03a07407403a00e801d001d000007ffffc0fff81d03a03a01d007400e800e8007400000fffff81fff03a07407403a00e801d001d000e8003a000003ffffe07ffc0e81d01d00e803a00740074003a000e8001d000000fffff81fff03a07407403a00e801d001d000e8003a00074000740000000000007fffffffffffffff8000fffff8000fffff81c0007ffffc0e070000fffff81c0e0380003ffffe070380e01c0000fffff81c0e0380700700001fffff0381c0700e00e00700000fffff81c0e03807007003800e00000fffff81c0e03807007003800e001c00000fffff81c0e03807007003800e001c001c000007ffffc0e0701c03803801c007000e000e0007000000fffff81c0e03807007003800e001c001c000e00038000003ffffe070380e01c01c00e0038007000700038000e0001c000000fffff81c0e03807007003800e001c001c000e0003800070000700000000000007ffffffff8000fffffffffffffffffffffffc0007ffc0fffff8000fff81fffff0360003ffe07ffffc0d81b0000fff81fffff03606c06c0001fff03ffffe06c0d80d806c0000fff81fffff03606c06c03600d80000fff81fffff03606c06c03600d801b00000fff81fffff03606c06c03600d801b001b000007ffc0fffff81b03603601b006c00d800d8006c00000fff81fffff03606c06c03600d801b001b000d80036000003ffe07ffffc0d81b01b00d8036006c006c0036000d8001b000000fff81fffff03606c06c03600d801b001b000d800360006c0006c0000000000007ffffffff8000ffffffffffff8000fff81ffc0007ffc0ffe068000fff81ffc0d0340003ffe07ff0340d01a0000fff81ffc0d0340680680001fff03ff81a0680d00d00680000fff81ffc0d03406806803400d00000fff81ffc0d03406806803400d001a00000fff81ffc0d03406806803400d001a001a000007ffc0ffe0681a03403401a006800d000d0006800000fff81ffc0d03406806803400d001a001a000d00034000003ffe07ff0340d01a01a00d0034006800680034000d0001a000000fff81ffc0d03406806803400d001a001a000d0003400068000680000000000007ffffffff8000fff8000fff81fffffffffffc0007ffc0c0dff8000fff8181bff0320003ffe0606ffc0c8190000fff8181bff0320640640001fff03037fe0640c80c80640000fff8181bff03206406403200c80000fff8181bff03206406403200c801900000fff8181bff03206406403200c80190019000007ffc0c0dff819032032019006400c800c8006400000fff8181bff03206406403200c80190019000c80032000003ffe0606ffc0c81901900c8032006400640032000c80019000000fff8181bff03206406403200c80190019000c8003200064000640000000000007ffffffff8000fff8000fff818000fff818180007ffc0c0c060000fff818180c0300003ffe06060300c0180000fff818180c0300600600001fff03030180600c00c00600000fff818180c03006006003000c00000fff818180c03006006003000c001800000fff818180c03006006003000c00180018000007ffc0c0c06018030030018006000c000c0006000000fff818180c03006006003000c00180018000c00030000003ffe06060300c01801800c0030006000600030000c00018000000fff818180c03006006003000c00180018000c0003000060000600000000000007fff0001ffffffffffffffffffffffffffffc0007e07ffffff8000fc0fffffff02e0003f03ffffffc0b8170000fc0fffffff02e05c05c0001f81ffffffe05c0b80b805c0000fc0fffffff02e05c05c02e00b80000fc0fffffff02e05c05c02e00b801700000fc0fffffff02e05c05c02e00b80170017000007e07ffffff81702e02e017005c00b800b8005c00000fc0fffffff02e05c05c02e00b80170017000b8002e000003f03ffffffc0b81701700b802e005c005c002e000b80017000000fc0fffffff02e05c05c02e00b80170017000b8002e0005c0005c0000000000007fff0001fffffffffffffffff8000fc0ffffc0007e07fffe058000fc0ffffc0b02c0003f03ffff02c0b0160000fc0ffffc0b02c0580580001f81ffff8160580b00b00580000fc0ffffc0b02c05805802c00b00000fc0ffffc0b02c05805802c00b001600000fc0ffffc0b02c05805802c00b00160016000007e07fffe0581602c02c016005800b000b0005800000fc0ffffc0b02c05805802c00b00160016000b0002c000003f03ffff02c0b01601600b002c00580058002c000b00016000000fc0ffffc0b02c05805802c00b00160016000b0002c00058000580000000000007fff0001ffffffff8000fc0fffffffffffffc0007e07fc0bff8000fc0ff817ff02a0003f03fe05ffc0a8150000fc0ff817ff02a0540540001f81ff02ffe0540a80a80540000fc0ff817ff02a05405402a00a80000fc0ff817ff02a05405402a00a801500000fc0ff817ff02a05405402a00a80150015000007e07fc0bff81502a02a015005400a800a8005400000fc0ff817ff02a05405402a00a80150015000a8002a000003f03fe05ffc0a81501500a802a00540054002a000a80015000000fc0ff817ff02a05405402a00a80150015000a8002a00054000540000000000007fff0001ffffffff8000fc0ff8000fc0ff8140007e07fc0a050000fc0ff8140a0280003f03fe050280a0140000fc0ff8140a0280500500001f81ff028140500a00a00500000fc0ff8140a02805005002800a00000fc0ff8140a02805005002800a001400000fc0ff8140a02805005002800a00140014000007e07fc0a05014028028014005000a000a0005000000fc0ff8140a02805005002800a00140014000a00028000003f03fe050280a01401400a0028005000500028000a00014000000fc0ff8140a02805005002800a00140014000a0002800050000500000000000007fff0001f8000fc0ffffffffffffffffffffc0007e040bffff8000fc0817ffff0260003f0205ffffc098130000fc0817ffff02604c04c0001f8102ffffe04c09809804c0000fc0817ffff02604c04c02600980000fc0817ffff02604c04c026009801300000fc0817ffff02604c04c02600980130013000007e040bffff813026026013004c00980098004c00000fc0817ffff02604c04c02600980130013000980026000003f0205ffffc098130130098026004c004c0026000980013000000fc0817ffff02604c04c026009801300130009800260004c0004c0000000000007fff0001f8000fc0fffffffff8000fc0817fc0007e040bfe048000fc0817fc090240003f0205ff024090120000fc0817fc090240480480001f8102ff8120480900900480000fc0817fc0902404804802400900000fc0817fc09024048048024009001200000fc0817fc0902404804802400900120012000007e040bfe04812024024012004800900090004800000fc0817fc0902404804802400900120012000900024000003f0205ff024090120120090024004800480024000900012000000fc0817fc090240480480240090012001200090002400048000480000000000007fff0001f8000fc08000fc0817ffffffffffc0007e040809ff8000fc081013ff0220003f020404ffc088110000fc081013ff0220440440001f8102027fe0440880880440000fc081013ff02204404402200880000fc081013ff022044044022008801100000fc081013ff02204404402200880110011000007e040809ff811022022011004400880088004400000fc081013ff02204404402200880110011000880022000003f020404ffc088110110088022004400440022000880011000000fc081013ff0220440440220088011001100088002200044000440000000000007fff0001f8000fc08000fc0810000fc0810100007e040808040000fc081010080200003f020404020080100000fc081010080200400400001f8102020100400800800400000fc0810100802004004002000800000fc08101008020040040020008001000000fc0810100802004004002000800100010000007e04080804010020020010004000800080004000000fc0810100802004004002000800100010000800020000003f020404020080100100080020004000400020000800010000000fc081010080200400400200080010001000080002000040000400000000000000000ffffffffffffffffffffffffffffffffc00001ffffffff800003ffffffff01e00000ffffffffc0780f000003ffffffff01e03c03c000007fffffffe03c07807803c000003ffffffff01e03c03c01e0078000003ffffffff01e03c03c01e007800f0000003ffffffff01e03c03c01e007800f000f0000001ffffffff80f01e01e00f003c00780078003c0000003ffffffff01e03c03c01e007800f000f00078001e0000000ffffffffc0780f00f007801e003c003c001e00078000f00000003ffffffff01e03c03c01e007800f000f00078001e0003c0003c0000000000000000fffffffffffffffffffff800003fffffc00001fffffe03800003fffffc0701c00000ffffff01c0700e000003fffffc0701c038038000007fffff80e038070070038000003fffffc0701c03803801c0070000003fffffc0701c03803801c007000e0000003fffffc0701c03803801c007000e000e0000001fffffe0380e01c01c00e00380070007000380000003fffffc0701c03803801c007000e000e00070001c0000000ffffff01c0700e00e007001c00380038001c00070000e00000003fffffc0701c03803801c007000e000e00070001c00038000380000000000000000ffffffffffff800003ffffffffffffffc00001fffc07ff800003fff80fff01a00000fffe03ffc0680d000003fff80fff01a034034000007fff01ffe034068068034000003fff80fff01a03403401a0068000003fff80fff01a03403401a006800d0000003fff80fff01a03403401a006800d000d0000001fffc07ff80d01a01a00d00340068006800340000003fff80fff01a03403401a006800d000d00068001a0000000fffe03ffc0680d00d006801a00340034001a00068000d00000003fff80fff01a03403401a006800d000d00068001a00034000340000000000000000ffffffffffff800003fff800003fff80c00001fffc0603000003fff80c0601800000fffe030180600c000003fff80c06018030030000007fff0180c030060060030000003fff80c060180300300180060000003fff80c06018030030018006000c0000003fff80c06018030030018006000c000c0000001fffc060300c01801800c00300060006000300000003fff80c06018030030018006000c000c0006000180000000fffe030180600c00c006001800300030001800060000c00000003fff80c06018030030018006000c000c00060001800030000300000000000000000fffff800003fffffffffffffffffffffc00001fc07ffff800003f80fffff01600000fe03ffffc0580b000003f80fffff01602c02c000007f01ffffe02c05805802c000003f80fffff01602c02c0160058000003f80fffff01602c02c016005800b0000003f80fffff01602c02c016005800b000b0000001fc07ffff80b01601600b002c00580058002c0000003f80fffff01602c02c016005800b000b0005800160000000fe03ffffc0580b00b0058016002c002c001600058000b00000003f80fffff01602c02c016005800b000b0005800160002c0002c0000000000000000fffff800003ffffffffff800003f80ffc00001fc07fe02800003f80ffc0501400000fe03ff0140500a000003f80ffc05014028028000007f01ff80a028050050028000003f80ffc050140280280140050000003f80ffc05014028028014005000a0000003f80ffc05014028028014005000a000a0000001fc07fe0280a01401400a00280050005000280000003f80ffc05014028028014005000a000a0005000140000000fe03ff0140500a00a005001400280028001400050000a00000003f80ffc05014028028014005000a000a00050001400028000280000000000000000fffff800003f800003f80fffffffffffc00001fc0405ff800003f8080bff01200000fe0202ffc04809000003f8080bff012024024000007f01017fe024048048024000003f8080bff0120240240120048000003f8080bff01202402401200480090000003f8080bff012024024012004800900090000001fc0405ff80901201200900240048004800240000003f8080bff012024024012004800900090004800120000000fe0202ffc04809009004801200240024001200048000900000003f8080bff0120240240120048009000900048001200024000240000000000000000fffff800003f800003f80800003f8080800001fc040402000003f808080401000000fe020201004008000003f8080804010020020000007f0101008020040040020000003f80808040100200200100040000003f808080401002002001000400080000003f8080804010020020010004000800080000001fc04040200801001000800200040004000200000003f8080804010020020010004000800080004000100000000fe020201004008008004001000200020001000040000800000003f80808040100200200100040008000800040001000020000200000000000000000000007ffffffffffffffffffffffffffc0000003ffffff80000007ffffff00e0000001ffffffc0380700000007ffffff00e01c01c0000000ffffffe01c03803801c00000007ffffff00e01c01c00e003800000007ffffff00e01c01c00e0038007000000007ffffff00e01c01c00e00380070007000000003ffffff80700e00e007001c00380038001c000000007ffffff00e01c01c00e0038007000700038000e000000001ffffffc03807007003800e001c001c000e0003800070000000007ffffff00e01c01c00e0038007000700038000e0001c0001c0000000000000000000007fffffffffffffff80000007fffc0000003fffe0180000007fffc0300c0000001ffff00c0300600000007fffc0300c0180180000000ffff80601803003001800000007fffc0300c01801800c003000000007fffc0300c01801800c0030006000000007fffc0300c01801800c00300060006000000003fffe0180600c00c0060018003000300018000000007fffc0300c01801800c0030006000600030000c000000001ffff00c03006006003000c00180018000c0003000060000000007fffc0300c01801800c0030006000600030000c00018000180000000000000000000007ffffff80000007ffffffffffffc0000003fc03ff80000007f807ff00a0000001fe01ffc0280500000007f807ff00a0140140000000ff00ffe01402802801400000007f807ff00a01401400a002800000007f807ff00a01401400a0028005000000007f807ff00a01401400a00280050005000000003fc03ff80500a00a0050014002800280014000000007f807ff00a01401400a0028005000500028000a000000001fe01ffc02805005002800a00140014000a0002800050000000007f807ff00a01401400a0028005000500028000a00014000140000000000000000000007ffffff80000007f80000007f8040000003fc020100000007f804020080000001fe010080200400000007f804020080100100000000ff0080401002002001000000007f80402008010010008002000000007f804020080100100080020004000000007f8040200801001000800200040004000000003fc02010040080080040010002000200010000000007f8040200801001000800200040004000200008000000001fe010080200400400200080010001000080002000040000000007f8040200801001000800200040004000200008000100001000000000000000000000000000007fffffffffffffffffffc000000003ffff8000000007ffff006000000001ffffc018030000000007ffff00600c00c000000000ffffe00c01801800c0000000007ffff00600c00c00600180000000007ffff00600c00c006001800300000000007ffff00600c00c0060018003000300000000003ffff803006006003000c00180018000c00000000007ffff00600c00c0060018003000300018000600000000001ffffc018030030018006000c000c0006000180003000000000007ffff00600c00c006001800300030001800060000c0000c00000000000000000000000000007ffffffff8000000007fc000000003fe008000000007fc01004000000001ff004010020000000007fc01004008008000000000ff8020080100100080000000007fc0100400800800400100000000007fc01004008008004001000200000000007fc010040080080040010002000200000000003fe00802004004002000800100010000800000000007fc010040080080040010002000200010000400000000001ff004010020020010004000800080004000100002000000000007fc0100400800800400100020002000100004000080000800000000000000000000000000000000000007ffffffffffc00000000001ff800000000003ff00200000000000ffc00801000000000003ff002004004000000000007fe004008008004000000000003ff0020040040020008000000000003ff00200400400200080010000000000003ff002004004002000800100010000000000001ff80100200200100040008000800040000000000003ff002004004002000800100010000800020000000000000ffc00801001000800200040004000200008000100000000000003ff002004004002000800100010000800020000400004000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
def UMT3 : ℕ := 0x7fffffffffffff7ffffbe7ffffbe7c7ffffbe7c7c3ffffdf3e3e1f07ffffbe7c7c3e0f81ffffef9f1f0f83e07c07ffffbe7c7c3e0f81f01f00fffff7cf8f87c1f03e03e01f007ffffbe7c7c3e0f81f01f00f803e007ffffbe7c7c3e0f81f01f00f803e007c007ffffbe7c7c3e0f81f01f00f803e007c007c003ffffdf3e3e1f07c0f80f807c01f003e003e001f0007ffffbe7c7c3e0f81f01f00f803e007c007c003e000f8001ffffef9f1f0f83e07c07c03e00f801f001f000f8003e0007c0007ffffbe7c7c3e0f81f01f00f803e007c007c003e000f8001f0001f0000000007fffffffefffde7ffef3c7ffef3c787ffef3c78783fff79e3c3c1e07ffef3c78783c0f01fffbcf1e1e0f03c07807ffef3c78783c0f01e01e00fffde78f0f0781e03c03c01e007ffef3c78783c0f01e01e00f003c007ffef3c78783c0f01e01e00f003c0078007ffef3c78783c0f01e01e00f003c00780078003fff79e3c3c1e0780f00f007801e003c003c001e0007ffef3c78783c0f01e01e00f003c00780078003c000f0001fffbcf1e1e0f03c07807803c00f001e001e000f0003c000780007ffef3c78783c0f01e01e00f003c00780078003c000f0001e0001e0000000007fffffffdfffbd7ffdeba7ffdeba747ffdeba74743ffef5d3a3a1d07ffdeba74743a0e81fff7ae9d1d0e83a07407ffdeba74743a0e81d01d00fffbd74e8e8741d03a03a01d007ffdeba74743a0e81d01d00e803a007ffdeba74743a0e81d01d00e803a0074007ffdeba74743a0e81d01d00e803a00740074003ffef5d3a3a1d0740e80e807401d003a003a001d0007ffdeba74743a0e81d01d00e803a00740074003a000e8001fff7ae9d1d0e83a07407403a00e801d001d000e8003a000740007ffdeba74743a0e81d01d00e803a00740074003a000e8001d0001d0000000007ffff7fdcffb9c7fdce387fdce38707fdce3870703fee71c38381c07fdce387070380e01ff738e1c1c0e03807007fdce387070380e01c01c00ffb9c70e0e0701c03803801c007fdce387070380e01c01c00e0038007fdce387070380e01c01c00e00380070007fdce387070380e01c01c00e003800700070003fee71c38381c0700e00e007001c00380038001c0007fdce387070380e01c01c00e0038007000700038000e0001ff738e1c1c0e03807007003800e001c001c000e00038000700007fdce387070380e01c01c00e0038007000700038000e0001c0001c0000000007fffffffbfff7b7ffbdb67ffbdb66c7ffbdb66c6c3ffdedb36361b07ffbdb66c6c360d81ffef6d9b1b0d83606c07ffbdb66c6c360d81b01b00fff7b6cd8d86c1b03603601b007ffbdb66c6c360d81b01b00d8036007ffbdb66c6c360d81b01b00d8036006c007ffbdb66c6c360d81b01b00d8036006c006c003ffdedb36361b06c0d80d806c01b00360036001b0007ffbdb66c6c360d81b01b00d8036006c006c0036000d8001ffef6d9b1b0d83606c06c03600d801b001b000d800360006c0007ffbdb66c6c360d81b01b00d8036006c006c0036000d8001b0001b0000000007fffeffbaff75a7fbad347fbad34687fbad3468683fdd69a34341a07fbad346868340d01feeb4d1a1a0d03406807fbad346868340d01a01a00ff75a68d0d0681a03403401a007fbad346868340d01a01a00d0034007fbad346868340d01a01a00d00340068007fbad346868340d01a01a00d003400680068003fdd69a34341a0680d00d006801a00340034001a0007fbad346868340d01a01a00d0034006800680034000d0001feeb4d1a1a0d03406806803400d001a001a000d00034000680007fbad346868340d01a01a00d0034006800680034000d0001a0001a0000000007fff7fdf9fbf397df9cb27df9cb2647df9cb264643efce5932321907df9cb26464320c81f7e72c99190c83206407df9cb26464320c81901900fbf3964c8c86419032032019007df9cb26464320c81901900c8032007df9cb26464320c81901900c80320064007df9cb26464320c81901900c803200640064003efce593232190640c80c80640190032003200190007df9cb26464320c81901900c8032006400640032000c8001f7e72c99190c83206406403200c80190019000c80032000640007df9cb26464320c81901900c8032006400640032000c80019000190000000007fdf67d98fb3187d98c307d98c30607d98c3060603ecc61830301807d98c306060300c01f6630c18180c03006007d98c306060300c01801800fb31860c0c06018030030018007d98c306060300c01801800c0030007d98c306060300c01801800c00300060007d98c306060300c01801800c003000600060003ecc6183030180600c00c00600180030003000180007d98c306060300c01801800c0030006000600030000c0001f6630c18180c03006006003000c00180018000c00030000600007d98c306060300c01801800c0030006000600030000c00018000180000000007fffffff7ffef77ff7bae7ff7bae5c7ff7bae5c5c3ffbdd72e2e1707ff7bae5c5c2e0b81ffdeeb97170b82e05c07ff7bae5c5c2e0b81701700ffef75cb8b85c1702e02e017007ff7bae5c5c2e0b81701700b802e007ff7bae5c5c2e0b81701700b802e005c007ff7bae5c5c2e0b81701700b802e005c005c003ffbdd72e2e1705c0b80b805c017002e002e00170007ff7bae5c5c2e0b81701700b802e005c005c002e000b8001ffdeeb97170b82e05c05c02e00b80170017000b8002e0005c0007ff7bae5c5c2e0b81701700b802e005c005c002e000b80017000170000000007fffdff76feed67f76b2c7f76b2c587f76b2c58583fbb5962c2c1607f76b2c58582c0b01fddacb16160b02c05807f76b2c58582c0b01601600feed658b0b0581602c02c016007f76b2c58582c0b01601600b002c007f76b2c58582c0b01601600b002c0058007f76b2c58582c0b01601600b002c00580058003fbb5962c2c160580b00b0058016002c002c00160007f76b2c58582c0b01601600b002c00580058002c000b0001fddacb16160b02c05805802c00b00160016000b0002c000580007f76b2c58582c0b01601600b002c00580058002c000b00016000160000000007ffeffbf5f7eb57bf5aaa7bf5aaa547bf5aaa54543dfad552a2a1507bf5aaa54542a0a81efd6aa95150a82a05407bf5aaa54542a0a81501500f7eb554a8a8541502a02a015007bf5aaa54542a0a81501500a802a007bf5aaa54542a0a81501500a802a0054007bf5aaa54542a0a81501500a802a00540054003dfad552a2a150540a80a8054015002a002a00150007bf5aaa54542a0a81501500a802a00540054002a000a8001efd6aa95150a82a05405402a00a80150015000a8002a000540007bf5aaa54542a0a81501500a802a00540054002a000a80015000150000000007fbed7b54f6a947b54a287b54a28507b54a2850503daa51428281407b54a285050280a01ed528a14140a02805007b54a285050280a01401400f6a9450a0a05014028028014007b54a285050280a01401400a0028007b54a285050280a01401400a00280050007b54a285050280a01401400a002800500050003daa5142828140500a00a00500140028002800140007b54a285050280a01401400a0028005000500028000a0001ed528a14140a02805005002800a00140014000a00028000500007b54a285050280a01401400a0028005000500028000a00014000140000000007ffbfeff3dfe736ff39a66ff39a64c6ff39a64c4c37f9cd326261306ff39a64c4c260981bfce6993130982604c06ff39a64c4c260981301300dfe734c98984c13026026013006ff39a64c4c26098130130098026006ff39a64c4c26098130130098026004c006ff39a64c4c26098130130098026004c004c0037f9cd326261304c09809804c0130026002600130006ff39a64c4c26098130130098026004c004c002600098001bfce6993130982604c04c026009801300130009800260004c0006ff39a64c4c26098130130098026004c004c0026000980013000130000000007efbcef32de6526f329246f32924486f329244848379949224241206f329244848240901bcca4912120902404806f329244848240901201200de6524890904812024024012006f32924484824090120120090024006f329244848240901201200900240048006f32924484824090120120090024004800480037994922424120480900900480120024002400120006f3292448482409012012009002400480048002400090001bcca4912120902404804802400900120012000900024000480006f329244848240901201200900240048004800240009000120001200000000077fa7e9f1d3e3169f18a269f18a24469f18a2444434f8c51222211069f18a24444220881a7c628911108822044069f18a24444220881101100d3e3144888844110220220110069f18a24444220881101100880220069f18a244442208811011008802200440069f18a2444422088110110088022004400440034f8c5122221104408808804401100220022001100069f18a244442208811011008802200440044002200088001a7c628911108822044044022008801100110008800220004400069f18a244442208811011008802200440044002200088001100011000000000769a46910d22106910820691082040691082040403488410202010069108204040200801a44208101008020040069108204040200801001000d22104080804010020020010006910820404020080100100080020006910820404020080100100080020004000691082040402008010010008002000400040003488410202010040080080040010002000200010000691082040402008010010008002000400040002000080001a4420810100802004004002000800100010000800020000400006910820404020080100100080020004000400020000800010000100000000007ffffffefffdef7fef79e7fef79e3c7fef79e3c3c3ff7bcf1e1e0f07fef79e3c3c1e0781ffbde78f0f0781e03c07fef79e3c3c1e0780f00f00ffdef3c78783c0f01e01e00f007fef79e3c3c1e0780f00f007801e007fef79e3c3c1e0780f00f007801e003c007fef79e3c3c1e0780f00f007801e003c003c003ff7bcf1e1e0f03c07807803c00f001e001e000f0007fef79e3c3c1e0780f00f007801e003c003c001e00078001ffbde78f0f0781e03c03c01e007800f000f00078001e0003c0007fef79e3c3c1e0780f00f007801e003c003c001e00078000f0000f0000000007fffbfeeefddce7eee71c7eee71c387eee71c38383f7738e1c1c0e07eee71c38381c0701fbb9c70e0e0701c03807eee71c38381c0700e00e00fddce387070380e01c01c00e007eee71c38381c0700e00e007001c007eee71c38381c0700e00e007001c0038007eee71c38381c0700e00e007001c00380038003f7738e1c1c0e03807007003800e001c001c000e0007eee71c38381c0700e00e007001c00380038001c00070001fbb9c70e0e0701c03803801c007000e000e00070001c000380007eee71c38381c0700e00e007001c00380038001c00070000e0000e0000000007ffdff7edefdad77ed69a77ed69a3477ed69a34343bf6b4d1a1a0d077ed69a34341a0681dfb5a68d0d0681a034077ed69a34341a0680d00d00efdad346868340d01a01a00d0077ed69a34341a0680d00d006801a0077ed69a34341a0680d00d006801a00340077ed69a34341a0680d00d006801a00340034003bf6b4d1a1a0d03406806803400d001a001a000d00077ed69a34341a0680d00d006801a00340034001a00068001dfb5a68d0d0681a03403401a006800d000d00068001a0003400077ed69a34341a0680d00d006801a00340034001a00068000d0000d0000000007f7db76cced98c76cc61876cc6183076cc61830303b6630c18180c076cc6183030180601db31860c0c06018030076cc6183030180600c00c00ed98c306060300c01801800c0076cc6183030180600c00c00600180076cc6183030180600c00c006001800300076cc6183030180600c00c006001800300030003b6630c18180c03006006003000c00180018000c00076cc6183030180600c00c006001800300030001800060001db31860c0c06018030030018006000c000c0006000180003000076cc6183030180600c00c006001800300030001800060000c0000c0000000007ff7fdfebbfd6b5feb5965feb5962c5feb5962c2c2ff5acb16160b05feb5962c2c1605817fad658b0b0581602c05feb5962c2c160580b00b00bfd6b2c58582c0b01601600b005feb5962c2c160580b00b0058016005feb5962c2c160580b00b0058016002c005feb5962c2c160580b00b0058016002c002c002ff5acb16160b02c05805802c00b00160016000b0005feb5962c2c160580b00b0058016002c002c0016000580017fad658b0b0581602c02c016005800b000b0005800160002c0005feb5962c2c160580b00b0058016002c002c001600058000b0000b0000000007df7adeaabd54a5eaa5145eaa514285eaa51428282f5528a14140a05eaa51428281405017aa9450a0a0501402805eaa5142828140500a00a00bd54a285050280a01401400a005eaa5142828140500a00a0050014005eaa5142828140500a00a00500140028005eaa5142828140500a00a005001400280028002f5528a14140a02805005002800a00140014000a0005eaa5142828140500a00a0050014002800280014000500017aa9450a0a05014028028014005000a000a000500014000280005eaa5142828140500a00a005001400280028001400050000a0000a0000000006ff57d5e9abd2955e949255e94922455e949224242af4a49121209055e9492242412048157a524890904812024055e94922424120480900900abd2924484824090120120090055e94922424120480900900480120055e949224241204809009004801200240055e949224241204809009004801200240024002af4a4912120902404804802400900120012000900055e94922424120480900900480120024002400120004800157a524890904812024024012004800900090004800120002400055e9492242412048090090048012002400240012000480009000090000000006d5525488a91085488410548841020548841020202a44208101008054884102020100401522104080804010020054884102020100400800800a91082040402008010010008005488410202010040080080040010005488410202010040080080040010002000548841020201004008008004001000200020002a4420810100802004004002000800100010000800054884102020100400800800400100020002000100004000152210408080401002002001000400080008000400010000200005488410202010040080080040010002000200010000400008000080000000007feffbfe77fce73fe738e3fe738e1c3fe738e1c1c1ff39c70e0e0703fe738e1c1c0e0380ff9ce387070380e01c03fe738e1c1c0e03807007007fce71c38381c0700e00e007003fe738e1c1c0e03807007003800e003fe738e1c1c0e03807007003800e001c003fe738e1c1c0e03807007003800e001c001c001ff39c70e0e0701c03803801c007000e000e00070003fe738e1c1c0e03807007003800e001c001c000e00038000ff9ce387070380e01c01c00e0038007000700038000e0001c0003fe738e1c1c0e03807007003800e001c001c000e000380007000070000000007bef9be667ccc63e6630c3e6630c183e6630c18181f331860c0c0603e6630c18180c0300f998c306060300c01803e6630c18180c03006006007ccc6183030180600c00c006003e6630c18180c03006006003000c003e6630c18180c03006006003000c0018003e6630c18180c03006006003000c00180018001f331860c0c06018030030018006000c000c00060003e6630c18180c03006006003000c00180018000c00030000f998c306060300c01801800c0030006000600030000c000180003e6630c18180c03006006003000c00180018000c000300006000060000000005fecfb3e567ca533e528a33e528a1433e528a141419f29450a0a05033e528a14140a0280cf94a285050280a014033e528a14140a028050050067ca5142828140500a00a0050033e528a14140a02805005002800a0033e528a14140a02805005002800a00140033e528a14140a02805005002800a001400140019f29450a0a05014028028014005000a000a000500033e528a14140a02805005002800a00140014000a00028000cf94a285050280a01401400a0028005000500028000a0001400033e528a14140a02805005002800a00140014000a000280005000050000000005b2c93244648843244208324420810324420810101922104080804032442081010080200c91082040402008010032442081010080200400400648841020201004008008004003244208101008020040040020008003244208101008020040040020008001000324420810100802004004002000800100010001922104080804010020020010004000800080004000324420810100802004004002000800100010000800020000c9108204040200801001000800200040004000200008000100003244208101008020040040020008001000100008000200004000040000000003fe3f8fe31fc630fe31860fe31860c0fe31860c0c07f18c306060300fe31860c0c0601803f8c6183030180600c00fe31860c0c0601803003001fc630c18180c03006006003000fe31860c0c06018030030018006000fe31860c0c06018030030018006000c000fe31860c0c06018030030018006000c000c0007f18c306060300c01801800c0030006000600030000fe31860c0c06018030030018006000c000c0006000180003f8c6183030180600c00c006001800300030001800060000c0000fe31860c0c06018030030018006000c000c00060001800030000300000000038e388e221c4420e221040e22104080e221040808071108204040200e22104080804010038884102020100400800e2210408080401002002001c4420810100802004004002000e22104080804010020020010004000e221040808040100200200100040008000e22104080804010020020010004000800080007110820404020080100100080020004000400020000e221040808040100200200100040008000800040001000038884102020100400800800400100020002000100004000080000e221040808040100200200100040008000800040001000020000200000000007e0781e103c2101e108201e10820401e1082040400f0841020201001e10820404020080078420810100802004001e1082040402008010010003c2104080804010020020010001e10820404020080100100080020001e108204040200801001000800200040001e1082040402008010010008002000400040000f084102020100400800800400100020002000100001e108204040200801001000800200040004000200008000078420810100802004004002000800100010000800020000400001e10820404020080100100080020004000400020000800010000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007fffffffffffff7ffffbe7ffffbe7c7ffffbe7c7c3ffffdf3e3e1f07ffffbe7c7c3e0f81ffffef9f1f0f83e07c07ffffbe7c7c3e0f81f01f00fffff7cf8f87c1f03e03e01f007ffffbe7c7c3e0f81f01f00f803e007ffffbe7c7c3e0f81f01f00f803e007c007ffffbe7c7c3e0f81f01f00f803e007c007c003ffffdf3e3e1f07c0f80f807c01f003e003e001f0007ffffbe7c7c3e0f81f01f00f803e007c007c003e000f8001ffffef9f1f0f83e07c07c03e00f801f001f000f8003e0007c0007ffffbe7c7c3e0f81f01f00f803e007c007c003e000f8001f0001f0000000007fffffffefffde7ffef3c7ffef3c787ffef3c78783fff79e3c3c1e07ffef3c78783c0f01fffbcf1e1e0f03c07807ffef3c78783c0f01e01e00fffde78f0f0781e03c03c01e007ffef3c78783c0f01e01e00f003c007ffef3c78783c0f01e01e00f003c0078007ffef3c78783c0f01e01e00f003c00780078003fff79e3c3c1e0780f00f007801e003c003c001e0007ffef3c78783c0f01e01e00f003c00780078003c000f0001fffbcf1e1e0f03c07807803c00f001e001e000f0003c000780007ffef3c78783c0f01e01e00f003c00780078003c000f0001e0001e0000000007fffffffdfffbd7ffdeba7ffdeba747ffdeba74743ffef5d3a3a1d07ffdeba74743a0e81fff7ae9d1d0e83a07407ffdeba74743a0e81d01d00fffbd74e8e8741d03a03a01d007ffdeba74743a0e81d01d00e803a007ffdeba74743a0e81d01d00e803a0074007ffdeba74743a0e81d01d00e803a00740074003ffef5d3a3a1d0740e80e807401d003a003a001d0007ffdeba74743a0e81d01d00e803a00740074003a000e8001fff7ae9d1d0e83a07407403a00e801d001d000e8003a000740007ffdeba74743a0e81d01d00e803a00740074003a000e8001d0001d0000000007ffff7fdcffb9c7fdce387fdce38707fdce3870703fee71c38381c07fdce387070380e01ff738e1c1c0e03807007fdce387070380e01c01c00ffb9c70e0e0701c03803801c007fdce387070380e01c01c00e0038007fdce387070380e01c01c00e00380070007fdce387070380e01c01c00e003800700070003fee71c38381c0700e00e007001c00380038001c0007fdce387070380e01c01c00e0038007000700038000e0001ff738e1c1c0e03807007003800e001c001c000e00038000700007fdce387070380e01c01c00e0038007000700038000e0001c0001c0000000007fffffffbfff7b7ffbdb67ffbdb66c7ffbdb66c6c3ffdedb36361b07ffbdb66c6c360d81ffef6d9b1b0d83606c07ffbdb66c6c360d81b01b00fff7b6cd8d86c1b03603601b007ffbdb66c6c360d81b01b00d8036007ffbdb66c6c360d81b01b00d8036006c007ffbdb66c6c360d81b01b00d8036006c006c003ffdedb36361b06c0d80d806c01b00360036001b0007ffbdb66c6c360d81b01b00d8036006c006c0036000d8001ffef6d9b1b0d83606c06c03600d801b001b000d800360006c0007ffbdb66c6c360d81b01b00d8036006c006c0036000d8001b0001b0000000007fffeffbaff75a7fbad347fbad34687fbad3468683fdd69a34341a07fbad346868340d01feeb4d1a1a0d03406807fbad346868340d01a01a00ff75a68d0d0681a03403401a007fbad346868340d01a01a00d0034007fbad346868340d01a01a00d00340068007fbad346868340d01a01a00d003400680068003fdd69a34341a0680d00d006801a00340034001a0007fbad346868340d01a01a00d0034006800680034000d0001feeb4d1a1a0d03406806803400d001a001a000d00034000680007fbad346868340d01a01a00d0034006800680034000d0001a0001a0000000007fff7fdf9fbf397df9cb27df9cb2647df9cb264643efce5932321907df9cb26464320c81f7e72c99190c83206407df9cb26464320c81901900fbf3964c8c86419032032019007df9cb26464320c81901900c8032007df9cb26464320c81901900c80320064007df9cb26464320c81901900c803200640064003efce593232190640c80c80640190032003200190007df9cb26464320c81901900c8032006400640032000c8001f7e72c99190c83206406403200c80190019000c80032000640007df9cb26464320c81901900c8032006400640032000c80019000190000000007fdf67d98fb3187d98c307d98c30607d98c3060603ecc61830301807d98c306060300c01f6630c18180c03006007d98c306060300c01801800fb31860c0c06018030030018007d98c306060300c01801800c0030007d98c306060300c01801800c00300060007d98c306060300c01801800c003000600060003ecc6183030180600c00c00600180030003000180007d98c306060300c01801800c0030006000600030000c0001f6630c18180c03006006003000c00180018000c00030000600007d98c306060300c01801800c0030006000600030000c00018000180000000007fffffff7ffef77ff7bae7ff7bae5c7ff7bae5c5c3ffbdd72e2e1707ff7bae5c5c2e0b81ffdeeb97170b82e05c07ff7bae5c5c2e0b81701700ffef75cb8b85c1702e02e017007ff7bae5c5c2e0b81701700b802e007ff7bae5c5c2e0b81701700b802e005c007ff7bae5c5c2e0b81701700b802e005c005c003ffbdd72e2e1705c0b80b805c017002e002e00170007ff7bae5c5c2e0b81701700b802e005c005c002e000b8001ffdeeb97170b82e05c05c02e00b80170017000b8002e0005c0007ff7bae5c5c2e0b81701700b802e005c005c002e000b80017000170000000007fffdff76feed67f76b2c7f76b2c587f76b2c58583fbb5962c2c1607f76b2c58582c0b01fddacb16160b02c05807f76b2c58582c0b01601600feed658b0b0581602c02c016007f76b2c58582c0b01601600b002c007f76b2c58582c0b01601600b002c0058007f76b2c58582c0b01601600b002c00580058003fbb5962c2c160580b00b0058016002c002c00160007f76b2c58582c0b01601600b002c00580058002c000b0001fddacb16160b02c05805802c00b00160016000b0002c000580007f76b2c58582c0b01601600b002c00580058002c000b00016000160000000007ffeffbf5f7eb57bf5aaa7bf5aaa547bf5aaa54543dfad552a2a1507bf5aaa54542a0a81efd6aa95150a82a05407bf5aaa54542a0a81501500f7eb554a8a8541502a02a015007bf5aaa54542a0a81501500a802a007bf5aaa54542a0a81501500a802a0054007bf5aaa54542a0a81501500a802a00540054003dfad552a2a150540a80a8054015002a002a00150007bf5aaa54542a0a81501500a802a00540054002a000a8001efd6aa95150a82a05405402a00a80150015000a8002a000540007bf5aaa54542a0a81501500a802a00540054002a000a80015000150000000007fbed7b54f6a947b54a287b54a28507b54a2850503daa51428281407b54a285050280a01ed528a14140a02805007b54a285050280a01401400f6a9450a0a05014028028014007b54a285050280a01401400a0028007b54a285050280a01401400a00280050007b54a285050280a01401400a002800500050003daa5142828140500a00a00500140028002800140007b54a285050280a01401400a0028005000500028000a0001ed528a14140a02805005002800a00140014000a00028000500007b54a285050280a01401400a0028005000500028000a00014000140000000007ffbfeff3dfe736ff39a66ff39a64c6ff39a64c4c37f9cd326261306ff39a64c4c260981bfce6993130982604c06ff39a64c4c260981301300dfe734c98984c13026026013006ff39a64c4c26098130130098026006ff39a64c4c26098130130098026004c006ff39a64c4c26098130130098026004c004c0037f9cd326261304c09809804c0130026002600130006ff39a64c4c26098130130098026004c004c002600098001bfce6993130982604c04c026009801300130009800260004c0006ff39a64c4c26098130130098026004c004c0026000980013000130000000007efbcef32de6526f329246f32924486f329244848379949224241206f329244848240901bcca4912120902404806f329244848240901201200de6524890904812024024012006f32924484824090120120090024006f329244848240901201200900240048006f32924484824090120120090024004800480037994922424120480900900480120024002400120006f3292448482409012012009002400480048002400090001bcca4912120902404804802400900120012000900024000480006f329244848240901201200900240048004800240009000120001200000000077fa7e9f1d3e3169f18a269f18a24469f18a2444434f8c51222211069f18a24444220881a7c628911108822044069f18a24444220881101100d3e3144888844110220220110069f18a24444220881101100880220069f18a244442208811011008802200440069f18a2444422088110110088022004400440034f8c5122221104408808804401100220022001100069f18a244442208811011008802200440044002200088001a7c628911108822044044022008801100110008800220004400069f18a244442208811011008802200440044002200088001100011000000000769a46910d22106910820691082040691082040403488410202010069108204040200801a44208101008020040069108204040200801001000d22104080804010020020010006910820404020080100100080020006910820404020080100100080020004000691082040402008010010008002000400040003488410202010040080080040010002000200010000691082040402008010010008002000400040002000080001a4420810100802004004002000800100010000800020000400006910820404020080100100080020004000400020000800010000100000000007ffffffefffdef7fef79e7fef79e3c7fef79e3c3c3ff7bcf1e1e0f07fef79e3c3c1e0781ffbde78f0f0781e03c07fef79e3c3c1e0780f00f00ffdef3c78783c0f01e01e00f007fef79e3c3c1e0780f00f007801e007fef79e3c3c1e0780f00f007801e003c007fef79e3c3c1e0780f00f007801e003c003c003ff7bcf1e1e0f03c07807803c00f001e001e000f0007fef79e3c3c1e0780f00f007801e003c003c001e00078001ffbde78f0f0781e03c03c01e007800f000f00078001e0003c0007fef79e3c3c1e0780f00f007801e003c003c001e00078000f0000f0000000007fffbfeeefddce7eee71c7eee71c387eee71c38383f7738e1c1c0e07eee71c38381c0701fbb9c70e0e0701c03807eee71c38381c0700e00e00fddce387070380e01c01c00e007eee71c38381c0700e00e007001c007eee71c38381c0700e00e007001c0038007eee71c38381c0700e00e007001c00380038003f7738e1c1c0e03807007003800e001c001c000e0007eee71c38381c0700e00e007001c00380038001c00070001fbb9c70e0e0701c03803801c007000e000e00070001c000380007eee71c38381c0700e00e007001c00380038001c00070000e0000e0000000007ffdff7edefdad77ed69a77ed69a3477ed69a34343bf6b4d1a1a0d077ed69a34341a0681dfb5a68d0d0681a034077ed69a34341a0680d00d00efdad346868340d01a01a00d0077ed69a34341a0680d00d006801a0077ed69a34341a0680d00d006801a00340077ed69a34341a0680d00d006801a00340034003bf6b4d1a1a0d03406806803400d001a001a000d00077ed69a34341a0680d00d006801a00340034001a00068001dfb5a68d0d0681a03403401a006800d000d00068001a0003400077ed69a34341a0680d00d006801a00340034001a00068000d0000d0000000007f7db76cced98c76cc61876cc6183076cc61830303b6630c18180c076cc6183030180601db31860c0c06018030076cc6183030180600c00c00ed98c306060300c01801800c0076cc6183030180600c00c00600180076cc6183030180600c00c006001800300076cc6183030180600c00c006001800300030003b6630c18180c03006006003000c00180018000c00076cc6183030180600c00c006001800300030001800060001db31860c0c06018030030018006000c000c0006000180003000076cc6183030180600c00c006001800300030001800060000c0000c0000000007ff7fdfebbfd6b5feb5965feb5962c5feb5962c2c2ff5acb16160b05feb5962c2c1605817fad658b0b0581602c05feb5962c2c160580b00b00bfd6b2c58582c0b01601600b005feb5962c2c160580b00b0058016005feb5962c2c160580b00b0058016002c005feb5962c2c160580b00b0058016002c002c002ff5acb16160b02c05805802c00b00160016000b0005feb5962c2c160580b00b0058016002c002c0016000580017fad658b0b0581602c02c016005800b000b0005800160002c0005feb5962c2c160580b00b0058016002c002c001600058000b0000b0000000007df7adeaabd54a5eaa5145eaa514285eaa51428282f5528a14140a05eaa51428281405017aa9450a0a0501402805eaa5142828140500a00a00bd54a285050280a01401400a005eaa5142828140500a00a0050014005eaa5142828140500a00a00500140028005eaa5142828140500a00a005001400280028002f5528a14140a02805005002800a00140014000a0005eaa5142828140500a00a0050014002800280014000500017aa9450a0a05014028028014005000a000a000500014000280005eaa5142828140500a00a005001400280028001400050000a0000a0000000006ff57d5e9abd2955e949255e94922455e949224242af4a49121209055e9492242412048157a524890904812024055e94922424120480900900abd2924484824090120120090055e94922424120480900900480120055e949224241204809009004801200240055e949224241204809009004801200240024002af4a4912120902404804802400900120012000900055e94922424120480900900480120024002400120004800157a524890904812024024012004800900090004800120002400055e9492242412048090090048012002400240012000480009000090000000006d5525488a91085488410548841020548841020202a44208101008054884102020100401522104080804010020054884102020100400800800a91082040402008010010008005488410202010040080080040010005488410202010040080080040010002000548841020201004008008004001000200020002a4420810100802004004002000800100010000800054884102020100400800800400100020002000100004000152210408080401002002001000400080008000400010000200005488410202010040080080040010002000200010000400008000080000000007feffbfe77fce73fe738e3fe738e1c3fe738e1c1c1ff39c70e0e0703fe738e1c1c0e0380ff9ce387070380e01c03fe738e1c1c0e03807007007fce71c38381c0700e00e007003fe738e1c1c0e03807007003800e003fe738e1c1c0e03807007003800e001c003fe738e1c1c0e03807007003800e001c001c001ff39c70e0e0701c03803801c007000e000e00070003fe738e1c1c0e03807007003800e001c001c000e00038000ff9ce387070380e01c01c00e0038007000700038000e0001c0003fe738e1c1c0e03807007003800e001c001c000e000380007000070000000007bef9be667ccc63e6630c3e6630c183e6630c18181f331860c0c0603e6630c18180c0300f998c306060300c01803e6630c18180c03006006007ccc6183030180600c00c006003e6630c18180c03006006003000c003e6630c18180c03006006003000c0018003e6630c18180c03006006003000c00180018001f331860c0c06018030030018006000c000c00060003e6630c18180c03006006003000c00180018000c00030000f998c306060300c01801800c0030006000600030000c000180003e6630c18180c03006006003000c00180018000c000300006000060000000005fecfb3e567ca533e528a33e528a1433e528a141419f29450a0a05033e528a14140a0280cf94a285050280a014033e528a14140a028050050067ca5142828140500a00a0050033e528a14140a02805005002800a0033e528a14140a02805005002800a00140033e528a14140a02805005002800a001400140019f29450a0a05014028028014005000a000a000500033e528a14140a02805005002800a00140014000a00028000cf94a285050280a01401400a0028005000500028000a0001400033e528a14140a02805005002800a00140014000a000280005000050000000005b2c93244648843244208324420810324420810101922104080804032442081010080200c91082040402008010032442081010080200400400648841020201004008008004003244208101008020040040020008003244208101008020040040020008001000324420810100802004004002000800100010001922104080804010020020010004000800080004000324420810100802004004002000800100010000800020000c9108204040200801001000800200040004000200008000100003244208101008020040040020008001000100008000200004000040000000003fe3f8fe31fc630fe31860fe31860c0fe31860c0c07f18c306060300fe31860c0c0601803f8c6183030180600c00fe31860c0c0601803003001fc630c18180c03006006003000fe31860c0c06018030030018006000fe31860c0c06018030030018006000c000fe31860c0c06018030030018006000c000c0007f18c306060300c01801800c0030006000600030000fe31860c0c06018030030018006000c000c0006000180003f8c6183030180600c00c006001800300030001800060000c0000fe31860c0c06018030030018006000c000c00060001800030000300000000038e388e221c4420e221040e22104080e221040808071108204040200e22104080804010038884102020100400800e2210408080401002002001c4420810100802004004002000e22104080804010020020010004000e221040808040100200200100040008000e22104080804010020020010004000800080007110820404020080100100080020004000400020000e221040808040100200200100040008000800040001000038884102020100400800800400100020002000100004000080000e221040808040100200200100040008000800040001000020000200000000007e0781e103c2101e108201e10820401e1082040400f0841020201001e10820404020080078420810100802004001e1082040402008010010003c2104080804010020020010001e10820404020080100100080020001e108204040200801001000800200040001e1082040402008010010008002000400040000f084102020100400800800400100020002000100001e108204040200801001000800200040004000200008000078420810100802004004002000800100010000800020000400001e10820404020080100100080020004000400020000800010000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
/-- The bitmask (over `Fin 23`) of triple `i`. -/
def tri (i : ℕ) : ℕ := fieldOf TRIPL 32 i
/-- Triples containing point `c`. -/
def star (c : ℕ) : ℕ := fieldOf STARL 1792 c
/-- `∀ i < n, p i`, as a kernel loop. -/
def allN (n : ℕ) (p : ℕ → Bool) : Bool :=
Nat.rec (motive := fun _ => Bool) true (fun i ih => p i && ih) n
/-- Table check: `UMTj` is built bit by bit: field `0` is empty and field `2^t + r` (`r < 2^t`) is
field `r` together with `star (6j + t)`. -/
def umtOK (U j : ℕ) : Bool :=
Nat.beq (fieldOf U 1792 0) 0 &&
allN 6 (fun t => allN (2 ^ t) (fun r =>
Nat.beq (fieldOf U 1792 (Nat.add (Nat.shiftLeft 1 t) r))
(Nat.lor (fieldOf U 1792 r) (star (Nat.add (Nat.mul 6 j) t)))))
end R6Chk.Bit
end
section
-- Source module: Solutions.R6ChkBitDag
/-!
# Bit round six (h = 23): DAG well-formedness and output supports (kernel checkers)
For a support function `sg : ℕ → ℕ` (node ↦ bitmask over the 1771 triples; in use
`sg = supG`, a lookup in the support tree):
* `gchunkChk sg x`: every gate record `(k, a, b)` of the chunk has disjoint operand supports
whose union is the support of `k` (`gchunk_sound`);
* `ochunkChk sg x`: every output record `(c, t₁, t₂, n)` has
`sg n = star c \ (star t₁ ∪ star t₂)` (triples through `c` meeting `{c,t₁,t₂}` only in `c`);
* `rchunkChk sg x`: every retained record `(c, n)` has `sg n = star c`;
* `leafChk sg`: `sg 0 = 0` and `sg (i+1) = 2^i` (input triple `i`).
These are the data facts behind `JLV = I` over `ZMod 2` (the scalar word) and behind label
nesting (supports grow along every slot chain since `sg a, sg b ⊆ sg k`).
-/
namespace R6Chk.Bit
open R6Chk
/-! ## Gates -/
/-- `cnt` gate records `(k, a, b)` (16-bit fields). -/
def gatesChk (sg : ℕ → ℕ) (cnt : ℕ) : ℕ → Bool :=
Nat.rec (motive := fun _ => ℕ → Bool) (fun _ => true)
(fun _ ih s =>
let k := Nat.land s 65535
let a := Nat.land (Nat.shiftRight s 16) 65535
let b := Nat.land (Nat.shiftRight s 32) 65535
let sa := sg a
let sb := sg b
Nat.beq (Nat.land sa sb) 0 && Nat.beq (Nat.lor sa sb) (sg k) && ih (Nat.shiftRight s 48)) cnt
/-- Decoded gate records. -/
def gatesDec (cnt : ℕ) : ℕ → List (ℕ × ℕ × ℕ) :=
Nat.rec (motive := fun _ => ℕ → List (ℕ × ℕ × ℕ)) (fun _ => [])
(fun _ ih s => (Nat.land s 65535, Nat.land (Nat.shiftRight s 16) 65535,
Nat.land (Nat.shiftRight s 32) 65535) :: ih (Nat.shiftRight s 48)) cnt
def gchunkChk (sg : ℕ → ℕ) (x : ℕ) : Bool := gatesChk sg (Nat.land x 65535) (Nat.shiftRight x 16)
def gchunkDec (x : ℕ) : List (ℕ × ℕ × ℕ) := gatesDec (Nat.land x 65535) (Nat.shiftRight x 16)
/-- A gate is well formed: disjoint operands, union = result. -/
def GateOK (sg : ℕ → ℕ) (g : ℕ × ℕ × ℕ) : Prop :=
sg g.2.1 &&& sg g.2.2 = 0 ∧ sg g.2.1 ||| sg g.2.2 = sg g.1
/-! ## Outputs and retained totals -/
/-- `star c \ (star t₁ ∪ star t₂)`. -/
def exclT (c t1 t2 : ℕ) : ℕ := Nat.xor (star c) (Nat.land (star c) (Nat.lor (star t1) (star t2)))
def outsChk (sg : ℕ → ℕ) (cnt : ℕ) : ℕ → Bool :=
Nat.rec (motive := fun _ => ℕ → Bool) (fun _ => true)
(fun _ ih s =>
Nat.beq (sg (Nat.land (Nat.shiftRight s 24) 65535))
(exclT (Nat.land s 255) (Nat.land (Nat.shiftRight s 8) 255) (Nat.land (Nat.shiftRight s 16) 255))
&& ih (Nat.shiftRight s 40)) cnt
def outsDec (cnt : ℕ) : ℕ → List (ℕ × ℕ × ℕ × ℕ) :=
Nat.rec (motive := fun _ => ℕ → List (ℕ × ℕ × ℕ × ℕ)) (fun _ => [])
(fun _ ih s => (Nat.land s 255, Nat.land (Nat.shiftRight s 8) 255, Nat.land (Nat.shiftRight s 16) 255,
Nat.land (Nat.shiftRight s 24) 65535) :: ih (Nat.shiftRight s 40)) cnt
def ochunkChk (sg : ℕ → ℕ) (x : ℕ) : Bool := outsChk sg (Nat.land x 65535) (Nat.shiftRight x 16)
def ochunkDec (x : ℕ) : List (ℕ × ℕ × ℕ × ℕ) := outsDec (Nat.land x 65535) (Nat.shiftRight x 16)
def retsChk (sg : ℕ → ℕ) (cnt : ℕ) : ℕ → Bool :=
Nat.rec (motive := fun _ => ℕ → Bool) (fun _ => true)
(fun _ ih s => Nat.beq (sg (Nat.land (Nat.shiftRight s 8) 65535)) (star (Nat.land s 255))
&& ih (Nat.shiftRight s 24)) cnt
def retsDec (cnt : ℕ) : ℕ → List (ℕ × ℕ) :=
Nat.rec (motive := fun _ => ℕ → List (ℕ × ℕ)) (fun _ => [])
(fun _ ih s => (Nat.land s 255, Nat.land (Nat.shiftRight s 8) 65535) :: ih (Nat.shiftRight s 24)) cnt
def rchunkChk (sg : ℕ → ℕ) (x : ℕ) : Bool := retsChk sg (Nat.land x 65535) (Nat.shiftRight x 16)
def rchunkDec (x : ℕ) : List (ℕ × ℕ) := retsDec (Nat.land x 65535) (Nat.shiftRight x 16)
/-! ## Leaves -/
def leafChk (sg : ℕ → ℕ) : Bool :=
Nat.beq (sg 0) 0 && allN 1771 (fun i => Nat.beq (sg (Nat.add i 1)) (Nat.shiftLeft 1 i))
end R6Chk.Bit
end
section
-- Source module: Solutions.R6ChkCx
/-!
# Reflective checker for nested nondegenerate `F₂` label pairs (complex round six)
Data: a list of **groups**. A group is one natural number read as 32-bit fields (LSB first):
`kV, cnt, B (kV rows), H (n-kV), D (kV), E (n-kV)`, then `cnt` entries `kU, U (kU), EU (kU),
R (kV-kU)`. Rows are vectors of `F₂^n` (`n ≤ 24`).
* `grpChk n bad G : Bool` — two packed products for the label `V = span B`
(`H·[B;E]ᵀ = [0 | I]`, `D·[H;B]ᵀ = [0 | I]`) and two per entry
(`U·[H;EU]ᵀ = [0 | I]`, `R·[H;U;R]ᵀ = [0 | 0 | I]`), plus row range checks.
* `grpChk_sound`: if `grpChk n (BADf n) G = true` then `V` is nondegenerate of dimension `kV`,
and for every entry `(U, kU)`, `PairOK n U kU V kV`: `span U ≤ span V`, `dim span U = kU`,
`span U` nondegenerate, and `span U = span V` or some `w ∈ span V` has `w·w = 1`, `w ⊥ U`
(i.e. `NetComplexP8.Up (span U) (span V)` with `Fd = kV - kU`; see `R6ChkCxBridge`).
-/
namespace R6Chk
open Matrix Module
/-! ## Stream decoding -/
/-- The low 32-bit field. -/
def f32 (s : ℕ) : ℕ := Nat.land s 4294967295
/-- Drop one field. -/
def nx (s : ℕ) : ℕ := Nat.shiftRight s 32
/-- The low `k` fields. -/
def tk (s k : ℕ) : ℕ := Nat.land s (Nat.sub (Nat.shiftLeft 1 (Nat.mul 32 k)) 1)
/-- Drop `k` fields. -/
def dr (s k : ℕ) : ℕ := Nat.shiftRight s (Nat.mul 32 k)
/-- Concatenate `X` (`a` rows) and `Y`. -/
def cat (X a Y : ℕ) : ℕ := Nat.add X (Nat.shiftLeft Y (Nat.mul 32 a))
/-- All rows below `2^n` (with `bad = BADf n`). -/
def okR (bad X : ℕ) : Bool := Nat.beq (Nat.land X bad) 0
/-! ## The checker -/
/-- One entry: `U·[H;EU]ᵀ = [0|I]` and `R·[H;U;R]ᵀ = [0|0|I]`. -/
def entChk (bad kV nH H s : ℕ) : Bool :=
let kU := f32 s
let s1 := nx s
let U := tk s1 kU
let s2 := dr s1 kU
let EU := tk s2 kU
let s3 := dr s2 kU
let kR := Nat.sub kV kU
let R := tk s3 kR
Nat.ble kU kV && okR bad U && okR bad EU && okR bad R &&
Nat.beq (dotsF U (cat H nH EU)) (tgtF nH kU) &&
Nat.beq (dotsF R (cat (cat H nH U) (Nat.add nH kU) R)) (tgtF (Nat.add nH kU) kR)
/-- Skip one entry. -/
def entNext (kV s : ℕ) : ℕ := dr (nx s) (Nat.add (f32 s) kV)
/-- `cnt` entries. -/
def entsChk (bad kV nH H : ℕ) (cnt : ℕ) : ℕ → Bool :=
Nat.rec (motive := fun _ => ℕ → Bool) (fun _ => true)
(fun _ ih s => entChk bad kV nH H s && ih (entNext kV s)) cnt
/-- A group, after decoding. -/
def grpBody (n bad kV cnt B H D E s5 : ℕ) : Bool :=
let nH := Nat.sub n kV
Nat.ble kV n && okR bad B && okR bad H && okR bad D && okR bad E &&
Nat.beq (dotsF H (cat B kV E)) (tgtF kV nH) &&
Nat.beq (dotsF D (cat H nH B)) (tgtF nH kV) &&
entsChk bad kV nH H cnt s5
/-- A group. -/
def grpChk (n bad G : ℕ) : Bool :=
let kV := f32 G
let s0 := nx G
let cnt := f32 s0
let s1 := nx s0
let nH := Nat.sub n kV
let B := tk s1 kV
let s2 := dr s1 kV
let H := tk s2 nH
let s3 := dr s2 nH
let D := tk s3 kV
let s4 := dr s3 kV
let E := tk s4 nH
let s5 := dr s4 nH
grpBody n bad kV cnt B H D E s5
/-- `List.all`, as a plain `List.rec` (cheap kernel unfolding). -/
def allL {α : Type} (p : α → Bool) (l : List α) : Bool :=
List.rec (motive := fun _ => Bool) true (fun a _ ih => p a && ih) l
/-! ## Semantics -/
/-- Span of the first `k` rows of `X` in `F₂^n`. -/
def spanP (n X k : ℕ) : Submodule (ZMod 2) (Fin n → ZMod 2) := spanF (fun i : Fin k => vr n X i)
/-- What an edge `U → V` needs (`NetComplexP8.Up`, with dimensions). -/
def PairOK (n U kU V kV : ℕ) : Prop :=
spanP n U kU ≤ spanP n V kV ∧ finrank (ZMod 2) (spanP n U kU) = kU ∧
finrank (ZMod 2) (spanP n V kV) = kV ∧ NondegF (spanP n U kU) ∧ NondegF (spanP n V kV) ∧
(spanP n U kU = spanP n V kV ∨
∃ w ∈ spanP n V kV, w ⬝ᵥ w = 1 ∧ ∀ z ∈ spanP n U kU, z ⬝ᵥ w = 0)
/-- The label of a group: `(B, kV)`. -/
def grpV (n G : ℕ) : ℕ × ℕ := (tk (nx (nx G)) (f32 G), f32 G)
/-- The entries `(U, kU)` of a stream. -/
def entsDec (kV : ℕ) (cnt : ℕ) : ℕ → List (ℕ × ℕ) :=
Nat.rec (motive := fun _ => ℕ → List (ℕ × ℕ)) (fun _ => [])
(fun _ ih s => (tk (nx s) (f32 s), f32 s) :: ih (entNext kV s)) cnt
/-- The entries of a group. -/
def grpEnts (n G : ℕ) : List (ℕ × ℕ) :=
entsDec (f32 G) (f32 (nx G))
(dr (dr (dr (dr (nx (nx G)) (f32 G)) (Nat.sub n (f32 G))) (f32 G)) (Nat.sub n (f32 G)))
/-! ## Soundness -/
end R6Chk
end
Source
S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean modules Solutions/R6ChkPack.lean, Solutions/R6ChkF2.lean, Solutions/R6ChkConst.lean, Solutions/R6ChkBitBase.lean, Solutions/R6ChkBitDag.lean, Solutions/R6ChkCx.lean.