Proofs

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

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

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

then Class Map at time 42 = [ ]

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

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

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

then Class Map at time 43 = [ ]

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

then Python Object Store at time 43 = [ ]

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

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

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

then Python Object Store at time 44 = [ ]

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

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

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

then Class Map at time 44 = [ ]

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

then Python Object Store at time 45 = [ ]

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

then arguments stack at time 45 = [ ]

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

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

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

then Class Map at time 45 = [ ]

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

then Variables Map at time 46 = [ entry a: 2, [ ] ]

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

then the line at time 46 = 4

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

then the tab at time 46 = 1

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

then Python Object Store at time 46 = [ ]

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

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

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

then Class Map at time 46 = [ ]

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

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

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

then Python Object Store at time 47 = [ ]

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

then Class Map at time 47 = [ ]

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

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

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

then expression state at time 48 = "begin_expr"

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

then the line at time 48 = 2

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

then the tab at time 48 = 0

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

then Value Stack at time 48 = [ ]

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

then parent stack at time 48 = [ ]

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

then arguments stack at time 48 = [ ]

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

then Python Object Store at time 48 = [ ]

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

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

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

then Class Map at time 48 = [ ]

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

then Python Object Store at time 49 = [ ]

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

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

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

then Class Map at time 49 = [ ]

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

then Python Object Store at time 50 = [ ]

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

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

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

then Class Map at time 50 = [ ]

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

then Python Object Store at time 51 = [ ]

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

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

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

then Class Map at time 51 = [ ]

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

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

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

then Class Map at time 52 = [ ]

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

then Python Object Store at time 52 = [ ]

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

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

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

then Python Object Store at time 53 = [ ]

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

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

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

then Class Map at time 53 = [ ]

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

then Python Object Store at time 54 = [ ]

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

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

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

then Class Map at time 54 = [ ]

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

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

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

then Class Map at time 55 = [ ]

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

then Python Object Store at time 55 = [ ]

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

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

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

then Python Object Store at time 56 = [ ]

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

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

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

then Class Map at time 56 = [ ]

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

then Python Object Store at time 57 = [ ]

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

then arguments stack at time 57 = [ ]

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

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

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

then Class Map at time 57 = [ ]

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

then Class Map at time 58 = [ ]

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

then Python Object Store at time 58 = [ ]

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

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

• the line at time 58 = 3
• the tab at time 58 = 0
• statement at line 3, tab 1 = a = __add__(a, 1)
• Variables Map at time 58 = [ entry a: 2, [ ] ]

then Variables Map at time 59 = [ entry a: 2, [ ] ]

• the line at time 58 = 3
• the tab at time 58 = 0
• statement at line 3, tab 1 = a = __add__(a, 1)
• stack at time 58 = [ ]

then stack at time 59 = [ ]

• the line at time 58 = 3
• the tab at time 58 = 0
• statement at line 3, tab 1 = a = __add__(a, 1)
• Python Object Store at time 58 = [ ]

then Python Object Store at time 59 = [ ]

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

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

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

then Class Map at time 59 = [ ]