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.

Even Length

if (length of stack xs) % 2 = 0, then length of xs is even

Odd Length

if (length of stack xs) % 2 = 1, then length of xs is odd

Add subtower list

if i < max_size, then get subtower map[ i, rest ] = get subtower maprest

Add subtower stop

if not (i < max_size), then get subtower map[ i, rest ] = result

Find Other

if the following are true:

not (one = x)
not (two = x)

then find other one = x

Towers of Hanoi Even

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

Towers of Hanoi Odd

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

Towers of Hanoi Move Top

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

Towers of Hanoi Most Rest

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)

height of leaf

if the element at index i of stack tree = node (v, (-1), (-1)), then Height of a tree tree and index i = 1

height of left child

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

height of right child

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

height when left is larger

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

height when right is larger

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

height when children are the same

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

tree insert move 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 left

tree insert move right

if the following are true:

val > a
the element at index i of stack tree = node (a, left, right)

tree insert left

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)

tree insert right

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)

find node reference next

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

tree root found

if find referece to node i in tree tree = False, then find root index in tree = i

tree insert help

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

tree insert help 2

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

rotate tree 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)

rotate tree counter-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, 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))

find nearest larger value start

if the element at index i of stack tree = node (value, left, right), then find nearest largertree = find nearest largertree

found nearest larger value

if the following are true:

val < a
the element at index i of stack tree = node (a, (-1), right)

then find nearest largertree = i

find nearest larger value less

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

find nearest larger value greater

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

find nearest larger value equal

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

tree delete leaf

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

tree delete single child parent

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)

tree delete single right child parent

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)

tree delete two children parent

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)

tree is already balanced

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

tree left left is taller

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

tree left right is taller

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

merge stacks a is larger

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 ]

merge stacks b is larger

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 ]

halve stack next

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)

merge sort begin

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)

tree contains value

if elem = value, then tree [ node (elem, cs), rest ] contains value = True

tree contains next

if not (elem = value), then tree [ node (elem, cs), rest ] contains value = tree rest contains value

d tree contains value

if elem = value, then tree [ node (elem, d, p), rest ] contains value = True

d tree contains next

if not (elem = value), then tree [ node (elem, d, p), rest ] contains value = tree rest contains value

element is not in tree

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 ]

element is in tree

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

get node children begin

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 [ ]

get node children not found

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

get node children found on left

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 ]

get node children found on right

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 ]

add new tree children

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

construct spanning tree next

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

construct spanning tree finished

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

get d node children begin

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)

get d node children not found

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

get d node children found on left

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 ]

get d node children found on right

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 ]

element is new

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 ]

element exists in tree

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

update node weight

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

leave node weight unchanged

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

add d children to 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)
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

compute shortest path next

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

find shortest path finished

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

construct dfs spanning tree next

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

BST search left

if val < a, then tree (node (a, left, right)) contains val = tree left contains val

BST search right

if val > a, then tree (node (a, left, right)) contains val = tree right contains val

BST search found

if val = a, then tree (node (a, left, right)) contains val = True

tree insert traverse left

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 ]

tree insert traverse right

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 ]

tree insert rebuild 1

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

tree insert rebuild 2

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

height of left is larger

if height of tree left > height of tree right, then height of tree (node (v, left, right)) = (height of tree left) + 1

height of right is larger

if height of tree left < height of tree right, then height of tree (node (v, left, right)) = (height of tree right) + 1

heights are the same

if height of tree left = height of tree right, then height of tree (node (v, left, right)) = (height of tree left) + 1

avl tree rotate 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)) clockwise

avl tree rotate twice

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

tree delete traverse left

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 ]

tree delete traverse right

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 ]

tree delete rebuild 2

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

tree delete rebuild 3

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