Enum FloorWindowFigure 

pub enum FloorWindowFigure {
    PowPositive {
        pow_fn: String,
    },
    PowSumSplit {
        pow_fn: String,
    },
    SigWindow {
        pow_fn: String,
        halve_fn: String,
        exp_fn: String,
        sig_fn: String,
        window_fn: String,
    },
    ProductWindow {
        pow_fn: String,
        fits_fn: String,
        claim_fn: String,
    },
    FloorPow2Window {
        pow_fn: String,
        floor_fn: String,
        window_fn: String,
    },
    FloorPow2Cancel {
        pow_fn: String,
        floor_fn: String,
        cancel_fn: String,
    },
}

The recognized figures of ProofStrategy::FloorDivWindow. All fn names are source names; backends translate. Every figure’s quantifier names come from the law’s givens (captured implicitly — backends render them through the law’s own given list).

Variants

PowPositive

pow(n) >= 1 => true with no premise — positivity of the power-of-two fn, by functional induction.

Fields

pow_fn: String

PowSumSplit

when m >= 0; n >= 0 -> pow(m + n) == pow(m) * pow(n) — the power homomorphism, by functional induction on the first exponent.

Fields

pow_fn: String

SigWindow

when b >= 1; a >= b; n >= 1 -> window(a, b, n) == true where window checks pow(n-1) <= sig(a,b,n) < pow(n), sig scales by pow(n-1-e) and floor-divides, and e is the floor-halving binary exponent of a/b.

Fields

pow_fn: String

halve_fn: String

exp_fn: String

sig_fn: String

window_fn: String

ProductWindow

when fits(j, m); fits(k, n) -> claim(j, k, m, n) == true where fits is the pow(m-1) <= j < pow(m) window predicate and claim states the product window pow(m+n-2) <= j*k < pow(m+n).

Fields

pow_fn: String

fits_fn: String

claim_fn: String

FloorPow2Window

The recursive-expo-FREE Euclidean floor window over a power-of-two divisor: window(args) == true (no premise) where window’s body is pow(E) * floor(N, pow(E)) <= N && N < pow(E) * (floor(N, pow(E)) + 1) for ARBITRARY numerator expression N and exponent expression E over the law’s givens, floor the Result.withDefault( Int.div(a, d), 0) Euclidean-floor wrapper, and pow any [is_pow2_shape] fn. Unlike [SigWindow] there is NO binary- exponent recursion — the divisor is pow(E) directly — so the figure is generic over N/E (a bare-given floorDivWindow(a, k) and a compound truncFitsWindow(f, i) both match). Closed by the core Int.ediv_add_emod / Int.emod_nonneg / Int.emod_lt_of_pos bridge plus power-of-two positivity, generic over the inferred N/pow(E). pow_fn/floor_fn are the (possibly module-qualified) dotted call names; window_fn is the law’s subject predicate.

Fields

pow_fn: String

floor_fn: String

window_fn: String

FloorPow2Cancel

The exact-division cancel sibling of [FloorPow2Window]: the EQUATIONAL fact that flooring a manifest multiple of a power of two by that power is exact. The law claim is floor(s * pow(b), pow(a)) == s * pow(b - a) with premise 0 <= a && a <= b — the divisor pow(a) divides the dividend s * pow(b) because pow(a) | pow(b) when a <= b (the power-of-two homomorphism pow(b) = pow(a) * pow(b - a)), so the Euclidean floor returns the exact quotient s * pow(b - a). Generic over the integer s and the two exponents a/b — “the exact cancel works for any provably-dividing floorDiv”. Closed by the homomorphism split plus Int.mul_ediv_cancel_left (core, no Mathlib), the same power algebra every floor-window figure proves. pow_fn/floor_fn are the (possibly module-qualified) dotted call names; cancel_fn is the law’s subject (the floor wrapper itself), so the lemma sits in the call cone of any rounding-composition law and the keystone cites it by name. Demonstrated by Lemmas 7.2.10 / 7.2.11 of the K5 division proof (projects/k5_fdiv/domain/round.av).

Fields

pow_fn: String

floor_fn: String

cancel_fn: String

Trait Implementations

impl Clone for FloorWindowFigure

fn clone(&self) -> FloorWindowFigure

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for FloorWindowFigure

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for FloorWindowFigure

impl PartialEq for FloorWindowFigure

fn eq(&self, other: &FloorWindowFigure) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for FloorWindowFigure