def word_xx2

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:8575

import Base

8575def word_xx2(n: Nat, a: Word(n), b: Word(n)) -> {b == Word.xor(n, a, Word.xor(n, a, b)) : Word(n)}:
8576  match n:
8577    case 0n:
8578      match a b:
8579        case WNil{} WNil{}:
8580          {==}
8581    case 1n+p:
8582      match a b:
8583        case WCon{ah, at} WCon{bh, bt}:
8584          %bool_xx2(ah, bh) : {WCon{bh, bt} == WCon{_, Word.xor(p, at, Word.xor(p, at, bt))} : Word(1n+p)}
8585          %word_xx2(p, at, bt) : {WCon{bh, bt} == WCon{bh, _} : Word(1n+p)}
8586          {==}