def bitw.ffs_zero

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

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

273def bitw.ffs_zero(n: Nat, w: Word(n), e: {A.bitw.ffs(n, w) == 0n : Nat}) -> {w == Word.zero(n) : Word(n)}:
274  match n:
275    case 0n:
276      match w:
277        case WNil{}:
278          {==}
279    case 1n+ +p:
280      match w:
281        case WCon{True{}, t}:
282          Empty.absurd({WCon{True{}, t} == Word.zero(1n+p) : Word(1n+p)}, absurd.sz(0n, e))
283        case WCon{False{}, +t}:
284          %bitw.ffs_zero(p, t, bitw.ffs_zero.h(A.bitw.ffs(p, t), e)) : {WCon{False{}, t} == WCon{False{}, _} : Word(1n+p)}
285          {==}