def and_all1

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/uint64n.bend:268

import Base

268def and_all1(+n: Nat, +w: Word(n)) -> {Word.and(n, w, all1(n)) == w : Word(n)}:
269  match n w:
270    case 0n WNil{}:
271      {==}
272    case 1n+p WCon{+x, +t}:
273      %Equal.sym(Bool, Bool.and(x, True{}), x, and_true(x)) : {WCon{_, Word.and(p, t, all1(p))} == WCon{x, t} : Word(1n+p)}
274      Equal.cong(Word(p), Word(1n+p), z => WCon{x, z}, Word.and(p, t, all1(p)), t, and_all1(p, t))