def word_and_zero

bend-osdev-gf@0.1.1.0 · PROOF.bend:6457

import Base

6457def word_and_zero(+n: Nat, +r: Word(n)) -> {Word.and(n, Word.zero(n), r) == Word.zero(n) : Word(n)}:
6458  match n:
6459    case 0n:
6460      {==}
6461    case 1n+p:
6462      match r:
6463        case WCon{+x, +rt}:
6464          %word_and_zero(p, rt) : {WCon{False{}, Word.and(p, Word.zero(p), rt)} == WCon{False{}, _} : Word(1n+p)}
6465          {==}