def cmp_join

bend-collections-laws-crypto@1.0.0.0 · proofs/math/u64/u64.bend:43

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as U
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W

43# Comparing two joined words is comparing the high parts, then the low parts.
44def cmp_join(+n: Nat, +m: Nat, +a1: Word(n), +b1: Word(m), +a2: Word(n), +b2: Word(m)) -> {Word.cmp(Nat.add(n, m), W.join(n, m, a1, b1), W.join(n, m, a2, b2)) == U.order(Word.cmp(m, b1, b2), Word.cmp(n, a1, a2)) : Cmp}:
45  match n a1 a2:
46    case 0n WNil{} WNil{}:
47      Equal.sym(Cmp, U.order(Word.cmp(m, b1, b2), EQ{}), Word.cmp(m, b1, b2), order_eq(Word.cmp(m, b1, b2)))
48    case 1n+p WCon{x, t1} WCon{y, t2}:
49      %Equal.sym(Cmp, Word.cmp(Nat.add(p, m), W.join(p, m, t1, b1), W.join(p, m, t2, b2)), U.order(Word.cmp(m, b1, b2), Word.cmp(p, t1, t2)), cmp_join(p, m, t1, b1, t2, b2)) : {Word.cmp.fin(x, y, _) == U.order(Word.cmp(m, b1, b2), Word.cmp.fin(x, y, Word.cmp(p, t1, t2))) : Cmp}
50      fin_order(x, y, Word.cmp(m, b1, b2), Word.cmp(p, t1, t2))