def un.so

bend-osdev-u32@0.1.0.0 · PROOF.bend:1487

import Base

1487# Word.shl.out is the bit going out and the shifted word
1488def un.so(n: Nat, +c: Bool, +w: Word(n)) -> {Word.shl.out(n, c, w) == (un.topc(n, c, w), Word.shl.put(n, c, w)) : Bool & Word(n)}:
1489  match n:
1490    case 0n:
1491      {==}
1492    case 1n+ +p:
1493      match w:
1494        case WCon{+x, +t}:
1495          %Equal.sym(Bool & Word(p), Word.shl.out(p, x, t), (un.topc(p, x, t), Word.shl.put(p, x, t)), un.so(p, x, t)) : {Word.shl.out.con(p, c, _) == (un.topc(p, x, t), WCon{c, Word.shl.put(p, x, t)}) : Bool & Word(1n+p)}
1496          {==}