Proofs

• expression state at time 16 = "return"
• arguments stack at time 16 = [ [ 1, [ ] ], [ ] ]

then arguments stack at time 17 = [ [ 1, [ ] ], [ ] ]

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

then Class Map at time 17 = [ ]

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

then Python Object Store at time 17 = [ ]

• expression state at time 16 = "return"
• Control Map at time 16 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 17 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Python Object Store at time 18 = [ ]

• expression state at time 17 = "iterate_args"
• Control Map at time 17 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 18 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Class Map at time 18 = [ ]

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

then Python Object Store at time 19 = [ ]

• expression state at time 18 = "begin_expr"
• Control Map at time 18 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 19 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Class Map at time 19 = [ ]

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

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

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

then Class Map at time 20 = [ ]

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

then Python Object Store at time 20 = [ ]

• expression state at time 19 = "return"
• Control Map at time 19 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 20 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Python Object Store at time 21 = [ ]

• expression state at time 20 = "iterate_args"
• Control Map at time 20 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 21 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Class Map at time 21 = [ ]

• expression state at time 21 = "call_function_begin"
• the expression at time 21 = __add__(a, 1)
• Python Object Store at time 21 = [ ]

then Python Object Store at time 22 = [ ]

• expression state at time 21 = "call_function_begin"
• arguments stack at time 21 = [ ]

then arguments stack at time 22 = [ ]

• expression state at time 21 = "call_function_begin"
• Control Map at time 21 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 22 = [ entry 0: (pair ("while", 2)), [ ] ]

• expression state at time 21 = "call_function_begin"
• Class Map at time 21 = [ ]

then Class Map at time 22 = [ ]

• the line at time 22 = 3
• the tab at time 22 = 1
• statement at line 3, tab 1 = a = __add__(a, 1)
• expression state at time 22 = "end_expr"
• Variables Map at time 22 = [ entry a: 0, [ ] ]
• Return Value at time 22 = 1

then Variables Map at time 23 = [ entry a: 1, [ ] ]

• the line at time 22 = 3
• the tab at time 22 = 1
• statement at line 3, tab 1 = a = __add__(a, 1)
• expression state at time 22 = "end_expr"

then the line at time 23 = 4

• the line at time 22 = 3
• the tab at time 22 = 1
• statement at line 3, tab 1 = a = __add__(a, 1)
• expression state at time 22 = "end_expr"

then the tab at time 23 = 1

• the line at time 22 = 3
• the tab at time 22 = 1
• statement at line 3, tab 1 = a = __add__(a, 1)
• 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 = 1
• statement at line 3, tab 1 = a = __add__(a, 1)
• Control Map at time 22 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 23 = [ entry 0: (pair ("while", 2)), [ ] ]

• the line at time 22 = 3
• the tab at time 22 = 1
• statement at line 3, tab 1 = a = __add__(a, 1)
• Class Map at time 22 = [ ]

then Class Map at time 23 = [ ]

• the line at time 23 = 4
• the tab at time 23 = 1
• number of lines = 3
• Control Map at time 23 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 24 = [ entry 0: (pair ("while", 2)), [ ] ]

• the line at time 23 = 4
• the tab at time 23 = 1
• number of lines = 3
• Control Map at time 23 = [ entry 0: (pair ("while", 2)), [ ] ]
• 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
• number of lines = 3
• Control Map at time 23 = [ entry 0: (pair ("while", 2)), [ ] ]
• Class Map at time 23 = [ ]

then Class Map at time 24 = [ ]

• the line at time 24 = 2
• the tab at time 24 = 0
• statement at line 2, tab 0 = while __lt__(a, 2):
• expression state at time 24 = "not_expr"

then the expression at time 25 = __lt__(a, 2)

• the line at time 24 = 2
• the tab at time 24 = 0
• statement at line 2, tab 0 = while __lt__(a, 2):
• expression state at time 24 = "not_expr"

then expression state at time 25 = "begin_expr"

• the line at time 24 = 2
• the tab at time 24 = 0
• statement at line 2, tab 0 = while __lt__(a, 2):
• expression state at time 24 = "not_expr"

then the line at time 25 = 2

• the line at time 24 = 2
• the tab at time 24 = 0
• statement at line 2, tab 0 = while __lt__(a, 2):
• expression state at time 24 = "not_expr"

then the tab at time 25 = 0

• the line at time 24 = 2
• the tab at time 24 = 0
• statement at line 2, tab 0 = while __lt__(a, 2):
• expression state at time 24 = "not_expr"

then Value Stack at time 25 = [ ]

• the line at time 24 = 2
• the tab at time 24 = 0
• statement at line 2, tab 0 = while __lt__(a, 2):
• expression state at time 24 = "not_expr"

then parent stack at time 25 = [ ]

• the line at time 24 = 2
• the tab at time 24 = 0
• statement at line 2, tab 0 = while __lt__(a, 2):
• expression state at time 24 = "not_expr"

then arguments stack at time 25 = [ ]

• the line at time 24 = 2
• the tab at time 24 = 0
• statement at line 2, tab 0 = while __lt__(a, 2):
• expression state at time 24 = "not_expr"
• Python Object Store at time 24 = [ ]

then Python Object Store at time 25 = [ ]

• the line at time 24 = 2
• the tab at time 24 = 0
• statement at line 2, tab 0 = while __lt__(a, 2):
• expression state at time 24 = "not_expr"
• Control Map at time 24 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 25 = [ entry 0: (pair ("while", 2)), [ ] ]

