How to prove that the pseudo-code of thresholded-A* algorithm from my teacher's book is correct?

Question

I have the following DFS2 pseudo-code, which is used in the pseudo-code of IDA*, from my teacher's book, but I cannot understand why it's correct:

DFS2(N0, f, threshold):

PQInit(PQ) // PQ means Priority Queue, for a pair (c, p) in PQ it represents a path from N0 to c.
PQ.offer(null, N0)

while isEmpty(PQ) is FALSE do
    current, parent := PQ.poll()
    R := next(current, parent)  // return the next child of parent
    
    if R is null then
        continue
    PQ.offer(R)

    Let P be the path from N0 to R.
    if f(P) > threshold then
        continue

    if isGoal(R) then
        return success

    if R in PQ then
        continue
    PQ.offer(null, R)
    
return fail

if I substitute the PQ to a Stack S in the code above, then it's just a non-recursive DFS which I can understand and prove its correctness. Even more I think I have a better version (reordering of the continue-conditions) of the non-recursive DFS:

StackInit(S)
S.push(null, null)               // assume that next(null, null) -> (N0, null)
while isEmpty(S) is FALSE do
    current, parent := S.pop()
    R := next(current, parent)
    if R is null then
        continue
    S.push(R,parent)
    if isVisited(R) then         // if it's visited then it cannot be goal
        continue
    markVisited(R)
    if isGoal(R) then            // if it's a goal then no need to visit its children
        return success
    Let P be the path from N0 to R
    if f(P) > threshold then
        continue
    S.push(null, R)
return fail

I thought this would be perfect since any visited node would not be visited again, but then I realized that revisiting of nodes (In CLRS this is called RELAXING weights of nodes.) is required to achieve A*. Can anyone explain for me why the A*(DFS2) pseudo-code I provided above is correct? And could anyone teach me how to improve my second DFS pseudo-code to make it a thresholded-A*?

In my current understand the nature of A*, which can be seen as a generalization of Dijkstra-shortest path algorithm, is BFS. So given a DONE set (A set of nodes which have been labeled with the shortest/smallest accumulated weight) A* will extend it by the end node of closest adjacent node(Greedy). In DFS2 not all adjacent edges are discovered since it's Depth-First, so how can I prove it that the path found is indeed optimal when it return success?