算法 4 中的双栈算数表达式求值算法

《算法（第四版）》中介绍了 Dijkstra 双栈算术表达式求值算法：

public class Evaluate
{
    public static void main(String[] args)
    {
      Stack<String> ops  = new Stack<String>();
      Stack<Double> vals = new Stack<Double>();
      while (! StdIn.isEmpty())
      {  // 读取字符，如果是运算符则压入栈
          String s = StdIn.readString();
          if       (s.equals("("))                 ;
          else if (s.equals("+"))    ops.push(s);
          else if (s.equals("-"))    ops.push(s);
          else if (s.equals("*"))    ops.push(s);
          else if (s.equals("/"))    ops.push(s);
          else if (s.equals("sqrt")) ops.push(s);
          else if (s.equals(")"))
          {  // 如果字符为")"，弹出运算符和操作数，计算结果并压入栈
            String op = ops.pop();
            double v = vals.pop();
            if       (op.equals("+"))    v = vals.pop() + v;
            else if (op.equals("-"))    v = vals.pop() - v;
            else if (op.equals("*"))    v = vals.pop() * v;
            else if (op.equals("/"))    v = vals.pop() / v;
            else if (op.equals("sqrt")) v = Math.sqrt(v);
            vals.push(v);
          }  // 如果字符既非运算符也不是括号，将它作为 double 值压入栈
          else vals.push(Double.parseDouble(s));
      }
      StdOut.println(vals.pop());
    }
}

书中写道：

要证明它能够计算得到正确的值很简单：每当算法遇到一个被括号包围并由一个运算符和两个操作数组成的子表达式时，它都将运算符和操作数的计算结果压入操作数栈。这样的结果就好像在输入中用这个值代替了该子表达式，因此用这个值代替子表达式得到的结果和原表达式相同。我们可以反复应用这个规律并得到一个最终值。例如，用该算法计算以下表达式得到的结果都是相同的：

( 1 + ( ( 2 + 3 ) ＊ ( 4 ＊ 5 ) ) )
( 1 + ( 5 ＊ ( 4 ＊ 5 ) ) )
( 1 + ( 5 ＊ 20 ) )
( 1 + 100 )
101

我懂得它的意思，但总的来说，我觉得这种解释还是偏向于直观，并不算是一种严谨的证明（比较看重准确的人应该都能够理解这种情感）。所以我的问题是，如何真正证明它？或者至少是给出一个更加抽象的说明？

我尝试用循环不变式 /数学归纳法来证明，但没能理出一个清晰的思路。

如果可以的话，最好能够用偏数学的语言来说明，以避免歧义并趋于准确（当然，能够给出一个直观的解释以帮助理解也是很好的）。谢谢。