~/bend-docscommunity

int_filled.bend checks

raw source on the hub · import 0xd5e9362591c1667c9894b781190e1ac9/int_filled.bend as Int_filled

3 imports
import Base
import ./nat.bend as N
import ./int.bend as C

Definitions

def Int.neg_nat source · line 15 · raw

@n:Nat -> 0xd5e9362591c1667c9894b781190e1ac9/int.Int

-n, as an Int (the only place the two zeros have to be reconciled)

def Int.sub_nat source · line 23 · raw

@a:Nat -> @b:Nat -> 0xd5e9362591c1667c9894b781190e1ac9/int.Int

a - b for Nats, as an Int

def Int.sub_nat_self source · line 118 · raw

@n:Nat -> {Int.sub_nat(n, n) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{0n} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

n - n = 0

def Int.toP source · line 249 · raw

@a:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> Nat

def Int.toM source · line 256 · raw

@a:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> Nat

def Int.sub_nat_zero source · line 263 · raw

@x:Nat -> {Int.sub_nat(x, 0n) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{x} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def Int.sub_nat_zero_l source · line 270 · raw

@x:Nat -> {Int.sub_nat(0n, x) == Int.neg_nat(x) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def Int.split source · line 277 · raw

@a:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {Int.sub_nat(Int.toP(a), Int.toM(a)) == a : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def Int.by1 source · line 284 · raw

@-P:(@_:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> Type) -> @+a:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @w:P(Int.sub_nat(Int.toP(a), Int.toM(a))) -> P(a)

def Int.by2 source · line 288 · raw

@-P:(@_:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @_:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> Type) -> @+a:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+b:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @w:P(Int.sub_nat(Int.toP(a), Int.toM(a)), Int.sub_nat(Int.toP(b), Int.toM(b))) -> P(a, b)

def Int.by3 source · line 293 · raw

@-P:(@_:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @_:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @_:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> Type) -> @+a:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+b:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+c:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @w:P(Int.sub_nat(Int.toP(a), Int.toM(a)), Int.sub_nat(Int.toP(b), Int.toM(b)), Int.sub_nat(Int.toP(c), Int.toM(c))) -> P(a, b, c)

def Int.add_pos source · line 300 · raw

@+x:Nat -> @q:Nat -> @n:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Pos{x}, Int.sub_nat(q, n)) == Int.sub_nat(Nat.add(x, q), n) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

p + (q - n) = (p + q) - n

def Int.add_negs source · line 314 · raw

@+m:Nat -> @q:Nat -> @n:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.NegS{m}, Int.sub_nat(q, n)) == Int.sub_nat(q, 1n+Nat.add(m, n)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

-(1+m) + (q - n) = q - (1 + m + n)

def Int.add_sub source · line 330 · raw

@p:Nat -> @m:Nat -> @+q:Nat -> @+n:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(Int.sub_nat(p, m), Int.sub_nat(q, n)) == Int.sub_nat(Nat.add(p, q), Nat.add(m, n)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

(p - m) + (q - n) = (p + q) - (m + n)

def Int.add_assoc.core source · line 341 · raw

@+p1:Nat -> @+m1:Nat -> @+p2:Nat -> @+m2:Nat -> @+p3:Nat -> @+m3:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(Int.sub_nat(p1, m1), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(Int.sub_nat(p2, m2), Int.sub_nat(p3, m3))) == 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(Int.sub_nat(p1, m1), Int.sub_nat(p2, m2)), Int.sub_nat(p3, m3)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def Int.sub_nat_cancel source · line 355 · raw

@k:Nat -> @-u:Nat -> @-v:Nat -> {Int.sub_nat(Nat.add(k, u), Nat.add(k, v)) == Int.sub_nat(u, v) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

(k+u) - (k+v) = u - v

def Int.mul_pos source · line 363 · raw

@+x:Nat -> @q:Nat -> @n:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Pos{x}, Int.sub_nat(q, n)) == Int.sub_nat(Nat.mul(x, q), Nat.mul(x, n)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

x * (q - n) = xq - xn

def Int.mul_negs source · line 382 · raw

@+m:Nat -> @q:Nat -> @n:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.NegS{m}, Int.sub_nat(q, n)) == Int.sub_nat(Nat.mul(1n+m, n), Nat.mul(1n+m, q)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

-(1+m) * (q - n) = (1+m)n - (1+m)q

def Int.mul_add.core source · line 400 · raw

@a:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+p2:Nat -> @+m2:Nat -> @+p3:Nat -> @+m3:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(a, 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(Int.sub_nat(p2, m2), Int.sub_nat(p3, m3))) == 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(a, Int.sub_nat(p2, m2)), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(a, Int.sub_nat(p3, m3))) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def Int.le_cast source · line 433 · raw

@-x:Nat -> @-y:Nat -> @-c:Nat -> @e:{x == y : Nat} -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(x, c) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(y, c)

def Int.le_cast_r source · line 437 · raw

@-x:Nat -> @-y:Nat -> @-c:Nat -> @e:{x == y : Nat} -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(c, x) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(c, y)

def Int.le_succ_zero source · line 441 · raw

@-k:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(1n+k, 0n) -> Empty

def Int.neg_sub source · line 444 · raw

@p:Nat -> @m:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.neg(Int.sub_nat(p, m)) == Int.sub_nat(m, p) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def Int.le_pos_f source · line 455 · raw

@+x:Nat -> @q:Nat -> @n:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/int.Int.Le(0xd5e9362591c1667c9894b781190e1ac9/int.Pos{x}, Int.sub_nat(q, n)) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(Nat.add(x, n), q)

def Int.le_negs_f source · line 469 · raw

@+m:Nat -> @q:Nat -> @n:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/int.Int.Le(0xd5e9362591c1667c9894b781190e1ac9/int.NegS{m}, Int.sub_nat(q, n)) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(n, Nat.add(q, 1n+m))

def Int.le_f source · line 480 · raw

@p:Nat -> @m:Nat -> @+q:Nat -> @+n:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/int.Int.Le(Int.sub_nat(p, m), Int.sub_nat(q, n)) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(Nat.add(p, n), Nat.add(q, m))

def Int.le_pos_b source · line 494 · raw

@+x:Nat -> @q:Nat -> @n:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(Nat.add(x, n), q) -> 0xd5e9362591c1667c9894b781190e1ac9/int.Int.Le(0xd5e9362591c1667c9894b781190e1ac9/int.Pos{x}, Int.sub_nat(q, n))

def Int.le_negs_b source · line 507 · raw

@+m:Nat -> @q:Nat -> @n:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(n, Nat.add(q, 1n+m)) -> 0xd5e9362591c1667c9894b781190e1ac9/int.Int.Le(0xd5e9362591c1667c9894b781190e1ac9/int.NegS{m}, Int.sub_nat(q, n))

def Int.le_b source · line 518 · raw

@p:Nat -> @m:Nat -> @+q:Nat -> @+n:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(Nat.add(p, n), Nat.add(q, m)) -> 0xd5e9362591c1667c9894b781190e1ac9/int.Int.Le(Int.sub_nat(p, m), Int.sub_nat(q, n))

def Int.le_split source · line 529 · raw

@+a:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+b:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @h:0xd5e9362591c1667c9894b781190e1ac9/int.Int.Le(a, b) -> 0xd5e9362591c1667c9894b781190e1ac9/int.Int.Le(Int.sub_nat(Int.toP(a), Int.toM(a)), Int.sub_nat(Int.toP(b), Int.toM(b)))

def Int.le_neg.core source · line 534 · raw

@+pa:Nat -> @+ma:Nat -> @+pb:Nat -> @+mb:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(Nat.add(pa, mb), Nat.add(pb, ma)) -> 0xd5e9362591c1667c9894b781190e1ac9/int.Int.Le(0xd5e9362591c1667c9894b781190e1ac9/int.Int.neg(Int.sub_nat(pb, mb)), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.neg(Int.sub_nat(pa, ma)))

def Int.le_add.core source · line 546 · raw

@+pa:Nat -> @+ma:Nat -> @+pb:Nat -> @+mb:Nat -> @+pc:Nat -> @+mc:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(Nat.add(pa, mb), Nat.add(pb, ma)) -> 0xd5e9362591c1667c9894b781190e1ac9/int.Int.Le(0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(Int.sub_nat(pa, ma), Int.sub_nat(pc, mc)), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.add(Int.sub_nat(pb, mb), Int.sub_nat(pc, mc)))

def Int.le_mul_r source · line 560 · raw

@x:Nat -> @y:Nat -> @+c:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(x, y) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(Nat.mul(x, c), Nat.mul(y, c))

x <= y gives xc <= yc

def Int.mul_sub_r source · line 572 · raw

@+p:Nat -> @+m:Nat -> @+k:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(Int.sub_nat(p, m), 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{k}) == Int.sub_nat(Nat.mul(p, k), Nat.mul(m, k)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

(p - m) * k = pk - mk

def Int.le_mul.core source · line 579 · raw

@+pa:Nat -> @+ma:Nat -> @+pb:Nat -> @+mb:Nat -> @+k:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(Nat.add(pa, mb), Nat.add(pb, ma)) -> 0xd5e9362591c1667c9894b781190e1ac9/int.Int.Le(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(Int.sub_nat(pa, ma), 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{k}), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(Int.sub_nat(pb, mb), 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{k}))

def Int.sgn source · line 594 · raw

@s:Bool -> @k:Nat -> 0xd5e9362591c1667c9894b781190e1ac9/int.Int

def Int.sign source · line 601 · raw

@a:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> Bool

def Int.sgn_split source · line 608 · raw

@a:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {Int.sgn(Int.sign(a), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.abs(a)) == a : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def Int.mul_pos_neg source · line 615 · raw

@+k:Nat -> @j:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Pos{k}, Int.neg_nat(j)) == Int.neg_nat(Nat.mul(k, j)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def Int.mul_neg_pos source · line 623 · raw

@k:Nat -> @+j:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(Int.neg_nat(k), 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{j}) == Int.neg_nat(Nat.mul(k, j)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def Int.mul_neg_neg source · line 630 · raw

@k:Nat -> @j:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(Int.neg_nat(k), Int.neg_nat(j)) == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{Nat.mul(k, j)} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def Int.mul_sgn source · line 642 · raw

@s:Bool -> @t:Bool -> @+k:Nat -> @+j:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(Int.sgn(s, k), Int.sgn(t, j)) == Int.sgn(0xd5e9362591c1667c9894b781190e1ac9/nat.Bool.same(s, t), Nat.mul(k, j)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def Int.same_assoc source · line 653 · raw

@a:Bool -> @b:Bool -> @c:Bool -> {0xd5e9362591c1667c9894b781190e1ac9/nat.Bool.same(a, 0xd5e9362591c1667c9894b781190e1ac9/nat.Bool.same(b, c)) == 0xd5e9362591c1667c9894b781190e1ac9/nat.Bool.same(0xd5e9362591c1667c9894b781190e1ac9/nat.Bool.same(a, b), c) : Bool}

def Int.sby3 source · line 672 · raw

@-P:(@_:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @_:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @_:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> Type) -> @+a:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+b:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @+c:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @w:P(Int.sgn(Int.sign(a), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.abs(a)), Int.sgn(Int.sign(b), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.abs(b)), Int.sgn(Int.sign(c), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.abs(c))) -> P(a, b, c)

def Int.mul_assoc.core source · line 678 · raw

@+sa:Bool -> @+ka:Nat -> @+sb:Bool -> @+kb:Nat -> @+sc:Bool -> @+kc:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(Int.sgn(sa, ka), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(Int.sgn(sb, kb), Int.sgn(sc, kc))) == 0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(Int.sgn(sa, ka), Int.sgn(sb, kb)), Int.sgn(sc, kc)) : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def Int.abs_neg_nat source · line 693 · raw

@k:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.abs(Int.neg_nat(k)) == k : Nat}

def Int.abs_mul source · line 700 · raw

@a:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @b:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> {0xd5e9362591c1667c9894b781190e1ac9/int.Int.abs(0xd5e9362591c1667c9894b781190e1ac9/int.Int.mul(a, b)) == Nat.mul(0xd5e9362591c1667c9894b781190e1ac9/int.Int.abs(a), 0xd5e9362591c1667c9894b781190e1ac9/int.Int.abs(b)) : Nat}

def Int.abs_zero source · line 711 · raw

@a:0xd5e9362591c1667c9894b781190e1ac9/int.Int -> @e:{0xd5e9362591c1667c9894b781190e1ac9/int.Int.abs(a) == 0n : Nat} -> {a == 0xd5e9362591c1667c9894b781190e1ac9/int.Pos{0n} : 0xd5e9362591c1667c9894b781190e1ac9/int.Int}

def Int.mul_eq_zero_nat source · line 719 · raw

@x:Nat -> @+y:Nat -> @e:{Nat.mul(x, y) == 0n : Nat} -> @nx:(@_:{x == 0n : Nat} -> Empty) -> {y == 0n : Nat}