Conditional Properties
In each statement, if the test expression is true, then the conclusion expression is also assumed to be true. Conditional properties are used to prove theorems.
if not (el = val), then index of value val in [ node (el, left, right), remain ] with current index idx = index of value val in remain with current index (idx + 1)
if not (el = val), then index of value val in [ node (el, w, p), remain ] with current index idx = index of value val in remain with current index (idx + 1)
if the following are true:
- not (left = val)
- not (right = val)
then find parent index of [ node (el, left, right), remain ] = find parent index of remain
if x = value, then stack [ x, y ] contains value = True
if not (x = value), then stack [ x, y ] contains value = stack y contains value
if entry_key = key, then output of function store_compute where input key is key, value is value, map is [ entry entry_key: entry_value, remaining ], and processed map is kvs = result of dumping kvs to [ entry key: value, remaining ]
if not (entry_key = key), then output of function store_compute where input key is key, value is value, map is [ entry entry_key: entry_value, remaining ], and processed map is kvs = output of function store_compute where input key is key, value is value, map is remaining, and processed map is [ entry entry_key: entry_value, kvs ]
if entry_key = key, then output of function delete_entry where input key is key, map is [ pair (entry_key, value), remaining ], and processed is kvs = result of dumping kvs to remaining
if not (entry_key = key), then output of function delete_entry where input key is key, map is [ pair (entry_key, value), remaining ], and processed is kvs = output of function delete_entry where input key is key, map is remaining, and processed is [ pair (entry_key, value), kvs ]
if (length of stack xs) % 2 = 0, then length of xs is even
if (length of stack xs) % 2 = 1, then length of xs is odd
if i < max_size, then get subtower map[ i, rest ] = get subtower maprest
if not (i < max_size), then get subtower map[ i, rest ] = result
if the following are true:
- not (one = x)
- not (two = x)
then find other one = x
if the following are true:
- the element at index src of stack towers = src_tower
- get subtowersrc_tower = sub_tower
- length of sub_tower is even
then towers of hanoi towers = towers of hanoi top disks towers
if the following are true:
- the element at index src of stack towers = src_tower
- get subtowersrc_tower = sub_tower
- length of sub_tower is odd
then towers of hanoi towers = towers of hanoi top disks towers
if the following are true:
- the element at index src of stack towers = [ 1, rest ]
- the element at index dst of stack towers = dst_tower
then towers of hanoi top towers = move disk towers is even
if the following are true:
- the element at index src of stack towers = [ x, rest ]
- the element at index dst of stack towers = dst_tower
- x > 1
then towers of hanoi top towers = towers of hanoi (move disk towers is even)
if the element at index i of stack tree = node (v, (-1), (-1)), then Height of a tree tree and index i = 1
if the element at index i of stack tree = node (v, left, (-1)), then Height of a tree tree and index i = (Height of a tree tree and index left) + 1
if the element at index i of stack tree = node (v, (-1), right), then Height of a tree tree and index i = (Height of a tree tree and index right) + 1
if the following are true:
- the element at index i of stack tree = node (v, a, b)
- Height of a tree tree and index a > Height of a tree tree and index b
then Height of a tree tree and index i = (Height of a tree tree and index a) + 1
if the following are true:
- the element at index i of stack tree = node (v, a, b)
- Height of a tree tree and index a < Height of a tree tree and index b
then Height of a tree tree and index i = (Height of a tree tree and index b) + 1
if the following are true:
- the element at index i of stack tree = node (v, a, b)
- Height of a tree tree and index a = Height of a tree tree and index b
then Height of a tree tree and index i = (Height of a tree tree and index a) + 1
if the following are true:
- val < a
- the element at index i of stack tree = node (a, left, right)
then output of the bst_insert function where input tree is tree, value is val and index is i = output of the bst_insert function where input tree is tree, value is val and index is left
if the following are true:
- val > a
- the element at index i of stack tree = node (a, left, right)
then output of the bst_insert function where input tree is tree, value is val and index is i = output of the bst_insert function where input tree is tree, value is val and index is right
if the following are true:
- val < a
- the element at index i of stack tree = node (a, (-1), right)
then output of the bst_insert function where input tree is tree, value is val and index is i = result of storing (node (a, (length of stack tree), right)) at index i of stack (result of appending (node (val, (-1), (-1))) to tree)
if the following are true:
- val > a
- the element at index i of stack tree = node (a, left, (-1))
then output of the bst_insert function where input tree is tree, value is val and index is i = result of storing (node (a, left, (length of stack tree))) at index i of stack (result of appending (node (val, (-1), (-1))) to tree)
if the following are true:
- not (left = index)
- not (right = index)
then find referece to node index in tree [ node (x, left, right), rest ] = find referece to node index in tree rest
if find referece to node i in tree tree = False, then find root index in tree = i
if the following are true:
- find root index in tree = ri
- the element at index ri of stack tree = node (root_val, left, right)
- the element at index left of stack tree = node (l_val, l_left, l_right)
- new_val < root_val
- new_val < l_val
then result of inserting new_val to tree tree = result of rotating (output of the bst_insert function where input tree is tree, value is new_val and index is ri) clockwise
if the following are true:
- find root index in tree = ri
- the element at index ri of stack tree = node (root_val, left, right)
- the element at index left of stack tree = node (l_val, l_left, l_right)
- new_val < root_val
- new_val > l_val
then result of inserting new_val to tree tree = result of rotating (result of rotating (output of the bst_insert function where input tree is tree, value is new_val and index is ri) twice) clockwise
if the following are true:
- find root index in tree = ri
- the element at index ri of stack tree = node (root_val, left, right)
- the element at index left of stack tree = node (l_val, l_left, l_right)
then result of rotating tree clockwise = result of storing (node (l_val, l_left, ri)) at index left of stack (result of storing (node (root_val, l_right, right)) at index ri of stack tree)
if the following are true:
- find root index in tree = ri
- the element at index ri of stack tree = node (root_val, left, right)
- the element at index left of stack tree = node (l_val, l_left, g)
- the element at index g of stack tree = node (g_val, g_left, g_right)
then result of rotating tree twice = result of storing (node (root_val, g, right)) at index ri of stack (result of storing (node (g_val, left, g_right)) at index g of stack (result of storing (node (l_val, l_left, g_left)) at index left of stack tree))
if the element at index i of stack tree = node (value, left, right), then find nearest largertree = find nearest largertree
if the following are true:
- val < a
- the element at index i of stack tree = node (a, (-1), right)
then find nearest largertree = i
if the following are true:
- val < a
- the element at index i of stack tree = node (a, left, right)
then find nearest largertree = find nearest largertree
if the following are true:
- val > a
- the element at index i of stack tree = node (a, left, right)
then find nearest largertree = find nearest largertree
if the following are true:
- val = a
- the element at index i of stack tree = node (a, left, right)
then find nearest largertree = find nearest largertree
if the following are true:
- index of value value in tree = i
- the element at index i of stack tree = node (value, (-1), (-1))
- find parent index of tree = p
- the element at index p of stack tree = node (pval, pleft, i)
then pop value from tree tree = result of storing (node (pval, pleft, (-1))) at index p of stack tree
if the following are true:
- index of value value in tree = i
- the element at index i of stack tree = node (value, left, (-1))
- the element at index left of stack tree = node (lvalue, lleft, lright)
- find parent index of tree = p
- the element at index p of stack tree = node (pval, pleft, i)
then pop value from tree tree = result of storing (node (value, (-1), (-1))) at index i of stack (result of storing (node (pval, pleft, left)) at index p of stack tree)
if the following are true:
- index of value value in tree = i
- the element at index i of stack tree = node (value, (-1), right)
- the element at index right of stack tree = node (rvalue, rleft, rright)
- find parent index of tree = p
- the element at index p of stack tree = node (pval, i, pright)
then pop value from tree tree = result of storing (node (value, (-1), (-1))) at index i of stack (result of storing (node (pval, right, pright)) at index p of stack tree)
if the following are true:
- index of value value in tree = i
- find nearest largertree = n
- the element at index n of stack tree = node (larger, nleft, nright)
- the element at index i of stack tree = node (value, left, right)
then pop value from tree tree = result of storing (node (larger, left, right)) at index i of stack (pop larger from tree tree)
if the following are true:
- find root index in tree = ri
- the element at index ri of stack tree = node (rvalue, left, right)
- Height of a tree tree and index left = Height of a tree tree and index right
then result of balancing the tree tree = tree
if the following are true:
- find root index in tree = ri
- the element at index ri of stack tree = node (rvalue, left, right)
- Height of a tree tree and index left > (Height of a tree tree and index right) + 1
- the element at index left of stack tree = node (lvalue, lleft, lright)
- Height of a tree tree and index lleft > Height of a tree tree and index lright
then result of balancing the tree tree = result of rotating tree clockwise
if the following are true:
- find root index in tree = ri
- the element at index ri of stack tree = node (rvalue, left, right)
- Height of a tree tree and index left > (Height of a tree tree and index right) + 1
- the element at index left of stack tree = node (lvalue, lleft, lright)
- Height of a tree tree and index lleft < Height of a tree tree and index lright
then result of balancing the tree tree = result of rotating (result of rotating tree twice) clockwise
if a < b, then output of the merge_stacks function where input stacks are [ a, a_rest ] and [ b, b_rest ], and merged stack is result = output of the merge_stacks function where input stacks are a_rest and [ b, b_rest ], and merged stack is [ a, result ]
if a > b, then output of the merge_stacks function where input stacks are [ a, a_rest ] and [ b, b_rest ], and merged stack is result = output of the merge_stacks function where input stacks are [ a, a_rest ] and b_rest, and merged stack is [ b, result ]
if c > 0, then output of the halve stack function where input stack is [ a, a_rest ], other stack is other, and count is c = output of the halve stack function where input stack is a_rest, other stack is [ a, other ], and count is (c - 1)
if result of halving the stack stack = [ first_half, [ second_half, [ ] ] ], then result of merge sorting stack = result of merging stacks (result of merge sorting first_half) and (result of merge sorting second_half)
if elem = value, then tree [ node (elem, cs), rest ] contains value = True
if not (elem = value), then tree [ node (elem, cs), rest ] contains value = tree rest contains value
if elem = value, then tree [ node (elem, d, p), rest ] contains value = True
if not (elem = value), then tree [ node (elem, d, p), rest ] contains value = tree rest contains value
if tree tree contains value = False, then output of the not_in_tree function where the input tree is tree, the values are [ value, rest ], and the new values are result = output of the not_in_tree function where the input tree is tree, the values are rest, and the new values are [ value, result ]
if tree tree contains value = True, then output of the not_in_tree function where the input tree is tree, the values are [ value, rest ], and the new values are result = output of the not_in_tree function where the input tree is tree, the values are rest, and the new values are result
if the following are true:
- ((length of stack tree) - 1) - index = back_i
- the element at index back_i of stack tree = node (value, cs)
then children of the node at backwards index index of tree tree in graph graph = output of the find_neighbors function where the input graph is graph, node is value, and children are [ ]
if the following are true:
- not (left = value)
- not (right = value)
then output of the find_neighbors function where the input graph is [ pair (left, right), rest ], node is value, and children are result = output of the find_neighbors function where the input graph is rest, node is value, and children are result
if left = value, then output of the find_neighbors function where the input graph is [ pair (left, right), rest ], node is value, and children are result = output of the find_neighbors function where the input graph is rest, node is value, and children are [ right, result ]
if right = value, then output of the find_neighbors function where the input graph is [ pair (left, right), rest ], node is value, and children are result = output of the find_neighbors function where the input graph is rest, node is value, and children are [ left, result ]
if the following are true:
- ((length of stack tree) - 1) - index = back_i
- the element at index back_i of stack tree = node (value, cs)
- elements of numbers that are not in tree tree = new_elements
- result of storing (node (value, new_elements)) at index back_i of stack tree = updated
then result of adding numbers to tree tree as children of the node at backwards index index = result of pushing values new_elements to tree updated
if the following are true:
- children of the node at backwards index i of tree tree in graph graph = children
- result of adding children to tree tree as children of the node at backwards index i = new_tree
then output of the spanning_tree function where the input graph is graph, backwards index is i, and the spanning tree is tree = output of the spanning_tree function where the input graph is graph, backwards index is (i + 1), and the spanning tree is new_tree
if i = (length of stack tree) - 1, then output of the spanning_tree function where the input graph is graph, backwards index is i, and the spanning tree is tree = tree
if the following are true:
- ((length of stack tree) - 1) - index = back_i
- the element at index back_i of stack tree = node (value, distance, previous)
then children of the node at backwards index index of tree tree in graph graph = output of the find_neighbors function where the input graph is graph, node is value, and children are [ ]
if the following are true:
- not (left = value)
- not (right = value)
then output of the find_neighbors function where the input graph is [ edge (left, right, weight), rest ], node is value, and children are result = output of the find_neighbors function where the input graph is rest, node is value, and children are result
if left = value, then output of the find_neighbors function where the input graph is [ edge (left, right, weight), rest ], node is value, and children are result = output of the find_neighbors function where the input graph is rest, node is value, and children are [ pair (right, weight), result ]
if right = value, then output of the find_neighbors function where the input graph is [ edge (left, right, weight), rest ], node is value, and children are result = output of the find_neighbors function where the input graph is rest, node is value, and children are [ pair (left, weight), result ]
if tree tree contains value = False, then output of the separate_nodes function where the input tree is tree, the nodes are [ pair (value, weight), rest ], the existing group is exist, and the new group is new = output of the separate_nodes function where the input tree is tree, the nodes are rest, the existing group is exist, and the new group is [ pair (value, weight), new ]
if index of value value in tree = index, then output of the separate_nodes function where the input tree is tree, the nodes are [ pair (value, weight), rest ], the existing group is exist, and the new group is new = output of the separate_nodes function where the input tree is tree, the nodes are rest, the existing group is [ pair (index, weight), exist ], and the new group is new
if the following are true:
- the element at index child_i of stack tree = node (child_value, child_d, child_prev)
- distance + weight < child_d
- result of storing (node (child_value, (distance + weight), index)) at index child_i of stack tree = updated
then result of updating nodes [ pair (child_i, weight), rest ] in tree tree with parent index index and parent distance distance = result of updating nodes rest in tree updated with parent index index and parent distance distance
if the following are true:
- the element at index child_i of stack tree = node (child_value, child_d, child_prev)
- distance + weight > child_d
then result of updating nodes [ pair (child_i, weight), rest ] in tree tree with parent index index and parent distance distance = result of updating nodes rest in tree tree with parent index index and parent distance distance
if the following are true:
- ((length of stack tree) - 1) - index = back_i
- the element at index back_i of stack tree = node (value, distance, previous)
- result of splitting pairs into nodes that exist in the tree tree and new nodes = pair (exists, new)
- result of updating nodes exists in tree tree with parent index index and parent distance distance = updated
then result of adding or updating children pairs of the node at backwards index index in tree tree = result of pushing nodes new into tree updated where parent is index and parent distance is distance
if the following are true:
- children of the node at backwards index i of tree tree in graph graph = children
- result of adding or updating children children of the node at backwards index i in tree tree = new_tree
then output of the shortest_path function where the input graph is graph, backwards index is i, and tree is tree = output of the shortest_path function where the input graph is graph, backwards index is (i + 1), and tree is new_tree
if i = length of stack tree, then output of the shortest_path function where the input graph is graph, backwards index is i, and tree is tree = tree
if the following are true:
- children of the node top in graph graph = children
- elements of children that are not in tree tree = new_elements
- nodes with values new_elements and parent top = final_elems
- result of dumping final_elems to rest = new_stack
then output of the build_dft_tree function where input graph is graph, tree is tree, and neighbor stack is [ node (top, parent), rest ] = output of the build_dft_tree function where input graph is graph, tree is [ node (top, parent), tree ], and neighbor stack is new_stack
if val < a, then tree (node (a, left, right)) contains val = tree left contains val
if val > a, then tree (node (a, left, right)) contains val = tree right contains val
if val = a, then tree (node (a, left, right)) contains val = True
if val < a, then output of the bst_insert function where the input tree is (node (a, left, right)), value is val, visited is visited, and moves are moves = output of the bst_insert function where the input tree is left, value is val, visited is [ node (a, None, right), visited ], and moves are [ "L", moves ]
if val > a, then output of the bst_insert function where the input tree is (node (a, left, right)), value is val, visited is visited, and moves are moves = output of the bst_insert function where the input tree is right, value is val, visited is [ node (a, left, None), visited ], and moves are [ "R", moves ]
if val < a, then output of the bst_insert function where the input tree is (node (a, None, None)), value is val, visited is visited, and moves are moves = result of building the BST from nodes [ node (a, (node (val, None, None)), None), visited ] and moves moves
if val > a, then output of the bst_insert function where the input tree is (node (a, None, None)), value is val, visited is visited, and moves are moves = result of building the BST from nodes [ node (a, None, (node (val, None, None))), visited ] and moves moves
if height of tree left > height of tree right, then height of tree (node (v, left, right)) = (height of tree left) + 1
if height of tree left < height of tree right, then height of tree (node (v, left, right)) = (height of tree right) + 1
if height of tree left = height of tree right, then height of tree (node (v, left, right)) = (height of tree left) + 1
if the following are true:
- height of tree (node (lv, ll, lr)) > (height of tree right) + 1
- height of tree ll > height of tree lr
then result of balancing the tree (node (v, (node (lv, ll, lr)), right)) = result of rotating (node (v, (node (lv, ll, lr)), right)) clockwise
if the following are true:
- height of tree (node (lv, ll, lr)) > (height of tree right) + 1
- height of tree ll < height of tree lr
then result of balancing the tree (node (v, (node (lv, ll, lr)), right)) = result of rotating (node (v, (node (lv, ll, lr)), right)) twice
if val < a, then output of the bst_delete function where input tree is (node (a, left, right)), value is val, visited is visited, and moves are moves = output of the bst_delete function where input tree is left, value is val, visited is [ node (a, None, right), visited ], and moves are [ "L", moves ]
if val > a, then output of the bst_delete function where input tree is (node (a, left, right)), value is val, visited is visited, and moves are moves = output of the bst_delete function where input tree is right, value is val, visited is [ node (a, left, None), visited ], and moves are [ "R", moves ]
if val = b, then output of the bst_delete function where input tree is (node (a, (node (b, None, (node (c, cl, cr)))), right)), value is val, visited is visited, and moves are moves = result of building the BST from nodes [ node (a, (node (c, cl, cr)), right), visited ] and moves moves
if the following are true:
- val = a
- tree = node (a, (node (l, ll, lr)), (node (r, rl, rr)))
- smallest value in (node (r, rl, rr)) = near
then output of the bst_delete function where input tree is tree, value is val, visited is visited, and moves are moves = result of building the BST from nodes [ result of updating the root of (result of removing near from tree tree) with near, visited ] and moves moves
if xp = z, then logxz = p
if logxz = p, then xp = z