Proof: Get Iterate Expr 2
Let's prove the following theorem:
if the following are true:
- expression state at time 2 = "iterate_args"
- arguments stack at time 2 = [ [ 1, [ 3, [ ] ] ], [ ] ]
then the expression at time 3 = 1
Proof:
Given
1 | expression state at time 2 = "iterate_args" |
---|---|
2 | arguments stack at time 2 = [ [ 1, [ 3, [ ] ] ], [ ] ] |
# | Claim | Reason |
---|---|---|
1 | the expression at time (2 + 1) = 1 | if expression state at time 2 = "iterate_args" and arguments stack at time 2 = [ [ 1, [ 3, [ ] ] ], [ ] ], then the expression at time (2 + 1) = 1 |
2 | 2 + 1 = 3 | 2 + 1 = 3 |
3 | the expression at time (2 + 1) = the expression at time 3 | if 2 + 1 = 3, then the expression at time (2 + 1) = the expression at time 3 |
4 | the expression at time 3 = 1 | if the expression at time (2 + 1) = the expression at time 3 and the expression at time (2 + 1) = 1, then the expression at time 3 = 1 |
Comments
Please log in to add comments