bend-mathlib

Releases (15):
  0.8.1.0  0x8ae61ec3a6615abd35f196c07232ad28  indexed  https://jend.leeeet.dev/files.txt?path=bend-mathlib@0.8.1.0
  0.8.0.0  0x78e347bf8d0582a322c01b02c727566f  unindexed  https://jend.leeeet.dev/files.txt?path=bend-mathlib@0.8.0.0
  0.7.5.0  0xcd4682caa53da19986acd472c2181473  unindexed  https://jend.leeeet.dev/files.txt?path=bend-mathlib@0.7.5.0
  0.7.4.0  0xcdaf59a0332a2e0cdb289bf7a32fba62  unindexed  https://jend.leeeet.dev/files.txt?path=bend-mathlib@0.7.4.0
  0.7.3.0  0xf8a2f05bbfb67041ce3d1eaece892a1a  unindexed  https://jend.leeeet.dev/files.txt?path=bend-mathlib@0.7.3.0
  0.7.2.0  0x449abff091641d732d7b9f0780df40ae  unindexed  https://jend.leeeet.dev/files.txt?path=bend-mathlib@0.7.2.0
  0.7.1.0  0x3c446c5bcf57d1eef89775ba0b411fc6  unindexed  https://jend.leeeet.dev/files.txt?path=bend-mathlib@0.7.1.0
  0.7.0.0  0x63d5fd78a2a52f082c7824372390170c  unindexed  https://jend.leeeet.dev/files.txt?path=bend-mathlib@0.7.0.0
  0.6.0.0  0x0eaaf505a355d14d67066b86c801e960  unindexed  https://jend.leeeet.dev/files.txt?path=bend-mathlib@0.6.0.0
  0.5.0.0  0x676cb0b2ca8c3fdeee47023a54e3ac54  unindexed  https://jend.leeeet.dev/files.txt?path=bend-mathlib@0.5.0.0
  0.4.0.0  0xfa8bcf3897afe3da6c28dd6f9de6cbea  unindexed  https://jend.leeeet.dev/files.txt?path=bend-mathlib@0.4.0.0
  0.3.0.0  0x74bdc843cd4bfb31bb6f7ba1eb38d231  unindexed  https://jend.leeeet.dev/files.txt?path=bend-mathlib@0.3.0.0
  0.2.0.0  0x3b339f308342d91e7e6c71e057d59f1b  unindexed  https://jend.leeeet.dev/files.txt?path=bend-mathlib@0.2.0.0
  0.1.0.1  0xafc61ca8b7738a6df7f28eddf80168f8  unindexed  https://jend.leeeet.dev/files.txt?path=bend-mathlib@0.1.0.1
  0.1.0.0  0xe225657a7b1852c0f87dfc66dd576f68  unindexed  https://jend.leeeet.dev/files.txt?path=bend-mathlib@0.1.0.0

