bend-ml-nat-lemmas

Releases (3):
  0.1.2.0  0x09966385f3a8541fb22fd49450cdf477  indexed  https://jend.leeeet.dev/files.txt?path=bend-ml-nat-lemmas@0.1.2.0
  0.1.1.0  0x2bbe4207657ea8b1158567d930651411  unindexed  https://jend.leeeet.dev/files.txt?path=bend-ml-nat-lemmas@0.1.1.0
  0.1.0.0  0xa7aa06c09e97c6747c12cc64bb5203d9  unindexed  https://jend.leeeet.dev/files.txt?path=bend-ml-nat-lemmas@0.1.0.0

Definitions (19):
  BendMlNatLemmas.product (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=product)
   # Product of the elements of a list of Nat; the empty list is 1.
   # It is the "number of elements" of a tensor whose shape is the list.
   def product(xs: List<&2, Nat>) -> Nat:
  BendMlNatLemmas.add_zero (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=add_zero)
   law add_zero:
     for a: Nat
     {Nat.add(a, 0n) == a : Nat}
  BendMlNatLemmas.add_succ (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=add_succ)
   law add_succ:
     for  a: Nat
     for -b: Nat
     {1n+Nat.add(a, b) == Nat.add(a, 1n+b) : Nat}
  BendMlNatLemmas.add_comm (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=add_comm)
   law add_comm:
     for  a: Nat
     for +b: Nat
     {Nat.add(a, b) == Nat.add(b, a) : Nat}
  BendMlNatLemmas.add_assoc (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=add_assoc)
   law add_assoc:
     for  a: Nat
     for -b: Nat
     for -c: Nat
     {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
  BendMlNatLemmas.mul_zero (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=mul_zero)
   law mul_zero:
     for a: Nat
     {Nat.mul(a, 0n) == 0n : Nat}
  BendMlNatLemmas.add_swap (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=add_swap)
   # x + (y + z) == y + (x + z): swaps the middle terms of a triple sum.
   # (Auxiliary lemma; not a published law.)
   def add_swap(x: Nat, +y: Nat, +z: Nat) -> {Nat.add(x, Nat.add(y, z)) == Nat.add(y, Nat.add(x, z)) : Nat}:
  BendMlNatLemmas.mul_succ (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=mul_succ)
   law mul_succ:
     for +a: Nat
     for +b: Nat
     {Nat.mul(a, 1n+b) == Nat.add(a, Nat.mul(a, b)) : Nat}
  BendMlNatLemmas.mul_comm (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=mul_comm)
   law mul_comm:
     for +a: Nat
     for +b: Nat
     {Nat.mul(a, b) == Nat.mul(b, a) : Nat}
  BendMlNatLemmas.mul_dist (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=mul_dist)
   law mul_dist:
     for  a: Nat
     for -b: Nat
     for +c: Nat
     {Nat.add(Nat.mul(a, c), Nat.mul(b, c)) == Nat.mul(Nat.add(a, b), c) : Nat}
  BendMlNatLemmas.mul_assoc (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=mul_assoc)
   law mul_assoc:
     for +a: Nat
     for +b: Nat
     for +c: Nat
     {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(Nat.mul(a, b), c) : Nat}
  BendMlNatLemmas.add4 (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=add4)
   law add4:
     for +a: Nat
     for +b: Nat
     for +c: Nat
     for +d: Nat
     {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
  BendMlNatLemmas.mul_dist_l (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=mul_dist_l)
   law mul_dist_l:
     for +k: Nat
     for +a: Nat
     for +b: Nat
     {Nat.mul(k, Nat.add(a, b)) == Nat.add(Nat.mul(k, a), Nat.mul(k, b)) : Nat}
  BendMlNatLemmas.mul_one_l (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=mul_one_l)
   law mul_one_l:
     for +a: Nat
     {Nat.mul(1n, a) == a : Nat}
  BendMlNatLemmas.mul_one_r (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=mul_one_r)
   law mul_one_r:
     for +a: Nat
     {Nat.mul(a, 1n) == a : Nat}
  BendMlNatLemmas.append_nil (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=append_nil)
   law append_nil:
     for -A: Data
     for  xs: List<&2, A>
     {List.append(&2, A, xs, Nil{}) == xs : List<&2, A>}
  BendMlNatLemmas.append_assoc (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=append_assoc)
   law append_assoc:
     for -A: Data
     for  xs: List<&2, A>
     for  ys: List<&2, A>
     for  zs: List<&2, A>
     {List.append(&2, A, List.append(&2, A, xs, ys), zs) == List.append(&2, A, xs, List.append(&2, A, ys, zs)) : List<&2, A>}
  BendMlNatLemmas.length_append (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=length_append)
   law length_append:
     for -A: Data
     for  xs: List<&2, A>
     for  ys: List<&2, A>
     {List.length(&2, A, List.append(&2, A, xs, ys)) == Nat.add(List.length(&2, A, xs), List.length(&2, A, ys)) : Nat}
  BendMlNatLemmas.product_append (https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=product_append)
   law product_append:
     for +xs: List<&2, Nat>
     for +ys: List<&2, Nat>
     {product(List.append(&2, Nat, xs, ys)) == Nat.mul(product(xs), product(ys)) : Nat}