Proof: Get Begin Expr Parent 26
Let's prove the following theorem:
if the following are true:
- expression state at time 26 = "begin_expr"
- the expression at time 26 = self."y" = 0
- parent stack at time 26 = [ ]
then parent stack at time 27 = [ self."y" = 0, [ ] ]
Proof:
Given
1 | expression state at time 26 = "begin_expr" |
---|---|
2 | the expression at time 26 = self."y" = 0 |
3 | parent stack at time 26 = [ ] |
# | Claim | Reason |
---|---|---|
1 | parent stack at time (26 + 1) = [ self."y" = 0, parent stack at time 26 ] | if expression state at time 26 = "begin_expr" and the expression at time 26 = self."y" = 0, then parent stack at time (26 + 1) = [ self."y" = 0, parent stack at time 26 ] |
2 | [ self."y" = 0, parent stack at time 26 ] = [ self."y" = 0, [ ] ] | if parent stack at time 26 = [ ], then [ self."y" = 0, parent stack at time 26 ] = [ self."y" = 0, [ ] ] |
3 | parent stack at time (26 + 1) = [ self."y" = 0, [ ] ] | if parent stack at time (26 + 1) = [ self."y" = 0, parent stack at time 26 ] and [ self."y" = 0, parent stack at time 26 ] = [ self."y" = 0, [ ] ], then parent stack at time (26 + 1) = [ self."y" = 0, [ ] ] |
4 | 26 + 1 = 27 | 26 + 1 = 27 |
5 | parent stack at time (26 + 1) = parent stack at time 27 | if 26 + 1 = 27, then parent stack at time (26 + 1) = parent stack at time 27 |
6 | parent stack at time 27 = [ self."y" = 0, [ ] ] | if parent stack at time (26 + 1) = parent stack at time 27 and parent stack at time (26 + 1) = [ self."y" = 0, [ ] ], then parent stack at time 27 = [ self."y" = 0, [ ] ] |
Comments
Please log in to add comments