Proof: Do Class Defs At Unchanged 8
Let's prove the following theorem:
if the following are true:
- expression state at time 8 = "return"
- Class Map at time 8 = [ ]
then Class Map at time 9 = [ ]
Proof:
Given
1 | expression state at time 8 = "return" |
---|---|
2 | Class Map at time 8 = [ ] |
# | Claim | Reason |
---|---|---|
1 | Class Map at time (8 + 1) = Class Map at time 8 | if expression state at time 8 = "return", then Class Map at time (8 + 1) = Class Map at time 8 |
2 | Class Map at time (8 + 1) = [ ] | if Class Map at time (8 + 1) = Class Map at time 8 and Class Map at time 8 = [ ], then Class Map at time (8 + 1) = [ ] |
3 | 8 + 1 = 9 | 8 + 1 = 9 |
4 | Class Map at time (8 + 1) = Class Map at time 9 | if 8 + 1 = 9, then Class Map at time (8 + 1) = Class Map at time 9 |
5 | Class Map at time 9 = [ ] | if Class Map at time (8 + 1) = Class Map at time 9 and Class Map at time (8 + 1) = [ ], then Class Map at time 9 = [ ] |
Comments
Please log in to add comments