Proofs

• the line at time 22 = 3
• the tab at time 22 = 0
• statement at line 3, tab 0 = elif __eq__(3, 3):
• expression state at time 22 = "end_expr"
• Python Object Store at time 22 = [ ]

then Python Object Store at time 23 = [ ]

• the line at time 22 = 3
• the tab at time 22 = 0
• statement at line 3, tab 0 = elif __eq__(3, 3):
• expression state at time 22 = "end_expr"
• Return Value at time 22 = True
• Control Map at time 22 = [ pair ("if", False), [ ] ]

then Control Map at time 23 = [ pair ("if", True), [ ] ]

• the line at time 23 = 4
• the tab at time 23 = 1
• statement at line 4, tab 1 = a = 8
• 8 is constant
• stack at time 23 = [ ]

then stack at time 24 = [ ]

• the line at time 23 = 4
• the tab at time 23 = 1
• statement at line 4, tab 1 = a = 8
• 8 is constant
• Python Object Store at time 23 = [ ]

then Python Object Store at time 24 = [ ]

• the line at time 23 = 4
• the tab at time 23 = 1
• statement at line 4, tab 1 = a = 8
• Control Map at time 23 = [ pair ("if", True), [ ] ]

then Control Map at time 24 = [ pair ("if", True), [ ] ]

• the line at time 23 = 4
• the tab at time 23 = 1
• statement at line 4, tab 1 = a = 8
• Class Map at time 23 = [ ]

then Class Map at time 24 = [ ]

• the line at time 24 = 5
• the tab at time 24 = 1
• statement at line 5, tab 0 = else:
• Control Map at time 24 = [ pair ("if", True), [ ] ]

then Control Map at time 25 = [ pair ("if", True), [ ] ]

• the line at time 24 = 5
• the tab at time 24 = 1
• statement at line 5, tab 0 = else:

then expression state at time 25 = "not_expr"

• the line at time 24 = 5
• the tab at time 24 = 1
• statement at line 5, tab 0 = else:
• Python Object Store at time 24 = [ ]
• Control Map at time 24 = [ entry 0: (pair ("if", True)), [ ] ]

then Python Object Store at time 25 = [ ]

• the line at time 24 = 5
• the tab at time 24 = 1
• statement at line 5, tab 0 = else:
• stack at time 24 = [ ]
• Control Map at time 24 = [ entry 0: (pair ("if", True)), [ ] ]

then stack at time 25 = [ ]

• the line at time 24 = 5
• the tab at time 24 = 1
• statement at line 5, tab 0 = else:
• Variables Map at time 24 = [ entry a: 8, [ ] ]
• Control Map at time 24 = [ entry 0: (pair ("if", True)), [ ] ]

then Variables Map at time 25 = [ entry a: 8, [ ] ]

• the line at time 24 = 5
• the tab at time 24 = 1
• statement at line 5, tab 0 = else:
• Class Map at time 24 = [ ]
• Control Map at time 24 = [ entry 0: (pair ("if", True)), [ ] ]

then Class Map at time 25 = [ ]

• the line at time 25 = 5
• the tab at time 25 = 0
• statement at line 5, tab 0 = else:
• Python Object Store at time 25 = [ ]

then Python Object Store at time 26 = [ ]

• the line at time 25 = 5
• the tab at time 25 = 0
• statement at line 5, tab 0 = else:
• Control Map at time 25 = [ pair ("if", True), [ ] ]

then Control Map at time 26 = [ pair ("if", True), [ ] ]

• the line at time 25 = 5
• the tab at time 25 = 0
• statement at line 5, tab 0 = else:
• Class Map at time 25 = [ ]

then Class Map at time 26 = [ ]

• the line at time 25 = 5
• the tab at time 25 = 0
• statement at line 5, tab 0 = else:
• expression state at time 25 = "not_expr"

then expression state at time 26 = "not_expr"

• the line at time 26 = 6
• the tab at time 26 = 0
• statement at line 6, tab 1 = a = 9
• Variables Map at time 26 = [ entry a: 8, [ ] ]

then Variables Map at time 27 = [ entry a: 8, [ ] ]

• the line at time 26 = 6
• the tab at time 26 = 0
• statement at line 6, tab 1 = a = 9
• stack at time 26 = [ ]

then stack at time 27 = [ ]

• the line at time 26 = 6
• the tab at time 26 = 0
• statement at line 6, tab 1 = a = 9
• Python Object Store at time 26 = [ ]

