def nearlo.c0b.k

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

import Base

784def nearlo.c0b.k(+a: Nat, +a2: Nat, +c: Nat, ng: LE(1n+1n+Nat.add(a, c), Nat.add(a2, c)), n2: LE(a2, 1n+a)) -> Empty:
785  +v = {VS{a, a2, c, 0n} : Vs}
786  +f_ng = cvle(1n+1n+Nat.add(a, c), Nat.add(a2, c), L{2n, 1n, 0n, 1n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v,
787    cv_add(1n, 1n+Nat.add(a, c), L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_add(1n, Nat.add(a, c), L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_add(a, c, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_1(a, a2, c, 0n), cv_3(a, a2, c, 0n)))),
788    cv_add(a2, c, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(a, a2, c, 0n), cv_3(a, a2, c, 0n)), ng)
789  +f_n2 = cvle(a2, 1n+a, L{0n, 0n, 1n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v,
790    cv_2(a, a2, c, 0n),
791    cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(a, a2, c, 0n)), n2)
792  contra(L{2n, 1n, 1n, 1n, 0n}, L{1n, 1n, 1n, 1n, 0n}, v,
793    comb(L{2n, 1n, 0n, 1n, 0n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, f_ng,
794    f_n2), {==})