def not_join

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/word.bend:174

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W

174def not_join(+n: Nat, +m: Nat, +a: Word(n), +b: Word(m)) -> {Word.not(Nat.add(n, m), W.join(n, m, a, b)) == W.join(n, m, Word.not(n, a), Word.not(m, b)) : Word(Nat.add(n, m))}:
175  match n a:
176    case 0n WNil{}:
177      {==}
178    case 1n+p WCon{x, t}:
179      Equal.cong(Word(Nat.add(p, m)), Word(1n+Nat.add(p, m)), w => WCon{Bool.not(x), w}, Word.not(Nat.add(p, m), W.join(p, m, t, b)), W.join(p, m, Word.not(p, t), Word.not(m, b)), not_join(p, m, t, b))