Hamiltonian Cycle; Prove: if there's an efficient algorithm to determine that an HC exists, then there's an efficient FIND algorithm

There is just one element missing in your pseudo code: it is not guaranteed that 𝐺 has a Hamilton Cycle.

So you would need to have a first check, before doing anything else, that ensures that it does have a Hamilton Cycle.

If not D(G):
    Return No_Hamilton_Cycle!

Secondly, the algorithm returns a Hamilton Cycle (not the): there can be many alternative Hamilton Cycles in 𝐺, but the order in which you try removing edges, determines which one of those competing Hamilton Cycles you will finally get.

With the above addition, you can be sure that at the start and end of each iteration, 𝐺’ has a Hamilton Cycle: either an iteration will remove an edge and confirm that 𝐺’ still has a Hamilton Cycle, or that removal is undone, so that the state of 𝐺’ is the same at the end as as at the start of that iteration.

When the loop has finished you know that:

1. 𝐺’ has a Hamilton Cycle, because that was true at the end of the last iteration
2. There is no edge you can remove from 𝐺’ and still have a Hamilton Cycle, because you tried removing all those edges without success. Granted, sometimes 𝐺’ still had other edges at that moment of attempt, but that doesn't matter: if an edge is essential for having a Hamilton Cycle in a 𝐺’, then it still is essential after you have removed some other non-essential edges.
3. This algorithm has not added or removed any nodes: 𝐺’ has the same nodes as 𝐺
4. This algorithm has not added any edges: the set of edges of 𝐺’ is a subset of the edges of 𝐺 (possibly equal to it).

From these points we can conclude that if 𝐺 has a Hamilton Cycle, then 𝐺’ is a Hamilton Cycle of 𝐺.

I'm not an expert in formal proofs, so I'll just give some observations that could be useful.

• An invariant for your for loop is that G' always contain an Hamiltonian Cycle, so it must be proved that in G' doesn't contain edges which are not part of the cycle

• There's a theorem that states that the number of edges of an Hamiltonian loop is equal to V + 1. So if you can prove that at the end of the loop there are exactly V + 1 edges you're done. (I don't think this is easy with the algorithm you provided, but maybe it could be with some minor modification)

• If you can formally prove the fact that you restore the edge if and only if it is necessary for the presence of an Hamiltonian cycle than it is immediate that at the end of the loop there won't be edges not part of the cycle