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