def bitw.fls_zero

bend-osdev-algo@0.1.0.0 · PROOF.bend:360

import Base
import bend-osdev-algo@0.1.0.0/algo.bend as A

360def bitw.fls_zero(n: Nat, w: Word(n), e: {A.bitw.fls(n, w) == 0n : Nat}) -> {w == Word.zero(n) : Word(n)}:
361  match n:
362    case 0n:
363      match w:
364        case WNil{}:
365          {==}
366    case 1n+ +p:
367      match w:
368        case WCon{+b, +t}:
369          +e2 = e
370          %bitw.fls_zero(p, t, bitw.fls_zero.m(A.bitw.fls(p, t), b, e2)) : {WCon{b, t} == WCon{False{}, _} : Word(1n+p)}
371          %bitw.fls_zero.b(A.bitw.fls(p, t), b, e2) : {WCon{b, t} == WCon{_, t} : Word(1n+p)}
372          {==}