~/jendhub

def wd.flip

bend-osdev-u32@0.1.0.0 · PROOF_order.bend:224

import bend-osdev-u32@0.1.0.0/PROOF_order.bend as PROOFOrder
import Base

224def wd.flip(n: Nat, a: Word(n), b: Word(n)) -> {Word.cmp(n, b, a) == cm.flip(Word.cmp(n, a, b)) : Cmp}:
225  match n:
226    case 0n:
227      {==}
228    case 1n+ +p:
229      match a b:
230        case WCon{+x, +at} WCon{+y, +bt}:
231          %Equal.sym(Cmp, Word.cmp(p, bt, at), cm.flip(Word.cmp(p, at, bt)), wd.flip(p, at, bt)) : {Word.cmp.fin(y, x, _) == cm.flip(Word.cmp.fin(x, y, Word.cmp(p, at, bt))) : Cmp}
232          wd.fin_flip(Word.cmp(p, at, bt), x, y)

Uses (9)

Used by (1)