Definitions (1126, 1 to 100 shown):
  Algebra.op_assoc4 (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=op_assoc4)
   # Four-way reassociation from associativity alone.
   law op_assoc4:
     for ~A: Data
     for ~op: A -> A -> A
     for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
     for +a: A
     for +b: A
     for +c: A
     for +d: A
     {op(op(op(a, b), c), d) == op(a, op(b, op(c, d))) : A}
  Algebra.op_left_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=op_left_comm)
   # Left commutation from associativity and commutativity.
   law op_left_comm:
     for ~A: Data
     for ~op: A -> A -> A
     for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
     for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
     for +a: A
     for +b: A
     for +c: A
     {op(a, op(b, c)) == op(b, op(a, c)) : A}
  Algebra.op_right_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=op_right_comm)
   # Right commutation from associativity and commutativity.
   law op_right_comm:
     for ~A: Data
     for ~op: A -> A -> A
     for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
     for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
     for +a: A
     for +b: A
     for +c: A
     {op(op(a, b), c) == op(op(a, c), b) : A}
  Algebra.op_four (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=op_four)
   # Middle-four interchange from associativity and commutativity.
   law op_four:
     for ~A: Data
     for ~op: A -> A -> A
     for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
     for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
     for +a: A
     for +b: A
     for +c: A
     for +d: A
     {op(op(a, b), op(c, d)) == op(op(a, c), op(b, d)) : A}
  Algebra.op_comm3 (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=op_comm3)
   # Three-way commutation from commutativity alone.
   law op_comm3:
     for ~A: Data
     for ~op: A -> A -> A
     for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
     for +a: A
     for +b: A
     for +c: A
     {op(op(a, b), c) == op(c, op(b, a)) : A}
  Algebra.internal_nat_add_assoc (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_nat_add_assoc)
   def internal_nat_add_assoc(x: Nat, y: Nat, z: Nat) -> {Nat.add(Nat.add(x, y), z) == Nat.add(x, Nat.add(y, z)) : Nat}:
  Algebra.internal_nat_add_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_nat_add_comm)
   def internal_nat_add_comm(x: Nat, y: Nat) -> {Nat.add(x, y) == Nat.add(y, x) : Nat}:
  Algebra.internal_nat_zero_add (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_nat_zero_add)
   def internal_nat_zero_add(x: Nat) -> {Nat.add(0n, x) == x : Nat}:
  Algebra.internal_nat_mul (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_nat_mul)
   def internal_nat_mul(x: Nat, y: Nat) -> Nat:
  Algebra.internal_nat_mul_assoc (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_nat_mul_assoc)
   def internal_nat_mul_assoc(x: Nat, y: Nat, z: Nat) -> {Nat.mul(Nat.mul(x, y), z) == Nat.mul(x, Nat.mul(y, z)) : Nat}:
  Algebra.internal_nat_mul_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_nat_mul_comm)
   def internal_nat_mul_comm(x: Nat, y: Nat) -> {Nat.mul(x, y) == Nat.mul(y, x) : Nat}:
  Algebra.internal_bool_and_assoc (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_bool_and_assoc)
   def internal_bool_and_assoc(x: Bool, y: Bool, z: Bool) -> {Bool.and(Bool.and(x, y), z) == Bool.and(x, Bool.and(y, z)) : Bool}:
  Algebra.internal_bool_and_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_bool_and_comm)
   def internal_bool_and_comm(x: Bool, y: Bool) -> {Bool.and(x, y) == Bool.and(y, x) : Bool}:
  Algebra.internal_bool_or_assoc (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_bool_or_assoc)
   def internal_bool_or_assoc(x: Bool, y: Bool, z: Bool) -> {Bool.or(Bool.or(x, y), z) == Bool.or(x, Bool.or(y, z)) : Bool}:
  Algebra.internal_bool_or_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_bool_or_comm)
   def internal_bool_or_comm(x: Bool, y: Bool) -> {Bool.or(x, y) == Bool.or(y, x) : Bool}:
  Algebra.internal_list_nat_append_assoc (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_list_nat_append_assoc)
   def internal_list_nat_append_assoc(x: List<&2, Nat>, y: List<&2, Nat>, z: List<&2, Nat>) -> {List.append(&2, Nat, List.append(&2, Nat, x, y), z) == List.append(&2, Nat, x, List.append(&2, Nat, y, z)) : List<&2, Nat>}:
  Algebra.nat_add_left_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=nat_add_left_comm)
   # Nat addition is left-commutative (the same statement as MNat.add_left_comm).
   law nat_add_left_comm:
     for +a: Nat
     for +b: Nat
     for +c: Nat
     {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}
  Algebra.nat_add_right_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=nat_add_right_comm)
   # Nat addition is right-commutative (the same statement as MNat.add_right_comm).
   law nat_add_right_comm:
     for +a: Nat
     for +b: Nat
     for +c: Nat
     {Nat.add(Nat.add(a, b), c) == Nat.add(Nat.add(a, c), b) : Nat}
  Algebra.nat_add_four (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=nat_add_four)
   # Nat addition's middle-four interchange (the same statement as MNat.add_add_add_comm).
   law nat_add_four:
     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}
  Algebra.nat_mul_left_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=nat_mul_left_comm)
   # Nat multiplication is left-commutative (the same statement as MNat.mul_left_comm).
   law nat_mul_left_comm:
     for +a: Nat
     for +b: Nat
     for +c: Nat
     {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(b, Nat.mul(a, c)) : Nat}
  Algebra.nat_mul_right_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=nat_mul_right_comm)
   # Nat multiplication is right-commutative (the same statement as MNat.mul_right_comm).
   law nat_mul_right_comm:
     for +a: Nat
     for +b: Nat
     for +c: Nat
     {Nat.mul(Nat.mul(a, b), c) == Nat.mul(Nat.mul(a, c), b) : Nat}
  Algebra.nat_mul_four (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=nat_mul_four)
   # Nat multiplication's middle-four interchange (the same statement as MNat.mul_mul_mul_comm).
   law nat_mul_four:
     for +a: Nat
     for +b: Nat
     for +c: Nat
     for +d: Nat
     {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) : Nat}
  Algebra.bool_and_left_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=bool_and_left_comm)
   # Bool and is left-commutative.
   law bool_and_left_comm:
     for +a: Bool
     for +b: Bool
     for +c: Bool
     {Bool.and(a, Bool.and(b, c)) == Bool.and(b, Bool.and(a, c)) : Bool}
  Algebra.bool_and_right_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=bool_and_right_comm)
   # Bool and is right-commutative.
   law bool_and_right_comm:
     for +a: Bool
     for +b: Bool
     for +c: Bool
     {Bool.and(Bool.and(a, b), c) == Bool.and(Bool.and(a, c), b) : Bool}
  Algebra.bool_or_left_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=bool_or_left_comm)
   # Bool or is left-commutative.
   law bool_or_left_comm:
     for +a: Bool
     for +b: Bool
     for +c: Bool
     {Bool.or(a, Bool.or(b, c)) == Bool.or(b, Bool.or(a, c)) : Bool}
  Algebra.bool_or_right_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=bool_or_right_comm)
   # Bool or is right-commutative.
   law bool_or_right_comm:
     for +a: Bool
     for +b: Bool
     for +c: Bool
     {Bool.or(Bool.or(a, b), c) == Bool.or(Bool.or(a, c), b) : Bool}
  Algebra.list_nat_append_assoc4 (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=list_nat_append_assoc4)
   # Four-way reassociation for List append over Nat.
   law list_nat_append_assoc4:
     for +a: List<&2, Nat>
     for +b: List<&2, Nat>
     for +c: List<&2, Nat>
     for +d: List<&2, Nat>
     {List.append(&2, Nat, List.append(&2, Nat, List.append(&2, Nat, a, b), c), d) == List.append(&2, Nat, a, List.append(&2, Nat, b, List.append(&2, Nat, c, d))) : List<&2, Nat>}
  Algebra.internal_foldl_foldr (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_foldl_foldr)
   def internal_foldl_foldr(~B: Data, ~op: B -> B -> B, ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}, ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}, ~z: B, ~id: @x: B -> {op(z, x) == x : B}, +xs: List<&2, B>, +acc: B) -> {List.foldl(&2, B, B, op, xs, acc) == op(acc, List.foldr(&2, B, B, op, xs, z)) : B}:
  Algebra.foldl_op_eq_foldr_op (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=foldl_op_eq_foldr_op)
   # Folding left equals folding right for an associative, commutative operation with a left identity (foldl_eq_foldr needs no identity).
   law foldl_op_eq_foldr_op:
     for ~B: Data
     for ~op: B -> B -> B
     for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
     for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
     for ~z: B
     for ~id: @x: B -> {op(z, x) == x : B}
     for +xs: List<&2, B>
     {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}
  Algebra.internal_nat_foldl_op_eq_foldr_op (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_nat_foldl_op_eq_foldr_op)
   # A Nat call: --verdict takes a ~ constant's model from a call of its law (PLAN F38).
   def internal_nat_foldl_op_eq_foldr_op(+xs: List<&2, Nat>) -> {List.foldl(&2, Nat, Nat, Nat.add, xs, 0n) == List.foldr(&2, Nat, Nat, Nat.add, xs, 0n) : Nat}:
  Algebra.internal_foldl_assoc (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_foldl_assoc)
   def internal_foldl_assoc(~B: Data, ~op: B -> B -> B, ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}, +xs: List<&2, B>, +a: B, +b: B) -> {List.foldl(&2, B, B, op, xs, op(a, b)) == op(a, List.foldl(&2, B, B, op, xs, b)) : B}:
  Algebra.internal_foldl_eq_foldr (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_foldl_eq_foldr)
   def internal_foldl_eq_foldr(~B: Data, ~op: B -> B -> B, ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}, ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}, +z: B, +xs: List<&2, B>) -> {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}:
  Algebra.foldl_eq_foldr (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=foldl_eq_foldr)
   # Folding left equals folding right for an associative, commutative operation (Mathlib's List.foldl_eq_foldr).
   law foldl_eq_foldr:
     for ~B: Data
     for ~op: B -> B -> B
     for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
     for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
     for +z: B
     for +xs: List<&2, B>
     {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}
  Algebra.op_assoc4_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=op_assoc4_sym)
   # Four-way reassociation from associativity alone, reversed to rewrite toward the simple side.
   law op_assoc4_sym:
     for ~A: Data
     for ~op: A -> A -> A
     for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
     for +a: A
     for +b: A
     for +c: A
     for +d: A
     {op(a, op(b, op(c, d))) == op(op(op(a, b), c), d) : A}
  Algebra.op_left_comm_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=op_left_comm_sym)
   # Left commutation from associativity and commutativity, reversed to rewrite toward the simple side.
   law op_left_comm_sym:
     for ~A: Data
     for ~op: A -> A -> A
     for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
     for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
     for +a: A
     for +b: A
     for +c: A
     {op(b, op(a, c)) == op(a, op(b, c)) : A}
  Algebra.op_right_comm_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=op_right_comm_sym)
   # Right commutation from associativity and commutativity, reversed to rewrite toward the simple side.
   law op_right_comm_sym:
     for ~A: Data
     for ~op: A -> A -> A
     for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
     for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
     for +a: A
     for +b: A
     for +c: A
     {op(op(a, c), b) == op(op(a, b), c) : A}
  Algebra.op_four_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=op_four_sym)
   # Middle-four interchange from associativity and commutativity, reversed to rewrite toward the simple side.
   law op_four_sym:
     for ~A: Data
     for ~op: A -> A -> A
     for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
     for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
     for +a: A
     for +b: A
     for +c: A
     for +d: A
     {op(op(a, c), op(b, d)) == op(op(a, b), op(c, d)) : A}
  Algebra.op_comm3_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=op_comm3_sym)
   # Three-way commutation from commutativity alone, reversed to rewrite toward the simple side.
   law op_comm3_sym:
     for ~A: Data
     for ~op: A -> A -> A
     for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
     for +a: A
     for +b: A
     for +c: A
     {op(c, op(b, a)) == op(op(a, b), c) : A}
  Algebra.nat_add_left_comm_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=nat_add_left_comm_sym)
   # Nat addition is left-commutative (the same statement as MNat.add_left_comm), reversed to rewrite toward the simple side.
   law nat_add_left_comm_sym:
     for +a: Nat
     for +b: Nat
     for +c: Nat
     {Nat.add(b, Nat.add(a, c)) == Nat.add(a, Nat.add(b, c)) : Nat}
  Algebra.nat_add_right_comm_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=nat_add_right_comm_sym)
   # Nat addition is right-commutative (the same statement as MNat.add_right_comm), reversed to rewrite toward the simple side.
   law nat_add_right_comm_sym:
     for +a: Nat
     for +b: Nat
     for +c: Nat
     {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(a, b), c) : Nat}
  Algebra.nat_add_four_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=nat_add_four_sym)
   # Nat addition's middle-four interchange (the same statement as MNat.add_add_add_comm), reversed to rewrite toward the simple side.
   law nat_add_four_sym:
     for +a: Nat
     for +b: Nat
     for +c: Nat
     for +d: Nat
     {Nat.add(Nat.add(a, c), Nat.add(b, d)) == Nat.add(Nat.add(a, b), Nat.add(c, d)) : Nat}
  Algebra.nat_mul_left_comm_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=nat_mul_left_comm_sym)
   # Nat multiplication is left-commutative (the same statement as MNat.mul_left_comm), reversed to rewrite toward the simple side.
   law nat_mul_left_comm_sym:
     for +a: Nat
     for +b: Nat
     for +c: Nat
     {Nat.mul(b, Nat.mul(a, c)) == Nat.mul(a, Nat.mul(b, c)) : Nat}
  Algebra.nat_mul_right_comm_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=nat_mul_right_comm_sym)
   # Nat multiplication is right-commutative (the same statement as MNat.mul_right_comm), reversed to rewrite toward the simple side.
   law nat_mul_right_comm_sym:
     for +a: Nat
     for +b: Nat
     for +c: Nat
     {Nat.mul(Nat.mul(a, c), b) == Nat.mul(Nat.mul(a, b), c) : Nat}
  Algebra.nat_mul_four_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=nat_mul_four_sym)
   # Nat multiplication's middle-four interchange (the same statement as MNat.mul_mul_mul_comm), reversed to rewrite toward the simple side.
   law nat_mul_four_sym:
     for +a: Nat
     for +b: Nat
     for +c: Nat
     for +d: Nat
     {Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) == Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) : Nat}
  Algebra.bool_and_left_comm_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=bool_and_left_comm_sym)
   # Bool and is left-commutative, reversed to rewrite toward the simple side.
   law bool_and_left_comm_sym:
     for +a: Bool
     for +b: Bool
     for +c: Bool
     {Bool.and(b, Bool.and(a, c)) == Bool.and(a, Bool.and(b, c)) : Bool}
  Algebra.bool_and_right_comm_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=bool_and_right_comm_sym)
   # Bool and is right-commutative, reversed to rewrite toward the simple side.
   law bool_and_right_comm_sym:
     for +a: Bool
     for +b: Bool
     for +c: Bool
     {Bool.and(Bool.and(a, c), b) == Bool.and(Bool.and(a, b), c) : Bool}
  Algebra.bool_or_left_comm_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=bool_or_left_comm_sym)
   # Bool or is left-commutative, reversed to rewrite toward the simple side.
   law bool_or_left_comm_sym:
     for +a: Bool
     for +b: Bool
     for +c: Bool
     {Bool.or(b, Bool.or(a, c)) == Bool.or(a, Bool.or(b, c)) : Bool}
  Algebra.bool_or_right_comm_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=bool_or_right_comm_sym)
   # Bool or is right-commutative, reversed to rewrite toward the simple side.
   law bool_or_right_comm_sym:
     for +a: Bool
     for +b: Bool
     for +c: Bool
     {Bool.or(Bool.or(a, c), b) == Bool.or(Bool.or(a, b), c) : Bool}
  Algebra.list_nat_append_assoc4_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=list_nat_append_assoc4_sym)
   # Four-way reassociation for List append over Nat, reversed to rewrite toward the simple side.
   law list_nat_append_assoc4_sym:
     for +a: List<&2, Nat>
     for +b: List<&2, Nat>
     for +c: List<&2, Nat>
     for +d: List<&2, Nat>
     {List.append(&2, Nat, a, List.append(&2, Nat, b, List.append(&2, Nat, c, d))) == List.append(&2, Nat, List.append(&2, Nat, List.append(&2, Nat, a, b), c), d) : List<&2, Nat>}
  Algebra.foldl_op_eq_foldr_op_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=foldl_op_eq_foldr_op_sym)
   # Folding left equals folding right for an associative, commutative operation with a left identity (foldl_eq_foldr needs no identity), reversed to rewrite toward the simple side.
   law foldl_op_eq_foldr_op_sym:
     for ~B: Data
     for ~op: B -> B -> B
     for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
     for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
     for ~z: B
     for ~id: @x: B -> {op(z, x) == x : B}
     for +xs: List<&2, B>
     {List.foldr(&2, B, B, op, xs, z) == List.foldl(&2, B, B, op, xs, z) : B}
  Algebra.foldl_eq_foldr_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=foldl_eq_foldr_sym)
   # Folding left equals folding right for an associative, commutative operation (Mathlib's List.foldl_eq_foldr), reversed to rewrite toward the simple side.
   law foldl_eq_foldr_sym:
     for ~B: Data
     for ~op: B -> B -> B
     for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
     for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
     for +z: B
     for +xs: List<&2, B>
     {List.foldr(&2, B, B, op, xs, z) == List.foldl(&2, B, B, op, xs, z) : B}
  Algebra.internal_nat_foldl_op_eq_foldr_op_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_nat_foldl_op_eq_foldr_op_sym)
   # Calls of the twins, as the calls above the generated section make of their laws (PLAN F38).
   def internal_nat_foldl_op_eq_foldr_op_sym(+xs: List<&2, Nat>) -> {List.foldr(&2, Nat, Nat, Nat.add, xs, 0n) == List.foldl(&2, Nat, Nat, Nat.add, xs, 0n) : Nat}:
  Bool.not_not (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=not_not)
   # Negating a boolean twice gives it back.
   law not_not:
     for b: Bool
     {Bool.not(Bool.not(b)) == b : Bool}
  Bool.and_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=and_comm)
   # Boolean and is commutative.
   law and_comm:
     for a: Bool
     for b: Bool
     {Bool.and(a, b) == Bool.and(b, a) : Bool}
  Bool.or_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=or_comm)
   # Boolean or is commutative.
   law or_comm:
     for a: Bool
     for b: Bool
     {Bool.or(a, b) == Bool.or(b, a) : Bool}
  Bool.and_assoc (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=and_assoc)
   # Boolean and is associative.
   law and_assoc:
     for a: Bool
     for -b: Bool
     for -c: Bool
     {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool}
  Bool.or_assoc (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=or_assoc)
   # Boolean or is associative.
   law or_assoc:
     for a: Bool
     for -b: Bool
     for -c: Bool
     {Bool.or(Bool.or(a, b), c) == Bool.or(a, Bool.or(b, c)) : Bool}
  Bool.and_true (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=and_true)
   # True is a right identity for and: a and true is a.
   law and_true:
     for a: Bool
     {Bool.and(a, True{}) == a : Bool}
  Bool.true_and (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=true_and)
   # True is a left identity for and: true and a is a.
   law true_and:
     for -a: Bool
     {Bool.and(True{}, a) == a : Bool}
  Bool.and_false (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=and_false)
   # False absorbs and on the right: a and false is false.
   law and_false:
     for a: Bool
     {Bool.and(a, False{}) == False{} : Bool}
  Bool.false_and (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=false_and)
   # False absorbs and on the left: false and a is false.
   law false_and:
     for -a: Bool
     {Bool.and(False{}, a) == False{} : Bool}
  Bool.or_false (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=or_false)
   # False is a right identity for or: a or false is a.
   law or_false:
     for a: Bool
     {Bool.or(a, False{}) == a : Bool}
  Bool.false_or (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=false_or)
   # False is a left identity for or: false or a is a.
   law false_or:
     for -a: Bool
     {Bool.or(False{}, a) == a : Bool}
  Bool.or_true (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=or_true)
   # True absorbs or on the right: a or true is true.
   law or_true:
     for a: Bool
     {Bool.or(a, True{}) == True{} : Bool}
  Bool.true_or (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=true_or)
   # True absorbs or on the left: true or a is true.
   law true_or:
     for -a: Bool
     {Bool.or(True{}, a) == True{} : Bool}
  Bool.de_morgan_and (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=de_morgan_and)
   # De Morgan: not (a and b) is (not a) or (not b).
   law de_morgan_and:
     for a: Bool
     for -b: Bool
     {Bool.not(Bool.and(a, b)) == Bool.or(Bool.not(a), Bool.not(b)) : Bool}
  Bool.de_morgan_or (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=de_morgan_or)
   # De Morgan: not (a or b) is (not a) and (not b).
   law de_morgan_or:
     for a: Bool
     for -b: Bool
     {Bool.not(Bool.or(a, b)) == Bool.and(Bool.not(a), Bool.not(b)) : Bool}
  Bool.internal_true_ne_false (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=internal_true_ne_false)
   def internal_true_ne_false(e: {True{} == False{} : Bool}) -> Empty:
  Bool.true_ne_false (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=true_ne_false)
   # True and False are different booleans.
   law true_ne_false:
     {True{} != False{} : Bool}
  Bool.and_self (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=and_self)
   # And with itself: a and a is a.
   law and_self:
     for a: Bool
     {Bool.and(a, a) == a : Bool}
  Bool.or_self (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=or_self)
   # Or with itself: a or a is a.
   law or_self:
     for a: Bool
     {Bool.or(a, a) == a : Bool}
  Bool.and_not_self (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=and_not_self)
   # A boolean and its negation are never both true: a and (not a) is false.
   law and_not_self:
     for a: Bool
     {Bool.and(a, Bool.not(a)) == False{} : Bool}
  Bool.or_not_self (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=or_not_self)
   # A boolean or its negation is always true: a or (not a) is true.
   law or_not_self:
     for a: Bool
     {Bool.or(a, Bool.not(a)) == True{} : Bool}
  Bool.and_or_distrib_left (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=and_or_distrib_left)
   # And distributes over or: a and (b or c) is (a and b) or (a and c).
   law and_or_distrib_left:
     for a: Bool
     for -b: Bool
     for -c: Bool
     {Bool.and(a, Bool.or(b, c)) == Bool.or(Bool.and(a, b), Bool.and(a, c)) : Bool}
  Bool.or_and_distrib_left (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=or_and_distrib_left)
   # Or distributes over and: a or (b and c) is (a or b) and (a or c).
   law or_and_distrib_left:
     for a: Bool
     for -b: Bool
     for -c: Bool
     {Bool.or(a, Bool.and(b, c)) == Bool.and(Bool.or(a, b), Bool.or(a, c)) : Bool}
  Bool.and_or_absorb (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=and_or_absorb)
   # Absorption: a and (a or b) is a.
   law and_or_absorb:
     for a: Bool
     for -b: Bool
     {Bool.and(a, Bool.or(a, b)) == a : Bool}
  Bool.or_and_absorb (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=or_and_absorb)
   # Absorption: a or (a and b) is a.
   law or_and_absorb:
     for a: Bool
     for -b: Bool
     {Bool.or(a, Bool.and(a, b)) == a : Bool}
  Bool.xor_comm (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=xor_comm)
   # Exclusive or is commutative.
   law xor_comm:
     for a: Bool
     for b: Bool
     {Bool.xor(a, b) == Bool.xor(b, a) : Bool}
  Bool.xor_assoc (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=xor_assoc)
   # Exclusive or is associative.
   law xor_assoc:
     for a: Bool
     for b: Bool
     for c: Bool
     {Bool.xor(Bool.xor(a, b), c) == Bool.xor(a, Bool.xor(b, c)) : Bool}
  Bool.xor_self (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=xor_self)
   # A boolean xor itself is false.
   law xor_self:
     for a: Bool
     {Bool.xor(a, a) == False{} : Bool}
  Bool.xor_false (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=xor_false)
   # False is an identity for xor: a xor false is a.
   law xor_false:
     for a: Bool
     {Bool.xor(a, False{}) == a : Bool}
  Bool.xor_true (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=xor_true)
   # Xor with true negates: a xor true is not a.
   law xor_true:
     for a: Bool
     {Bool.xor(a, True{}) == Bool.not(a) : Bool}
  Bool.not_inj (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=not_inj)
   # Negation is injective: not a = not b implies a = b.
   law not_inj:
     for a: Bool
     for b: Bool
     for h: {Bool.not(a) == Bool.not(b) : Bool}
     {a == b : Bool}
  Bool.eq_true_of_ne_false (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=eq_true_of_ne_false)
   # A boolean that is not false is true.
   law eq_true_of_ne_false:
     for a: Bool
     for h: {a == False{} : Bool} -> Empty
     {a == True{} : Bool}
  Bool.internal_false_ne_true (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=internal_false_ne_true)
   def internal_false_ne_true(e: {False{} == True{} : Bool}) -> Empty:
  Bool.cmp_refl (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=cmp_refl)
   # Comparing a boolean with itself gives EQ.
   law cmp_refl:
     for b: Bool
     {Bool.cmp(b, b) == EQ{} : Cmp}
  Bool.eq_of_cmp_eq (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=eq_of_cmp_eq)
   # Two booleans that compare EQ are equal.
   law eq_of_cmp_eq:
     for a: Bool
     for b: Bool
     for h: {Cmp.is_eq(Bool.cmp(a, b)) == True{} : Bool}
     {a == b : Bool}
  Bool.false_ne_true (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=false_ne_true)
   # False and True are different booleans, the other way round.
   law false_ne_true:
     {False{} != True{} : Bool}
  Bool.eq_true_of_and_left (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=eq_true_of_and_left)
   # If a and b is true then a is true.
   law eq_true_of_and_left:
     for a: Bool
     for -b: Bool
     for h: {Bool.and(a, b) == True{} : Bool}
     {a == True{} : Bool}
  Bool.eq_true_of_and_right (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=eq_true_of_and_right)
   # If a and b is true then b is true.
   law eq_true_of_and_right:
     for a: Bool
     for -b: Bool
     for h: {Bool.and(a, b) == True{} : Bool}
     {b == True{} : Bool}
  Bool.and_eq_true (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=and_eq_true)
   # If a and b are both true then a and b is true.
   law and_eq_true:
     for a: Bool
     for -b: Bool
     for ha: {a == True{} : Bool}
     for hb: {b == True{} : Bool}
     {Bool.and(a, b) == True{} : Bool}
  Bool.eq_true_of_or_eq_false_right (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=eq_true_of_or_eq_false_right)
   # If a or b is true and b is false then a is true.
   law eq_true_of_or_eq_false_right:
     for a: Bool
     for -b: Bool
     for h: {Bool.or(a, b) == True{} : Bool}
     for hb: {b == False{} : Bool}
     {a == True{} : Bool}
  Bool.eq_true_of_or_eq_false_left (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=eq_true_of_or_eq_false_left)
   # If a or b is true and a is false then b is true.
   law eq_true_of_or_eq_false_left:
     for a: Bool
     for -b: Bool
     for h: {Bool.or(a, b) == True{} : Bool}
     for ha: {a == False{} : Bool}
     {b == True{} : Bool}
  Bool.eq_false_of_not_eq_true (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=eq_false_of_not_eq_true)
   # If not b is true then b is false.
   law eq_false_of_not_eq_true:
     for b: Bool
     for h: {Bool.not(b) == True{} : Bool}
     {b == False{} : Bool}
  Bool.not_not_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=not_not_sym)
   # Negating a boolean twice gives it back, reversed to rewrite toward the simple side.
   law not_not_sym:
     for b: Bool
     {b == Bool.not(Bool.not(b)) : Bool}
  Bool.and_comm_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=and_comm_sym)
   # Boolean and is commutative, reversed to rewrite toward the simple side.
   law and_comm_sym:
     for a: Bool
     for b: Bool
     {Bool.and(b, a) == Bool.and(a, b) : Bool}
  Bool.or_comm_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=or_comm_sym)
   # Boolean or is commutative, reversed to rewrite toward the simple side.
   law or_comm_sym:
     for a: Bool
     for b: Bool
     {Bool.or(b, a) == Bool.or(a, b) : Bool}
  Bool.and_assoc_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=and_assoc_sym)
   # Boolean and is associative, reversed to rewrite toward the simple side.
   law and_assoc_sym:
     for a: Bool
     for -b: Bool
     for -c: Bool
     {Bool.and(a, Bool.and(b, c)) == Bool.and(Bool.and(a, b), c) : Bool}
  Bool.or_assoc_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=or_assoc_sym)
   # Boolean or is associative, reversed to rewrite toward the simple side.
   law or_assoc_sym:
     for a: Bool
     for -b: Bool
     for -c: Bool
     {Bool.or(a, Bool.or(b, c)) == Bool.or(Bool.or(a, b), c) : Bool}
  Bool.and_true_sym (https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=and_true_sym)
   # True is a right identity for and: a and true is a, reversed to rewrite toward the simple side.
   law and_true_sym:
     for a: Bool
     {a == Bool.and(a, True{}) : Bool}
More: https://jend.leeeet.dev/packages/bend-mathlib.txt?definitions_offset=100