then Python Object Store at time 27 = [ ]

• the line at time 26 = 6
• the tab at time 26 = 0
• statement at line 6, tab 1 = a = 9
• Control Map at time 26 = [ pair ("if", True), [ ] ]

then Control Map at time 27 = [ pair ("if", True), [ ] ]

• the line at time 26 = 6
• the tab at time 26 = 0
• statement at line 6, tab 1 = a = 9
• Class Map at time 26 = [ ]

then Class Map at time 27 = [ ]

• the line at time 0 = 1
• the tab at time 0 = 0
• statement at line 1, tab 0 = if __eq__(1, 3):
• expression state at time 0 = "not_expr"

then the expression at time 1 = __eq__(1, 3)

• the line at time 0 = 1
• the tab at time 0 = 0
• statement at line 1, tab 0 = if __eq__(1, 3):
• expression state at time 0 = "not_expr"

then expression state at time 1 = "begin_expr"

• the line at time 0 = 1
• the tab at time 0 = 0
• statement at line 1, tab 0 = if __eq__(1, 3):
• expression state at time 0 = "not_expr"

then the line at time 1 = 1

• the line at time 0 = 1
• the tab at time 0 = 0
• statement at line 1, tab 0 = if __eq__(1, 3):
• expression state at time 0 = "not_expr"

then the tab at time 1 = 0

• the line at time 0 = 1
• the tab at time 0 = 0
• statement at line 1, tab 0 = if __eq__(1, 3):
• expression state at time 0 = "not_expr"

then Value Stack at time 1 = [ ]

• the line at time 0 = 1
• the tab at time 0 = 0
• statement at line 1, tab 0 = if __eq__(1, 3):
• expression state at time 0 = "not_expr"

then parent stack at time 1 = [ ]

• the line at time 0 = 1
• the tab at time 0 = 0
• statement at line 1, tab 0 = if __eq__(1, 3):
• expression state at time 0 = "not_expr"

then arguments stack at time 1 = [ ]

• the line at time 0 = 1
• the tab at time 0 = 0
• statement at line 1, tab 0 = if __eq__(1, 3):
• expression state at time 0 = "not_expr"
• Python Object Store at time 0 = [ ]

then Python Object Store at time 1 = [ ]

• the line at time 0 = 1
• the tab at time 0 = 0
• statement at line 1, tab 0 = if __eq__(1, 3):
• expression state at time 0 = "not_expr"
• Control Map at time 0 = [ ]

then Control Map at time 1 = [ ]

• the line at time 0 = 1
• the tab at time 0 = 0
• statement at line 1, tab 0 = if __eq__(1, 3):
• Variables Map at time 0 = [ ]

then Variables Map at time 1 = [ ]

• the line at time 0 = 1
• the tab at time 0 = 0
• statement at line 1, tab 0 = if __eq__(1, 3):
• stack at time 0 = [ ]

then stack at time 1 = [ ]

• the line at time 0 = 1
• the tab at time 0 = 0
• statement at line 1, tab 0 = if __eq__(1, 3):
• Class Map at time 0 = [ ]

then Class Map at time 1 = [ ]

• expression state at time 1 = "begin_expr"
• the expression at time 1 = __eq__(1, 3)
• Value Stack at time 1 = [ ]

then Value Stack at time 2 = [ [ ], [ ] ]

• expression state at time 1 = "begin_expr"
• the expression at time 1 = __eq__(1, 3)
• parent stack at time 1 = [ ]

then parent stack at time 2 = [ __eq__(1, 3), [ ] ]

• expression state at time 1 = "begin_expr"
• the expression at time 1 = __eq__(1, 3)
• arguments stack at time 1 = [ ]

then arguments stack at time 2 = [ [ 1, [ 3, [ ] ] ], [ ] ]

• expression state at time 1 = "begin_expr"
• the expression at time 1 = __eq__(1, 3)

then expression state at time 2 = "iterate_args"

• expression state at time 1 = "begin_expr"
• the expression at time 1 = __eq__(1, 3)

then the expression at time 2 = __eq__(1, 3)

• expression state at time 1 = "begin_expr"
• Variables Map at time 1 = [ ]

then Variables Map at time 2 = [ ]

• expression state at time 1 = "begin_expr"
• the line at time 1 = 1

then the line at time 2 = 1

• expression state at time 1 = "begin_expr"
• the tab at time 1 = 0

then the tab at time 2 = 0

