Big Step Semantics Editor
Big Step Semantics
Write a proof tree for the following judgement:
Each line of your tree should have the following components:
- a number followed by a period to indicate its depth in the tree. 0 is the root.
- a configuration, in the form < , s > (where is an integer) or as a set of variable assignments. For example, the notation s2 represents .
- A downarrow operator as ||, ||e, or ||b, as appropriate.
- A value
- 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 .
Here are the big step rules.
Proof Tree Editor