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.
- not (one = x)
- not (two = x)
then find other one = x
- 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
- 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
- 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
- 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)
- 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
- 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
- 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
- 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
- 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
- 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)
- 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)
- 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
- 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
- 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
- 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)
- 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))
- val < a
- the element at index i of stack tree = node (a, (-1), right)
then find nearest largertree = i
- val < a
- the element at index i of stack tree = node (a, left, right)
then find nearest largertree = find nearest largertree
- val > a
- the element at index i of stack tree = node (a, left, right)
then find nearest largertree = find nearest largertree
- val = a
- the element at index i of stack tree = node (a, left, right)
then find nearest largertree = find nearest largertree
- 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
- 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)
- 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)
- 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)
- 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
- 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
- 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
- ((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 [ ]
- 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
- ((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
- 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
- ((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 [ ]
- 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
- 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
- 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
- ((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
- 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
- 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
- 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
- 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
- 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