Not bad. May I suggest a few improvements?

• Distinguish between the algorithm (what you do) and the argument (the proof of why it works).
• Your D, which you say is a list, is better thought of as a map/associative-array from Node to [distance, Node], where the latter Node is the predecessor of the former.
• Start the computation with {start-node -> [0, nil]} in D.
• Define the graph G as a mapping Node -> Set of [distance, Node], where the distance is the edge length from the former to the latter node. This makes the iterative step easier to describe precisely.

The point of Dijkstra's algorithm is that the tentative distances turn out to be final. The way to prove this is to show that - given that it is true of D so far - it is true at the next step too. This is called the inductive hypothesis. Given that it is true of the initial D, which it is, it is true of all the Ds thereafter, including the final one.

Not bad. May I suggest a few improvements?

• Distinguish between the algorithm (what you do) and the argument (the proof of why it works).
• Your D, which you say is a list, is better thought of as a map/associative-array from Node to [distance, Node], where the former Node is the predecessor of the latter.
• Start the computation with {start-node -> [0, nil]} in D.
• Define the graph G as a mapping Node -> Set of [distance, Node], where the distance is the edge length from the former to the latter node. This makes the iterative step easier to describe precisely.

The point of Dijkstra's algorithm is that the tentative distances turn out to be final. The way to prove this is to show that - given that it is true of D so far - it is true at the next step too. This is called the inductive hypothesis. Given that it is true of the initial D, which it is, it is true of all the Ds thereafter, including the final one.

Not bad. May I suggest a few improvements?

• Distinguish between the algorithm (what you do) and the argument (the proof of why it works).
• Your D, which you say is a list, is better thought of as a map/associative-array from Node to [distance, Node], where the latter Node is the predecessor of the former.
• Start the computation with {start-node -> [0, nil]} in D.
• Define the graph G as a mapping Node -> Set of [distance, Node], where the distance is the edge length from the former to the latter node. This makes the iterative step easier to describe precisely.

Not bad. May I suggest a few improvements?

• Distinguish between the algorithm (what you do) and the argument (the proof of why it works).
• Your D, which you say is a list, is better thought of as a map/associative-array from Node to [distance, Node], where the latter Node is the predecessor of the former.
• Start the computation with {start-node -> [0, nil]} in D.
• Define the graph G as a mapping Node -> Set of [distance, Node], where the distance is the edge length from the former to the latter node. This makes the iterative step easier to describe precisely.

The point of Dijkstra's algorithm is that the tentative distances turn out to be final. The way to prove this is to show that - given that it is true of D so far - it is true at the next step too. This is called the inductive hypothesis. Given that it is true of the initial D, which it is, it is true of all the Ds thereafter, including the final one.