def shl_adc

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32alg.bend:246

import Base

246# Doubling by shifting: shl.put n c w == w + w + c.
247def shl_adc(+n: Nat, +w: Word(n), +c: Bool) -> {Word.shl.put(n, c, w) == Word.adc(n, w, w, False{}, c) : Word(n)}:
248  match n:
249    case 0n:
250      match w:
251        case WNil{}:
252          {==}
253    case 1n+p:
254      match w:
255        case WCon{True{}, t}:
256          match c:
257            case True{}:
258              Equal.cong(Word(p), Word(1n+p), x => WCon{True{}, x}, Word.shl.put(p, True{}, t), Word.adc(p, t, t, False{}, True{}), shl_adc(p, t, True{}))
259            case False{}:
260              Equal.cong(Word(p), Word(1n+p), x => WCon{False{}, x}, Word.shl.put(p, True{}, t), Word.adc(p, t, t, False{}, True{}), shl_adc(p, t, True{}))
261        case WCon{False{}, t}:
262          match c:
263            case True{}:
264              Equal.cong(Word(p), Word(1n+p), x => WCon{True{}, x}, Word.shl.put(p, False{}, t), Word.adc(p, t, t, False{}, False{}), shl_adc(p, t, False{}))
265            case False{}:
266              Equal.cong(Word(p), Word(1n+p), x => WCon{False{}, x}, Word.shl.put(p, False{}, t), Word.adc(p, t, t, False{}, False{}), shl_adc(p, t, False{}))