def AP.and_zero

bend-osdev-array@0.1.0.1 · PROOF.bend:875

import Base

875def AP.and_zero(n: Nat, w: Word(n)) -> {Word.and(n, w, Word.zero(n)) == Word.zero(n) : Word(n)}:
876  match n:
877    case 0n:
878      {==}
879    case 1n+ +q:
880      match w:
881        case WCon{False{}, t}:
882          AP.wcon_cong(q, False{}, Word.and(q, t, Word.zero(q)), Word.zero(q), AP.and_zero(q, t))
883        case WCon{True{}, t}:
884          AP.wcon_cong(q, False{}, Word.and(q, t, Word.zero(q)), Word.zero(q), AP.and_zero(q, t))