• expression state at time 1 = "begin_expr"
• stack at time 1 = [ ]

then stack at time 2 = [ ]

• expression state at time 1 = "begin_expr"
• Python Object Store at time 1 = [ ]

then Python Object Store at time 2 = [ ]

• expression state at time 1 = "begin_expr"
• Control Map at time 1 = [ ]

then Control Map at time 2 = [ ]

• expression state at time 1 = "begin_expr"
• Class Map at time 1 = [ ]

then Class Map at time 2 = [ ]

• expression state at time 2 = "iterate_args"
• arguments stack at time 2 = [ [ 1, [ 3, [ ] ] ], [ ] ]

then the expression at time 3 = 1

• expression state at time 2 = "iterate_args"
• arguments stack at time 2 = [ [ 1, [ 3, [ ] ] ], [ ] ]

then arguments stack at time 3 = [ [ 3, [ ] ], [ ] ]

• expression state at time 2 = "iterate_args"
• arguments stack at time 2 = [ [ 1, [ 3, [ ] ] ], [ ] ]

then expression state at time 3 = "begin_expr"

• expression state at time 2 = "iterate_args"
• arguments stack at time 2 = [ [ 1, [ 3, [ ] ] ], [ ] ]
• parent stack at time 2 = [ __eq__(1, 3), [ ] ]

then parent stack at time 3 = [ __eq__(1, 3), [ ] ]

• expression state at time 2 = "iterate_args"
• Value Stack at time 2 = [ [ ], [ ] ]

then Value Stack at time 3 = [ [ ], [ ] ]

• expression state at time 2 = "iterate_args"
• the line at time 2 = 1

then the line at time 3 = 1

• expression state at time 2 = "iterate_args"
• the tab at time 2 = 0

then the tab at time 3 = 0

• expression state at time 2 = "iterate_args"
• stack at time 2 = [ ]

then stack at time 3 = [ ]

• expression state at time 2 = "iterate_args"
• Python Object Store at time 2 = [ ]

then Python Object Store at time 3 = [ ]

• expression state at time 2 = "iterate_args"
• Control Map at time 2 = [ ]

then Control Map at time 3 = [ ]

• expression state at time 2 = "iterate_args"
• Variables Map at time 2 = [ ]

then Variables Map at time 3 = [ ]

• expression state at time 2 = "iterate_args"
• Class Map at time 2 = [ ]

then Class Map at time 3 = [ ]

• the expression at time 3 = 1
• expression state at time 3 = "begin_expr"
• 1 is constant
• parent stack at time 3 = [ __eq__(1, 3), [ ] ]

then expression state at time 4 = "return"

• the expression at time 3 = 1
• expression state at time 3 = "begin_expr"
• 1 is constant
• Value Stack at time 3 = [ [ ], [ ] ]

then Value Stack at time 4 = [ [ ], [ ] ]

• the expression at time 3 = 1
• expression state at time 3 = "begin_expr"
• 1 is constant
• arguments stack at time 3 = [ [ 3, [ ] ], [ ] ]

then arguments stack at time 4 = [ [ 3, [ ] ], [ ] ]

• expression state at time 3 = "begin_expr"
• the expression at time 3 = 1
• 1 is constant

then Return Value at time 4 = 1

• expression state at time 3 = "begin_expr"
• the expression at time 3 = 1
• 1 is constant
• parent stack at time 3 = [ __eq__(1, 3), [ ] ]

then parent stack at time 4 = [ __eq__(1, 3), [ ] ]

• expression state at time 3 = "begin_expr"
• the line at time 3 = 1

then the line at time 4 = 1

• expression state at time 3 = "begin_expr"
• the tab at time 3 = 0

then the tab at time 4 = 0

• expression state at time 3 = "begin_expr"
• stack at time 3 = [ ]

then stack at time 4 = [ ]

• expression state at time 3 = "begin_expr"
• Python Object Store at time 3 = [ ]

then Python Object Store at time 4 = [ ]

• expression state at time 3 = "begin_expr"
• Control Map at time 3 = [ ]

then Control Map at time 4 = [ ]

• expression state at time 3 = "begin_expr"
• Variables Map at time 3 = [ ]

then Variables Map at time 4 = [ ]

• expression state at time 3 = "begin_expr"
• Class Map at time 3 = [ ]

then Class Map at time 4 = [ ]

• expression state at time 4 = "return"
• Value Stack at time 4 = [ [ ], [ ] ]
• Return Value at time 4 = 1

