~/bend-docscommunity

LAWS.bend open laws/TODOs

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

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

Laws

law empty_is_leaf provedin PROOF.bendsource · line 5 · raw

@-a:Quant -> @-A:Kind(a) -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.empty(a, A) == 0x92b0674fe90445059e34a1165b692b0e/lib.Leaf{} : 0x92b0674fe90445059e34a1165b692b0e/lib.Tree<a, A>}

empty is Leaf.

law leaf_is_leaf provedin PROOF.bendsource · line 11 · raw

@-a:Quant -> @-A:Kind(a) -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.leaf(a, A) == 0x92b0674fe90445059e34a1165b692b0e/lib.Leaf{} : 0x92b0674fe90445059e34a1165b692b0e/lib.Tree<a, A>}

leaf is Leaf.

law leaf_eq_empty provedin PROOF.bendsource · line 17 · raw

@-a:Quant -> @-A:Kind(a) -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.leaf(a, A) == 0x92b0674fe90445059e34a1165b692b0e/lib.Tree.empty(a, A) : 0x92b0674fe90445059e34a1165b692b0e/lib.Tree<a, A>}

leaf equals empty.

law singleton_is_node provedin PROOF.bendsource · line 23 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.singleton(a, A, x) == 0x92b0674fe90445059e34a1165b692b0e/lib.Node{0x92b0674fe90445059e34a1165b692b0e/lib.Leaf{}, x, 0x92b0674fe90445059e34a1165b692b0e/lib.Leaf{}} : 0x92b0674fe90445059e34a1165b692b0e/lib.Tree<a, A>}

singleton is Node{Leaf, x, Leaf}.

law size_empty provedin PROOF.bendsource · line 30 · raw

@-a:Quant -> @-A:Kind(a) -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.size(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Tree.empty(a, A)) == 0n : Nat}

size(empty) is 0.

law size_leaf provedin PROOF.bendsource · line 36 · raw

@-a:Quant -> @-A:Kind(a) -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.size(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Leaf{}) == 0n : Nat}

size(Leaf) is 0.

law size_singleton provedin PROOF.bendsource · line 42 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.size(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Tree.singleton(a, A, x)) == 1n : Nat}

size(singleton(x)) is 1.

law size_node_leaves provedin PROOF.bendsource · line 49 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.size(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Node{0x92b0674fe90445059e34a1165b692b0e/lib.Leaf{}, x, 0x92b0674fe90445059e34a1165b692b0e/lib.Leaf{}}) == 1n : Nat}

size(Node{Leaf,x,Leaf}) is 1.

law size_node_def provedin PROOF.bendsource · line 56 · raw

@-a:Quant -> @-A:Kind(a) -> @l:0x92b0674fe90445059e34a1165b692b0e/lib.Tree<a, A> -> @v:A -> @r:0x92b0674fe90445059e34a1165b692b0e/lib.Tree<a, A> -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.size(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Node{l, v, r}) == 1n+Nat.add(0x92b0674fe90445059e34a1165b692b0e/lib.Tree.size(a, A, l), 0x92b0674fe90445059e34a1165b692b0e/lib.Tree.size(a, A, r)) : Nat}

Definitional size of Node.

law size_left_leaf_right_one provedin PROOF.bendsource · line 69 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> @y:A -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.size(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Node{0x92b0674fe90445059e34a1165b692b0e/lib.Leaf{}, x, 0x92b0674fe90445059e34a1165b692b0e/lib.Tree.singleton(a, A, y)}) == 2n : Nat}

size(Node{Leaf, x, singleton(y)}) is 2.

law size_both_singletons provedin PROOF.bendsource · line 81 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> @y:A -> @z:A -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.size(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Node{0x92b0674fe90445059e34a1165b692b0e/lib.Tree.singleton(a, A, x), y, 0x92b0674fe90445059e34a1165b692b0e/lib.Tree.singleton(a, A, z)}) == 3n : Nat}

size of balanced three-node tree is 3.

law to_list_empty provedin PROOF.bendsource · line 94 · raw

@-a:Quant -> @-A:Kind(a) -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.to_list(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Tree.empty(a, A)) == [] : List<a, A>}

to_list(empty) is Nil.

law to_list_leaf provedin PROOF.bendsource · line 100 · raw

@-a:Quant -> @-A:Kind(a) -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.to_list(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Leaf{}) == [] : List<a, A>}

to_list(Leaf) is Nil.

law to_list_singleton provedin PROOF.bendsource · line 106 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.to_list(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Tree.singleton(a, A, x)) == [x] : List<a, A>}

to_list(singleton(x)) is x <> Nil.

law to_list_node_leaves provedin PROOF.bendsource · line 113 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.to_list(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Node{0x92b0674fe90445059e34a1165b692b0e/lib.Leaf{}, x, 0x92b0674fe90445059e34a1165b692b0e/lib.Leaf{}}) == [x] : List<a, A>}

to_list(Node{Leaf,x,Leaf}) is x <> Nil.

law to_list_right_one provedin PROOF.bendsource · line 120 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> @y:A -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.to_list(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Node{0x92b0674fe90445059e34a1165b692b0e/lib.Leaf{}, x, 0x92b0674fe90445059e34a1165b692b0e/lib.Tree.singleton(a, A, y)}) == [x, y] : List<a, A>}

to_list with right singleton.

law to_list_left_one provedin PROOF.bendsource · line 132 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> @y:A -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.to_list(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Node{0x92b0674fe90445059e34a1165b692b0e/lib.Tree.singleton(a, A, x), y, 0x92b0674fe90445059e34a1165b692b0e/lib.Leaf{}}) == [x, y] : List<a, A>}

to_list with left singleton.

law is_empty_empty provedin PROOF.bendsource · line 144 · raw

@-a:Quant -> @-A:Kind(a) -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.is_empty(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Tree.empty(a, A)) == True{} : Bool}

is_empty(empty) is True.

law is_empty_leaf provedin PROOF.bendsource · line 150 · raw

@-a:Quant -> @-A:Kind(a) -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.is_empty(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Leaf{}) == True{} : Bool}

is_empty(Leaf) is True.

law is_empty_singleton provedin PROOF.bendsource · line 156 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.is_empty(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Tree.singleton(a, A, x)) == False{} : Bool}

is_empty(singleton(x)) is False.

law is_empty_node provedin PROOF.bendsource · line 163 · raw

@-a:Quant -> @-A:Kind(a) -> @l:0x92b0674fe90445059e34a1165b692b0e/lib.Tree<a, A> -> @v:A -> @r:0x92b0674fe90445059e34a1165b692b0e/lib.Tree<a, A> -> {0x92b0674fe90445059e34a1165b692b0e/lib.Tree.is_empty(a, A, 0x92b0674fe90445059e34a1165b692b0e/lib.Node{l, v, r}) == False{} : Bool}

is_empty(Node{...}) is False.