def pk.wself

bend-osdev-pkcs7@0.1.0.0 · PROOF.bend:210

import Base

210# a word XOR itself is zero, bit by bit
211def pk.wself(+n: Nat, w: Word(n)) -> {Word.xor(n, w, w) == Word.zero(n) : Word(n)}:
212  match n:
213    case 0n:
214      match w:
215        case WNil{}:
216          {==}
217    case 1n+p:
218      match w:
219        case WCon{h, t}:
220          match h:
221            case False{}:
222              %pk.wself(p, t) : {WCon{False{}, Word.xor(p, t, t)} == WCon{False{}, _} : Word(1n+p)}
223              {==}
224            case True{}:
225              %pk.wself(p, t) : {WCon{False{}, Word.xor(p, t, t)} == WCon{False{}, _} : Word(1n+p)}
226              {==}