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