Properties
Properties are true expressions. They are used to prove theorems
result of storing value at key: key in map: entries = output of function store_compute where input key is key, value is value, map is entries, and processed map is [ ]
output of function store_compute where input key is key, value is value, map is [ ], and processed map is kvs = reverse of [ entry key: value, kvs ]
output of function store_compute where input key is key, value is value, map is [ ], and processed map is kvs = result of dumping kvs to [ entry key: value, [ ] ]
value at key in map [ pair (key, value), remaining ] = value
value at key in map [ pair (bad_key, value), remaining ] = value at key in map remaining
value at key in map [ entry key: value, remaining ] = value
value at key in map [ entry bad_key: value, remaining ] = value at key in map remaining
map [ entry key: value, remaining ] contains key key = True
map [ entry bad_key: value, remaining ] contains key key = map remaining contains key key
map [ ] contains key key = False
result of deleting the entry with key key from map entries = output of function delete_entry where input key is key, map is entries, and processed is [ ]
output of function delete_entry where input key is key, map is [ pair (key, value), remaining ], and processed is kvs = output of function delete_entry where input key is key, map is remaining, and processed is kvs
output of function delete_entry where input key is key, map is [ pair (lkey, lvalue), remaining ], and processed is kvs = output of function delete_entry where input key is key, map is remaining, and processed is [ pair (lkey, lvalue), kvs ]
output of function delete_entry where input key is key, map is [ entry key: value, remaining ], and processed is kvs = output of function delete_entry where input key is key, map is remaining, and processed is kvs
output of function delete_entry where input key is key, map is [ entry lkey: lvalue, remaining ], and processed is kvs = output of function delete_entry where input key is key, map is remaining, and processed is [ entry lkey: lvalue, kvs ]
output of function delete_entry where input key is key, map is [ ], and processed is kvs = reverse of kvs
Get first key from [ entry key: value, remaining ] = key
towers of hanoi top disks towers = towers of hanoi top disks (towers of hanoi top towers)
towers of hanoi top disks towers = towers
move disk towers is even = result of storing [ x, dst_tower ] at index dst of stack (result of storing rest at index src of stack towers)
get subtowertower = get subtower maptower
get subtower map[ ] = reverse of result
move disk towers = move disk (move one (move disk towers))
move disk towers = move one towers
height of tree tree = Height of a tree tree and index 0
find referece to node index in tree [ node (x, index, right), rest ] = True
find referece to node index in tree [ node (x, left, index), rest ] = True
find referece to node index in tree [ ] = False
find root index in tree = find root index in tree current index is 0
find parent index of tree = find parent index of tree
find parent index of [ node (x, index, right), rest ] = i
find parent index of [ node (x, left, index), rest ] = i
result of removing value from tree tree = result of balancing the tree (pop value from tree tree)
result of halving the stack stack = output of the halve stack function where input stack is stack, other stack is [ ], and count is ((length of stack stack) / 2)
output of the halve stack function where input stack is stack, other stack is other, and count is 0 = [ stack, [ other, [ ] ] ]
result of merging stacks a and b = output of the merge_stacks function where input stacks are a and b, and merged stack is [ ]
output of the merge_stacks function where input stacks are [ ] and [ b, b_rest ], and merged stack is result = output of the merge_stacks function where input stacks are [ ] and b_rest, and merged stack is [ b, result ]
output of the merge_stacks function where input stacks are [ a, a_rest ] and [ ], and merged stack is result = output of the merge_stacks function where input stacks are a_rest and [ ], and merged stack is [ a, result ]
output of the merge_stacks function where input stacks are [ ] and [ ], and merged stack is result = reverse of result
result of merge sorting [ a, [ ] ] = [ a, [ ] ]
result of merge sorting stack = result of merging stacks (result of merge sorting (the element at index 0 of stack (result of halving the stack stack))) and (result of merge sorting (the element at index 1 of stack (result of halving the stack stack)))
tree [ ] contains value = False
elements of values that are not in tree tree = output of the not_in_tree function where the input tree is tree, the values are values, and the new values are [ ]
output of the not_in_tree function where the input tree is tree, the values are [ ], and the new values are result = result
output of the find_neighbors function where the input graph is [ ], node is value, and children are result = result
result of pushing values [ a, rest ] to tree tree = result of pushing values rest to tree [ node (a, [ ]), tree ]
result of pushing values [ ] to tree tree = tree
spanning tree of graph graph starting at node v = output of the spanning_tree function where the input graph is graph, backwards index is 0, and the spanning tree is [ node (v, [ ]), [ ] ]
spanning DFT tree of graph graph starting from v = output of the build_dft_tree function where input graph is graph, tree is [ ], and neighbor stack is [ node (v, None), [ ] ]
output of the build_dft_tree function where input graph is graph, tree is tree, and neighbor stack is [ ] = tree
result of pushing nodes [ pair (value, weight), rest ] into tree tree where parent is index and parent distance is distance = result of pushing nodes rest into tree [ node (value, (distance + weight), index), tree ] where parent is index and parent distance is distance
result of pushing nodes [ ] into tree tree where parent is index and parent distance is distance = tree
result of splitting pairs into nodes that exist in the tree tree and new nodes = output of the separate_nodes function where the input tree is tree, the nodes are pairs, the existing group is [ ], and the new group is [ ]
output of the separate_nodes function where the input tree is tree, the nodes are [ ], the existing group is exist, and the new group is new = pair (exist, new)
result of updating nodes [ ] in tree tree with parent index index and parent distance distance = tree
shortest path from node v to every other node in graph graph = output of the shortest_path function where the input graph is graph, backwards index is 0, and tree is [ node (v, 0, None), [ ] ]
children of the node value in graph graph = output of the find_neighbors function where the input graph is graph, node is value, and children are [ ]
nodes with values values and parent parent = output of the make_nodes function where input values are values, parent is parent, and nodes are [ ]
output of the make_nodes function where input values are [ v, rest ], parent is parent, and nodes are nodes = output of the make_nodes function where input values are rest, parent is parent, and nodes are [ node (v, parent), nodes ]
output of the make_nodes function where input values are [ ], parent is parent, and nodes are nodes = nodes
result of inserting value to tree tree = output of the bst_insert function where the input tree is tree, value is val, visited is [ ], and moves are [ ]
result of building the BST from nodes [ n, [ node (a, None, right), others ] ] and moves [ "L", moves ] = result of building the BST from nodes [ node (a, n, right), others ] and moves moves
result of building the BST from nodes [ n, [ node (a, left, None), others ] ] and moves [ "R", moves ] = result of building the BST from nodes [ node (a, left, n), others ] and moves moves
result of building the BST from nodes [ node, [ ] ] and moves [ ] = node
result of AVL insert of tree tree and value value = result of balancing the tree (result of inserting value to tree tree)
result of rotating (node (v, (node (l, ll, lr)), right)) clockwise = node (l, ll, (node (v, lr, right)))
result of rotating (node (v, (node (l, ll, (node (lr, lrl, lrr)))), right)) twice = node (v, (node (lr, (node (l, ll, lrl)), lrr)), right)
height of tree (node (v, None, None)) = 1
height of tree (node (v, (node (l, ll, lr)), None)) = (height of tree (node (l, ll, lr))) + 1
height of tree (node (v, None, (node (r, rl, rr)))) = (height of tree (node (r, rl, rr))) + 1
result of removing value from tree tree = output of the bst_delete function where input tree is tree, value is val, visited is [ ], and moves are [ ]
output of the bst_delete function where input tree is (node (a, None, None)), value is a, visited is visited, and moves are [ move, rest ] = result of building the BST from nodes visited and moves rest
smallest value in (node (a, (node (l, ll, lr)), right)) = smallest value in (node (l, ll, lr))
smallest value in (node (a, None, right)) = a
result of updating the root of (node (a, left, right)) with b = node (b, left, right)
x squared = x ⋅ x
square_root(x) == power(x, 1 / 2)
x1 = x
x0 = 1
x(m + n) = (xm) ⋅ (xn)
(xm)n = x(m ⋅ n)
(x ⋅ y)n = (xn) ⋅ (yn)
slope of line AB = ((the y coordinate of point B) - (the y coordinate of point A)) / ((the x coordinate of point B) - (the x coordinate of point A))
area of △ABC = area of △BCA
area of △ABC = area of △CAB
area of quadrilateral ABCD = area of quadrilateral BCDA
area of pentagon ABCDE = area of pentagon EABCD
area of hexagon ABCDEF = area of hexagon BCDEFA
area of quadrilateral ABCD = (area of pentagon ABCDX) + (area of △DAX)
area of pentagon ABCDE = (area of quadrilateral ABCD) + (area of △DEA)
area of pentagon ABCDE = (area of pentagon ABCDX) + (area of quadrilateral DEAX)
area of hexagon ABCDEF = (area of hexagon ABCDEX) + (area of quadrilateral EFAX)
sum of bit 0 bit 0 and bit 0 = 0
sum of bit 1 bit 0 and bit 0 = 1
sum of bit 0 bit 1 and bit 0 = 1
sum of bit 1 bit 1 and bit 0 = 0
sum of bit 0 bit 0 and bit 1 = 1
sum of bit 1 bit 0 and bit 1 = 0