def bx.wself

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1590

import Base

1590def bx.wself(n: Nat, w: Word(n)) -> {Word.xor(n, w, w) == Word.zero(n) : Word(n)}:
1591  match n:
1592    case 0n:
1593      match w:
1594        case WNil{}:
1595          {==}
1596    case 1n+p:
1597      match w:
1598        case WCon{h, t}:
1599          match h:
1600            case False{}:
1601              %bx.wself(p, t) : {WCon{False{}, Word.xor(p, t, t)} == WCon{False{}, _} : Word(1n+p)}
1602              {==}
1603            case True{}:
1604              %bx.wself(p, t) : {WCon{False{}, Word.xor(p, t, t)} == WCon{False{}, _} : Word(1n+p)}
1605              {==}