# Big Step Semantics

Write a proof tree for the following judgement:

$\lt \mathtt{if}\ x \gt y\ \mathtt{then}\ m:=x * x\ \mathtt{else}\ m := y * y\ \mathtt{fi}, \{ x:=10, y:=20 \} \gt \Downarrow \{ x:=10, y:=20, m:=400 \}$

Each line of your tree should have the following components:

1. a number followed by a period to indicate its depth in the tree. 0 is the root.
2. a configuration, in the form < $stmt$, s$n$ > (where $n$ is an integer) or as a set of variable assignments. For example, the notation s2 represents $\sigma_2$.
3. A downarrow operator as ||, ||e, or ||b, as appropriate.
4. A value
5. A rule name in parenthesis.

If you use s or s1, etc. in your proof tree, you must follow the tree with their expanded out definitions.

The starter code shows a valid tree for a proof of $\lt m := x + 1, \sigma \gt \Downarrow \sigma_2$.

Here are the big step rules.

# Proof Tree Editor

Score: 29.56%
$\frac{\frac{\frac{}{\displaystyle \Downarrow_e 3} \textstyle \mathrm{V\small{AR}} \quad \frac{}{\displaystyle <1,\sigma_{}> \Downarrow_e 1} \textstyle \mathrm{C\small{ONST}}}{\displaystyle \Downarrow_e 10}\textstyle \mathrm{A\small{RITH}}}{\displaystyle \Downarrow \sigma_{2}}\textstyle \mathrm{A\small{SSIGN}}$