then Value Stack at time 5 = [ [ 1, [ ] ], [ ] ]

• expression state at time 4 = "return"
• Variables Map at time 4 = [ ]

then Variables Map at time 5 = [ ]

• expression state at time 4 = "return"
• the line at time 4 = 1

then the line at time 5 = 1

• expression state at time 4 = "return"
• the tab at time 4 = 0

then the tab at time 5 = 0

• expression state at time 4 = "return"
• arguments stack at time 4 = [ [ 3, [ ] ], [ ] ]

then arguments stack at time 5 = [ [ 3, [ ] ], [ ] ]

• expression state at time 4 = "return"
• parent stack at time 4 = [ __eq__(1, 3), [ ] ]

then parent stack at time 5 = [ __eq__(1, 3), [ ] ]

• expression state at time 4 = "return"
• stack at time 4 = [ ]

then stack at time 5 = [ ]

• expression state at time 4 = "return"
• Class Map at time 4 = [ ]

then Class Map at time 5 = [ ]

• expression state at time 4 = "return"
• Python Object Store at time 4 = [ ]

then Python Object Store at time 5 = [ ]

• expression state at time 4 = "return"
• Control Map at time 4 = [ ]

then Control Map at time 5 = [ ]

• expression state at time 5 = "iterate_args"
• arguments stack at time 5 = [ [ 3, [ ] ], [ ] ]

then the expression at time 6 = 3

• expression state at time 5 = "iterate_args"
• arguments stack at time 5 = [ [ 3, [ ] ], [ ] ]

then arguments stack at time 6 = [ [ ], [ ] ]

• expression state at time 5 = "iterate_args"
• arguments stack at time 5 = [ [ 3, [ ] ], [ ] ]

then expression state at time 6 = "begin_expr"

• expression state at time 5 = "iterate_args"
• arguments stack at time 5 = [ [ 3, [ ] ], [ ] ]
• parent stack at time 5 = [ __eq__(1, 3), [ ] ]

then parent stack at time 6 = [ __eq__(1, 3), [ ] ]

• expression state at time 5 = "iterate_args"
• Value Stack at time 5 = [ [ 1, [ ] ], [ ] ]

then Value Stack at time 6 = [ [ 1, [ ] ], [ ] ]

• expression state at time 5 = "iterate_args"
• the line at time 5 = 1

then the line at time 6 = 1

• expression state at time 5 = "iterate_args"
• the tab at time 5 = 0

then the tab at time 6 = 0

• expression state at time 5 = "iterate_args"
• stack at time 5 = [ ]

then stack at time 6 = [ ]

• expression state at time 5 = "iterate_args"
• Python Object Store at time 5 = [ ]

then Python Object Store at time 6 = [ ]

• expression state at time 5 = "iterate_args"
• Control Map at time 5 = [ ]

then Control Map at time 6 = [ ]

• expression state at time 5 = "iterate_args"
• Variables Map at time 5 = [ ]

then Variables Map at time 6 = [ ]

• expression state at time 5 = "iterate_args"
• Class Map at time 5 = [ ]

then Class Map at time 6 = [ ]

• the expression at time 6 = 3
• expression state at time 6 = "begin_expr"
• 3 is constant
• parent stack at time 6 = [ __eq__(1, 3), [ ] ]

then expression state at time 7 = "return"

• the expression at time 6 = 3
• expression state at time 6 = "begin_expr"
• 3 is constant
• Value Stack at time 6 = [ [ 1, [ ] ], [ ] ]

then Value Stack at time 7 = [ [ 1, [ ] ], [ ] ]

• the expression at time 6 = 3
• expression state at time 6 = "begin_expr"
• 3 is constant
• arguments stack at time 6 = [ [ ], [ ] ]

then arguments stack at time 7 = [ [ ], [ ] ]

• expression state at time 6 = "begin_expr"
• the expression at time 6 = 3
• 3 is constant

then Return Value at time 7 = 3

• expression state at time 6 = "begin_expr"
• the expression at time 6 = 3
• 3 is constant
• parent stack at time 6 = [ __eq__(1, 3), [ ] ]

then parent stack at time 7 = [ __eq__(1, 3), [ ] ]

• expression state at time 6 = "begin_expr"
• the line at time 6 = 1

then the line at time 7 = 1

• expression state at time 6 = "begin_expr"
• the tab at time 6 = 0

then the tab at time 7 = 0