• the line at time 24 = 2
• the tab at time 24 = 0
• statement at line 2, tab 0 = while __lt__(a, 2):
• Class Map at time 24 = [ ]

then Class Map at time 25 = [ ]

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

then Python Object Store at time 26 = [ ]

• expression state at time 25 = "begin_expr"
• Control Map at time 25 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 26 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Class Map at time 26 = [ ]

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

then Python Object Store at time 27 = [ ]

• expression state at time 26 = "iterate_args"
• Control Map at time 26 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 27 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Class Map at time 27 = [ ]

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

then Python Object Store at time 28 = [ ]

• expression state at time 27 = "begin_expr"
• Control Map at time 27 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 28 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Class Map at time 28 = [ ]

• expression state at time 28 = "return"
• arguments stack at time 28 = [ [ 2, [ ] ], [ ] ]

then arguments stack at time 29 = [ [ 2, [ ] ], [ ] ]

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

then Class Map at time 29 = [ ]

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

then Python Object Store at time 29 = [ ]

• expression state at time 28 = "return"
• Control Map at time 28 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 29 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Python Object Store at time 30 = [ ]

• expression state at time 29 = "iterate_args"
• Control Map at time 29 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 30 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Class Map at time 30 = [ ]

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

then Python Object Store at time 31 = [ ]

• expression state at time 30 = "begin_expr"
• Control Map at time 30 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 31 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Class Map at time 31 = [ ]

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

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

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

then Class Map at time 32 = [ ]

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

then Python Object Store at time 32 = [ ]

• expression state at time 31 = "return"
• Control Map at time 31 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 32 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Python Object Store at time 33 = [ ]

• expression state at time 32 = "iterate_args"
• Control Map at time 32 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 33 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Class Map at time 33 = [ ]

• expression state at time 33 = "call_function_begin"
• the expression at time 33 = __lt__(a, 2)
• Python Object Store at time 33 = [ ]

then Python Object Store at time 34 = [ ]

• expression state at time 33 = "call_function_begin"
• arguments stack at time 33 = [ ]

then arguments stack at time 34 = [ ]

• expression state at time 33 = "call_function_begin"
• Control Map at time 33 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 34 = [ entry 0: (pair ("while", 2)), [ ] ]

• expression state at time 33 = "call_function_begin"
• Class Map at time 33 = [ ]

then Class Map at time 34 = [ ]

• the line at time 34 = 2
• the tab at time 34 = 0
• statement at line 2, tab 0 = while __lt__(a, 2):
• expression state at time 34 = "end_expr"
• Return Value at time 34 = True
• Control Map at time 34 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 35 = [ entry 0: (pair ("while", 2)), [ ] ]

• the line at time 34 = 2
• the tab at time 34 = 0
• statement at line 2, tab 0 = while __lt__(a, 2):
• Class Map at time 34 = [ ]

then Class Map at time 35 = [ ]

• the line at time 34 = 2
• the tab at time 34 = 0
• statement at line 2, tab 0 = while __lt__(a, 2):
• expression state at time 34 = "end_expr"
• Python Object Store at time 34 = [ ]

then Python Object Store at time 35 = [ ]

• the line at time 35 = 3
• the tab at time 35 = 1
• statement at line 3, tab 1 = a = __add__(a, 1)
• expression state at time 35 = "not_expr"

then arguments stack at time 36 = [ ]

• the line at time 35 = 3
• the tab at time 35 = 1
• statement at line 3, tab 1 = a = __add__(a, 1)
• expression state at time 35 = "not_expr"
• Python Object Store at time 35 = [ ]

then Python Object Store at time 36 = [ ]

• the line at time 35 = 3
• the tab at time 35 = 1
• statement at line 3, tab 1 = a = __add__(a, 1)
• Control Map at time 35 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 36 = [ entry 0: (pair ("while", 2)), [ ] ]

• the line at time 35 = 3
• the tab at time 35 = 1
• statement at line 3, tab 1 = a = __add__(a, 1)
• Class Map at time 35 = [ ]

then Class Map at time 36 = [ ]

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

then Python Object Store at time 37 = [ ]

• expression state at time 36 = "begin_expr"
• Control Map at time 36 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 37 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Class Map at time 37 = [ ]

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

then Python Object Store at time 38 = [ ]

• expression state at time 37 = "iterate_args"
• Control Map at time 37 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 38 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Class Map at time 38 = [ ]

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

then Python Object Store at time 39 = [ ]

• expression state at time 38 = "begin_expr"
• Control Map at time 38 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 39 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Class Map at time 39 = [ ]

• expression state at time 39 = "return"
• arguments stack at time 39 = [ [ 1, [ ] ], [ ] ]

then arguments stack at time 40 = [ [ 1, [ ] ], [ ] ]

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

then Class Map at time 40 = [ ]

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

then Python Object Store at time 40 = [ ]

• expression state at time 39 = "return"
• Control Map at time 39 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 40 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Python Object Store at time 41 = [ ]

• expression state at time 40 = "iterate_args"
• Control Map at time 40 = [ entry 0: (pair ("while", 2)), [ ] ]

then Control Map at time 41 = [ entry 0: (pair ("while", 2)), [ ] ]

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

then Class Map at time 41 = [ ]

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

then Python Object Store at time 42 = [ ]