~/bend-docscommunity

LAWS.bend open laws/TODOs

raw source on the hub · import 0x498c837faf89711c8803bb21f694c5ca/LAWS.bend as LAWS

2 imports
import Base
import ./lib.bend as R

Laws

law bound_inclusive provedin PROOF.bendsource · line 5 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Bound.is_inclusive(0x498c837faf89711c8803bb21f694c5ca/lib.Inclusive{}) == True{} : Bool}

Bound and constructor semantics.

law bound_exclusive provedin PROOF.bendsource · line 8 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Bound.is_inclusive(0x498c837faf89711c8803bb21f694c5ca/lib.Exclusive{}) == False{} : Bool}

law nat_make provedin PROOF.bendsource · line 11 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.make(2n, 0x498c837faf89711c8803bb21f694c5ca/lib.Inclusive{}, 5n, 0x498c837faf89711c8803bb21f694c5ca/lib.Exclusive{}) == 0x498c837faf89711c8803bb21f694c5ca/lib.NR{2n, 0x498c837faf89711c8803bb21f694c5ca/lib.Inclusive{}, 5n, 0x498c837faf89711c8803bb21f694c5ca/lib.Exclusive{}} : 0x498c837faf89711c8803bb21f694c5ca/lib.Range.NatRange}

law nat_closed provedin PROOF.bendsource · line 15 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.closed(2n, 5n) == 0x498c837faf89711c8803bb21f694c5ca/lib.NR{2n, 0x498c837faf89711c8803bb21f694c5ca/lib.Inclusive{}, 5n, 0x498c837faf89711c8803bb21f694c5ca/lib.Inclusive{}} : 0x498c837faf89711c8803bb21f694c5ca/lib.Range.NatRange}

law u32_make provedin PROOF.bendsource · line 19 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.make_u32(2, 0x498c837faf89711c8803bb21f694c5ca/lib.Inclusive{}, 5, 0x498c837faf89711c8803bb21f694c5ca/lib.Exclusive{}) == 0x498c837faf89711c8803bb21f694c5ca/lib.UR{2, 0x498c837faf89711c8803bb21f694c5ca/lib.Inclusive{}, 5, 0x498c837faf89711c8803bb21f694c5ca/lib.Exclusive{}} : 0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32Range}

law nat_closed_open provedin PROOF.bendsource · line 24 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.to_list(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.closed_open(2n, 5n)) == [2n, 3n, 4n] : List<&2, Nat>}

Nat endpoint semantics, emptiness, cardinality, and enumeration.

law nat_closed_open_length provedin PROOF.bendsource · line 28 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.length(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.closed_open(2n, 5n)) == 3n : Nat}

law nat_open_closed provedin PROOF.bendsource · line 31 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.to_list(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.open_closed(2n, 5n)) == [3n, 4n, 5n] : List<&2, Nat>}

law nat_open provedin PROOF.bendsource · line 35 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.to_list(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.open(2n, 5n)) == [3n, 4n] : List<&2, Nat>}

law nat_singleton provedin PROOF.bendsource · line 39 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.length(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.closed(4n, 4n)) == 1n : Nat}

law nat_open_singleton_empty provedin PROOF.bendsource · line 42 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.is_empty(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.open(4n, 4n)) == True{} : Bool}

law nat_reversed_empty provedin PROOF.bendsource · line 45 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.to_list(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.closed(5n, 2n)) == [] : List<&2, Nat>}

law nat_contains_inside provedin PROOF.bendsource · line 48 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.contains(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.closed_open(2n, 5n), 4n) == True{} : Bool}

law nat_contains_excluded_upper provedin PROOF.bendsource · line 52 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.contains(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.closed_open(2n, 5n), 5n) == False{} : Bool}

law nat_contains_excluded_lower provedin PROOF.bendsource · line 56 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.contains(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.open_closed(2n, 5n), 2n) == False{} : Bool}

law nat_overlap_touch_closed provedin PROOF.bendsource · line 60 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.overlap(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.closed(1n, 3n), 0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.closed(3n, 5n)) == True{} : Bool}

law nat_overlap_touch_open provedin PROOF.bendsource · line 64 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.overlaps(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.closed(1n, 3n), 0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.open(3n, 5n)) == False{} : Bool}

law nat_overlap_disjoint provedin PROOF.bendsource · line 68 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.overlap(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.closed(1n, 2n), 0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.closed(3n, 5n)) == False{} : Bool}

law nat_clamp_low provedin PROOF.bendsource · line 72 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.clamp(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.closed(2n, 5n), 0n) == 2n : Nat}

law nat_clamp_mid provedin PROOF.bendsource · line 75 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.clamp(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.closed(2n, 5n), 4n) == 4n : Nat}

law nat_clamp_high provedin PROOF.bendsource · line 78 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.clamp(0x498c837faf89711c8803bb21f694c5ca/lib.Range.Nat.closed(2n, 5n), 9n) == 5n : Nat}

law u32_closed_open_length provedin PROOF.bendsource · line 82 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.length(0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.closed_open(2, 5)) == 3n : Nat}

U32 has the same endpoint semantics and uses Nat for its length.

law u32_closed_open_list provedin PROOF.bendsource · line 85 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.to_list(0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.closed_open(2, 5)) == [2, 3, 4] : List<&2, U32>}

law u32_open_list provedin PROOF.bendsource · line 89 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.to_list(0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.open(2, 5)) == [3, 4] : List<&2, U32>}

law u32_singleton provedin PROOF.bendsource · line 93 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.length(0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.closed(7, 7)) == 1n : Nat}

law u32_open_singleton_empty provedin PROOF.bendsource · line 96 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.is_empty(0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.open(7, 7)) == True{} : Bool}

law u32_contains_inside provedin PROOF.bendsource · line 99 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.contains(0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.closed_open(2, 5), 4) == True{} : Bool}

law u32_contains_excluded_upper provedin PROOF.bendsource · line 103 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.contains(0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.closed_open(2, 5), 5) == False{} : Bool}

law u32_overlap_touch_open provedin PROOF.bendsource · line 107 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.overlap(0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.closed(1, 3), 0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.open(3, 5)) == False{} : Bool}

law u32_overlap_disjoint provedin PROOF.bendsource · line 111 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.overlaps(0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.closed(1, 2), 0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.closed(3, 5)) == False{} : Bool}

law u32_clamp_low provedin PROOF.bendsource · line 115 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.clamp(0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.closed(2, 5), 0) == 2 : U32}

law u32_clamp_high provedin PROOF.bendsource · line 118 · raw

{0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.clamp(0x498c837faf89711c8803bb21f694c5ca/lib.Range.U32.closed(2, 5), 9) == 5 : U32}