def h.and_z

bend-kit-collections@0.1.4.1 · PROOF.bend:1848

import Base
import bend-mathlib@0.7.4.0/bool.bend as MBool

1848def h.and_z(+n: Nat, x: Word(n), m: Word(n), e: {h.isz(n, m) == True{} : Bool})
1849  -> {Word.and(n, x, m) == Word.zero(n) : Word(n)}:
1850  match n:
1851    case 0n:
1852      match x m:
1853        case WNil{} WNil{}:
1854          {==}
1855    case 1n+p:
1856      match x m:
1857        case WCon{+a, +xt} WCon{True{}, +mt}:
1858          Empty.absurd({Word.and(1n+p, WCon{a, xt}, WCon{True{}, mt}) == Word.zero(1n+p) : Word(1n+p)}, MBool.false_ne_true()(e))
1859        case WCon{True{}, +xt} WCon{False{}, +mt}:
1860          Equal.cong(Word(p), Word(1n+p), w => WCon{False{}, w}, Word.and(p, xt, mt), Word.zero(p),
1861            h.and_z(p, xt, mt, e))
1862        case WCon{False{}, +xt} WCon{False{}, +mt}:
1863          Equal.cong(Word(p), Word(1n+p), w => WCon{False{}, w}, Word.and(p, xt, mt), Word.zero(p),
1864            h.and_z(p, xt, mt, e))