Properties
Properties are true expressions. They are used to prove theorems
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 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, [ ] ]
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
sum of bit 0 bit 1 and bit 1 = 0
sum of bit 1 bit 1 and bit 1 = 1
carry on sum of bit 0 bit 0 and 0 = 0
carry on sum of bit 1 bit 0 and 0 = 0
carry on sum of bit 0 bit 1 and 0 = 0
carry on sum of bit 1 bit 1 and 0 = 1
carry on sum of bit 0 bit 0 and 1 = 0
carry on sum of bit 1 bit 0 and 1 = 1
carry on sum of bit 0 bit 1 and 1 = 1
carry on sum of bit 1 bit 1 and 1 = 1
sum of (empty list) (empty list) and carry bit 0 = empty list
sum of (empty list) (empty list) and carry bit 1 = list 1 and (empty list)
sum of (list x and xs) (empty list) and carry bit 0 = list x and xs
sum of (list 0 and xs) (empty list) and carry bit 1 = list 1 and xs
sum of (list 1 and xs) (empty list) and carry bit 1 = list 0 and (sum of xs (empty list) and carry bit 1)
sum of (empty list) (list y and ys) and carry bit 0 = list y and ys
sum of (empty list) (list 0 and ys) and carry bit 1 = list 1 and ys
sum of (empty list) (list 1 and ys) and carry bit 1 = list 0 and (sum of (empty list) ys and carry bit 1)
sum of (list x and xs) (list y and ys) and carry bit carry = list (sum of bit x bit y and bit carry) and (sum of xs ys and carry bit (carry on sum of bit x bit y and carry))