# Translation Correctness for Expressions

Recall Evaluating Postfix

## Notation

Functions:

For simplicity we will omit environments mapping variables

- does not affect this proof

We often write X instead of List(X) when X is one element

Also, we often use same symbol '*' for

- operator in the tree
- operator in instruction sequence
- corresponding mathematical operator

## Key Facts

**Evaluation of expressions:**

**Translation:**

Here

- the last occurrence of is the imul instruction
- denotes a tree with node type and children ,

**run-virtual machine**: From definition of and by induction on ,

Of course

where is the result of computing , and

for constant , and

## Correctness Theorem

For every ,

## Attempt at Inductive Proof

Induction on structure of

## Induction Hypothesis

For every expression and every list of integers ,

## Inductive Proof