def inc_join

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

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

196# incrementing a joined word carries into the high part iff the low part is all ones
197def inc_join(+n: Nat, +m: Nat, +a: Word(n), +b: Word(m)) -> {Word.inc(Nat.add(n, m), W.join(n, m, a, b)) == W.join(n, m, Word.inc(n, a), incif(m, ones(n, a), b)) : Word(Nat.add(n, m))}:
198  match n a:
199    case 0n WNil{}:
200      {==}
201    case 1n+p WCon{False{}, t}:
202      {==}
203    case 1n+p WCon{True{}, t}:
204      Equal.cong(Word(Nat.add(p, m)), Word(1n+Nat.add(p, m)), w => WCon{False{}, w}, Word.inc(Nat.add(p, m), W.join(p, m, t, b)), W.join(p, m, Word.inc(p, t), incif(m, ones(p, t), b)), inc_join(p, m, t, b))