def rhd.c1a.k

bend-kit-collections@0.1.4.1 · nat_order.bend:582

import Base

582def rhd.c1a.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, b), y), h1: LE(Nat.add(y, x), Nat.mul(3n, b))) -> Empty:
583  +v = {VS{l, x, y, b} : Vs}
584  +f_ng = cvle(1n+Nat.mul(3n, b), y, L{1n, 0n, 0n, 0n, 3n}, L{0n, 0n, 0n, 1n, 0n}, v,
585    cv_add(1n, Nat.mul(3n, b), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v, cv_c(1n, v), cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b))),
586    cv_3(l, x, y, b), ng)
587  +f_h1 = cvle(Nat.add(y, x), Nat.mul(3n, b), L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v,
588    cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b)),
589    cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)), h1)
590  contra(L{1n, 0n, 1n, 1n, 3n}, L{0n, 0n, 0n, 1n, 3n}, v,
591    comb(L{1n, 0n, 0n, 0n, 3n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v, f_ng,
592    f_h1), {==})