Proofs

A proof is a series of claims that lead to a conclusion. Some proofs are conditional, which means that the claims can only be made under certain conditions. Click on a statement to see the proof

Write Set Name Arg Stack At on State 11

if the following are true:

the line at time 11 = 2
the tab at time 11 = 0
statement at line 2, tab 0 = for value in numbers:
expression state at time 11 = "not_expr"
map (Control Map at time 11) does not contain a for loop entry at line: 2 and tab: 0

then arguments stack at time 12 = [ ]

Write Stmt Object Store At Unchanged Expr11

if the following are true:

the line at time 11 = 2
the tab at time 11 = 0
statement at line 2, tab 0 = for value in numbers:
expression state at time 11 = "not_expr"
Python Object Store at time 11 = [ [4, 7], [ ] ]
map (Control Map at time 11) does not contain a for loop entry at line: 2 and tab: 0

then Python Object Store at time 12 = [ [4, 7], [ ] ]

Write Stmt Control Map At Unchanged Expr11

if the following are true:

the line at time 11 = 2
the tab at time 11 = 0
statement at line 2, tab 0 = for value in numbers:
expression state at time 11 = "not_expr"
Control Map at time 11 = [ ]
map (Control Map at time 11) does not contain a for loop entry at line: 2 and tab: 0

then Control Map at time 12 = [ ]

Write Stmt Variables At Unchanged Expr11

if the following are true:

the line at time 11 = 2
the tab at time 11 = 0
statement at line 2, tab 0 = for value in numbers:
expression state at time 11 = "not_expr"
Variables Map at time 11 = [ entry numbers: (Python reference 0), [ ] ]
map (Control Map at time 11) does not contain a for loop entry at line: 2 and tab: 0

then Variables Map at time 12 = [ entry numbers: (Python reference 0), [ ] ]

Write Stmt Stack At Unchanged 11

if the following are true:

the line at time 11 = 2
the tab at time 11 = 0
statement at line 2, tab 0 = for value in numbers:
stack at time 11 = [ ]
numbers is a variable

then stack at time 12 = [ ]

Write Stmt Class Defs At Unchanged 11

if the following are true:

the line at time 11 = 2
the tab at time 11 = 0
statement at line 2, tab 0 = for value in numbers:
Class Map at time 11 = [ ]
numbers is a variable

then Class Map at time 12 = [ ]

Do Get Key Value 12 0

value at numbers in map [ entry numbers: (Python reference 0), [ ] ] = Python reference 0

Do Variables At Unchanged 12

if the following are true:

expression state at time 12 = "begin_expr"
Variables Map at time 12 = [ entry numbers: (Python reference 0), [ ] ]

then Variables Map at time 13 = [ entry numbers: (Python reference 0), [ ] ]

Get Begin Expr State Name 12

if the following are true:

the expression at time 12 = numbers
expression state at time 12 = "begin_expr"
numbers is a variable
parent stack at time 12 = [ ]

then expression state at time 13 = "end_expr"

Get Begin Expr Value Unchaged Name 12

if the following are true:

the expression at time 12 = numbers
expression state at time 12 = "begin_expr"
numbers is a variable
Value Stack at time 12 = [ ]

then Value Stack at time 13 = [ ]

Get Begin Expr Params Unchanged Name12

if the following are true:

the expression at time 12 = numbers
expression state at time 12 = "begin_expr"
numbers is a variable
arguments stack at time 12 = [ ]

then arguments stack at time 13 = [ ]

Get Begin Expr Return Name 12

if the following are true:

expression state at time 12 = "begin_expr"
the expression at time 12 = numbers
numbers is a variable
Variables Map at time 12 = [ entry numbers: (Python reference 0), [ ] ]

then Return Value at time 13 = Python reference 0

Get Begin Expr Parent Name 12

if the following are true:

expression state at time 12 = "begin_expr"
the expression at time 12 = numbers
numbers is a variable
parent stack at time 12 = [ ]

then parent stack at time 13 = [ ]

Do Line At Unchanged 12

if the following are true:

expression state at time 12 = "begin_expr"
the line at time 12 = 2

then the line at time 13 = 2

Do Tab At Unchanged 12

if the following are true:

expression state at time 12 = "begin_expr"
the tab at time 12 = 0

then the tab at time 13 = 0

Do Stack At Unchanged 12

if the following are true:

expression state at time 12 = "begin_expr"
stack at time 12 = [ ]

then stack at time 13 = [ ]

Do Object Store At Unchanged 12

if the following are true:

expression state at time 12 = "begin_expr"
Python Object Store at time 12 = [ [4, 7], [ ] ]

then Python Object Store at time 13 = [ [4, 7], [ ] ]

Do Control Map At Unchanged 12

if the following are true:

expression state at time 12 = "begin_expr"
Control Map at time 12 = [ ]

then Control Map at time 13 = [ ]

Do Class Defs At Unchanged 12

if the following are true:

expression state at time 12 = "begin_expr"
Class Map at time 12 = [ ]

then Class Map at time 13 = [ ]

Write End to Not Expr 13

if expression state at time 13 = "end_expr", then expression state at time 14 = "not_expr"

Write Set Name Line At on State 13

if the following are true:

the line at time 13 = 2
the tab at time 13 = 0
statement at line 2, tab 0 = for value in numbers:
expression state at time 13 = "end_expr"

then the line at time 14 = 2

Write Set Name Tab At on State 13

if the following are true:

the line at time 13 = 2
the tab at time 13 = 0
statement at line 2, tab 0 = for value in numbers:
expression state at time 13 = "end_expr"

then the tab at time 14 = 0

Write Stmt Variables At Unchanged Expr13

if the following are true:

the line at time 13 = 2
the tab at time 13 = 0
statement at line 2, tab 0 = for value in numbers:
expression state at time 13 = "end_expr"
Variables Map at time 13 = [ entry numbers: (Python reference 0), [ ] ]

then Variables Map at time 14 = [ entry numbers: (Python reference 0), [ ] ]

Write Stmt Stack At Unchanged Expr13

if the following are true:

the line at time 13 = 2
the tab at time 13 = 0
statement at line 2, tab 0 = for value in numbers:
expression state at time 13 = "end_expr"
stack at time 13 = [ ]

then stack at time 14 = [ ]

Write Stmt Object Store At Unchanged Expr13

if the following are true:

the line at time 13 = 2
the tab at time 13 = 0
statement at line 2, tab 0 = for value in numbers:
expression state at time 13 = "end_expr"
Python Object Store at time 13 = [ [4, 7], [ ] ]

then Python Object Store at time 14 = [ [4, 7], [ ] ]

Write Stmt Class Defs At Unchanged Expr13

if the following are true:

the line at time 13 = 2
the tab at time 13 = 0
statement at line 2, tab 0 = for value in numbers:
expression state at time 13 = "end_expr"
Class Map at time 13 = [ ]

then Class Map at time 14 = [ ]

Do Element At 13 0

the element at index 0 of stack [ [4, 7], [ ] ] = [4, 7]

Write Element At Object Store 13

if Python Object Store at time 13 = [ [4, 7], [ ] ], then the element at index 0 of stack (Python Object Store at time 13) = [4, 7]

Do Set Key Value 13 0

result of storing (trio ("for", 2, [ 4, [ 7, [ ] ] ])) at key: 0 in map: [ ] = [ entry 0: (trio ("for", 2, [ 4, [ 7, [ ] ] ])), [ ] ]

Write For Iterable Finished Control Map13

if the following are true:

the line at time 13 = 2
the tab at time 13 = 0
statement at line 2, tab 0 = for value in numbers:
expression state at time 13 = "end_expr"
Return Value at time 13 = Python reference 0
Control Map at time 13 = [ ]
the element at index 0 of stack (Python Object Store at time 13) = [4, 7]

then Control Map at time 14 = [ entry 0: (trio ("for", 2, [ 4, [ 7, [ ] ] ])), [ ] ]

Do Set Key Value 14 0

result of storing 4 at key: value in map: [ entry numbers: (Python reference 0), [ ] ] = [ entry numbers: (Python reference 0), [ entry value: 4, [ ] ] ]

Do Get Key Value 14 0

value at 0 in map [ entry 0: (trio ("for", 2, [ 4, [ 7, [ ] ] ])), [ ] ] = trio ("for", 2, [ 4, [ 7, [ ] ] ])

Get Key Value Control Map At 14

if Control Map at time 14 = [ entry 0: (trio ("for", 2, [ 4, [ 7, [ ] ] ])), [ ] ], then value at 0 in map (Control Map at time 14) = trio ("for", 2, [ 4, [ 7, [ ] ] ])

Write For Iterate Line At 14

if the following are true:

the line at time 14 = 2
the tab at time 14 = 0
statement at line 2, tab 0 = for value in numbers:
Control Map at time 14 = [ entry 0: (trio ("for", 2, [ 4, [ 7, [ ] ] ])), [ ] ]

then the line at time 15 = 3

Write For Iterate Tab At 14

if the following are true:

the line at time 14 = 2
the tab at time 14 = 0
statement at line 2, tab 0 = for value in numbers:
Control Map at time 14 = [ entry 0: (trio ("for", 2, [ 4, [ 7, [ ] ] ])), [ ] ]

then the tab at time 15 = 1

Write For Iterate Expr State At 14

if the following are true:

the line at time 14 = 2
the tab at time 14 = 0
statement at line 2, tab 0 = for value in numbers:
Control Map at time 14 = [ entry 0: (trio ("for", 2, [ 4, [ 7, [ ] ] ])), [ ] ]

then expression state at time 15 = "not_expr"

Write For Iterate Variables 14

if the following are true:

the line at time 14 = 2
the tab at time 14 = 0
statement at line 2, tab 0 = for value in numbers:
Control Map at time 14 = [ entry 0: (trio ("for", 2, [ 4, [ 7, [ ] ] ])), [ ] ]
Variables Map at time 14 = [ entry numbers: (Python reference 0), [ ] ]

then Variables Map at time 15 = [ entry numbers: (Python reference 0), [ entry value: 4, [ ] ] ]

Do Set Key Value 14 1

result of storing (trio ("for", 2, [ 7, [ ] ])) at key: 0 in map: [ entry 0: (trio ("for", 2, [ 4, [ 7, [ ] ] ])), [ ] ] = [ entry 0: (trio ("for", 2, [ 7, [ ] ])), [ ] ]

Write For Iterate Control Map 14

if the following are true:

the line at time 14 = 2
the tab at time 14 = 0
statement at line 2, tab 0 = for value in numbers:
Control Map at time 14 = [ entry 0: (trio ("for", 2, [ 4, [ 7, [ ] ] ])), [ ] ]

then Control Map at time 15 = [ entry 0: (trio ("for", 2, [ 7, [ ] ])), [ ] ]

Write For Iterate Stack At Unchanged 14

if the following are true:

the line at time 14 = 2
the tab at time 14 = 0
statement at line 2, tab 0 = for value in numbers:
Control Map at time 14 = [ entry 0: (trio ("for", 2, [ 4, [ 7, [ ] ] ])), [ ] ]
stack at time 14 = [ ]

then stack at time 15 = [ ]

Write For Iterate Object Store At Unchanged 14

if the following are true:

the line at time 14 = 2
the tab at time 14 = 0
statement at line 2, tab 0 = for value in numbers:
Control Map at time 14 = [ entry 0: (trio ("for", 2, [ 4, [ 7, [ ] ] ])), [ ] ]
Python Object Store at time 14 = [ [4, 7], [ ] ]

then Python Object Store at time 15 = [ [4, 7], [ ] ]

Write For Iterate Class Defs At Unchanged 14

if the following are true:

the line at time 14 = 2
the tab at time 14 = 0
statement at line 2, tab 0 = for value in numbers:
Control Map at time 14 = [ entry 0: (trio ("for", 2, [ 4, [ 7, [ ] ] ])), [ ] ]
Class Map at time 14 = [ ]

then Class Map at time 15 = [ ]

Do Convert Stmt 15

if statement at line 3, tab 1 = x = value * 4, then statement at line 3, tab 1 = x = __mul__(value, 4)

Write Set Name Expr At on State 15

if the following are true:

the line at time 15 = 3
the tab at time 15 = 1
statement at line 3, tab 1 = x = __mul__(value, 4)
expression state at time 15 = "not_expr"

then the expression at time 16 = __mul__(value, 4)

Write Set Name Expr State At on State 15

if the following are true:

the line at time 15 = 3
the tab at time 15 = 1
statement at line 3, tab 1 = x = __mul__(value, 4)
expression state at time 15 = "not_expr"

then expression state at time 16 = "begin_expr"

Write Set Name Line At on State 15

if the following are true:

the line at time 15 = 3
the tab at time 15 = 1
statement at line 3, tab 1 = x = __mul__(value, 4)
expression state at time 15 = "not_expr"

then the line at time 16 = 3

Write Set Name Tab At on State 15

if the following are true:

the line at time 15 = 3
the tab at time 15 = 1
statement at line 3, tab 1 = x = __mul__(value, 4)
expression state at time 15 = "not_expr"

then the tab at time 16 = 1

Write Set Name Value Stack At on State 15

if the following are true:

the line at time 15 = 3
the tab at time 15 = 1
statement at line 3, tab 1 = x = __mul__(value, 4)
expression state at time 15 = "not_expr"

then Value Stack at time 16 = [ ]

Write Set Name Parent Stack At on State 15

if the following are true:

the line at time 15 = 3
the tab at time 15 = 1
statement at line 3, tab 1 = x = __mul__(value, 4)
expression state at time 15 = "not_expr"

then parent stack at time 16 = [ ]

Write Set Name Arg Stack At on State 15

if the following are true:

the line at time 15 = 3
the tab at time 15 = 1
statement at line 3, tab 1 = x = __mul__(value, 4)
expression state at time 15 = "not_expr"

then arguments stack at time 16 = [ ]

Write Stmt Variables At Unchanged Expr15

if the following are true:

the line at time 15 = 3
the tab at time 15 = 1
statement at line 3, tab 1 = x = __mul__(value, 4)
expression state at time 15 = "not_expr"
Variables Map at time 15 = [ entry numbers: (Python reference 0), [ entry value: 4, [ ] ] ]

then Variables Map at time 16 = [ entry numbers: (Python reference 0), [ entry value: 4, [ ] ] ]

Write Stmt Stack At Unchanged Expr15

if the following are true:

the line at time 15 = 3
the tab at time 15 = 1
statement at line 3, tab 1 = x = __mul__(value, 4)
expression state at time 15 = "not_expr"
stack at time 15 = [ ]

then stack at time 16 = [ ]

Write Stmt Object Store At Unchanged Expr15

if the following are true:

the line at time 15 = 3
the tab at time 15 = 1
statement at line 3, tab 1 = x = __mul__(value, 4)
expression state at time 15 = "not_expr"
Python Object Store at time 15 = [ [4, 7], [ ] ]

then Python Object Store at time 16 = [ [4, 7], [ ] ]

Write Stmt Control Map At Unchanged 15

if the following are true:

the line at time 15 = 3
the tab at time 15 = 1
statement at line 3, tab 1 = x = __mul__(value, 4)
Control Map at time 15 = [ entry 0: (trio ("for", 2, [ 7, [ ] ])), [ ] ]

then Control Map at time 16 = [ entry 0: (trio ("for", 2, [ 7, [ ] ])), [ ] ]

Write Stmt Class Defs At Unchanged 15

if the following are true:

the line at time 15 = 3
the tab at time 15 = 1
statement at line 3, tab 1 = x = __mul__(value, 4)
Class Map at time 15 = [ ]

then Class Map at time 16 = [ ]

Get Begin Expr Value 16

if the following are true:

expression state at time 16 = "begin_expr"
the expression at time 16 = __mul__(value, 4)
Value Stack at time 16 = [ ]

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

Get Begin Expr Parent 16

if the following are true:

expression state at time 16 = "begin_expr"
the expression at time 16 = __mul__(value, 4)
parent stack at time 16 = [ ]

then parent stack at time 17 = [ __mul__(value, 4), [ ] ]

Get Begin Expr Params 16

if the following are true:

expression state at time 16 = "begin_expr"
the expression at time 16 = __mul__(value, 4)
arguments stack at time 16 = [ ]

then arguments stack at time 17 = [ [ value, [ 4, [ ] ] ], [ ] ]

Get Begin Expr Call State 16

if the following are true:

expression state at time 16 = "begin_expr"
the expression at time 16 = __mul__(value, 4)

then expression state at time 17 = "iterate_args"

Do Expr At Unchanged 16

if the following are true:

expression state at time 16 = "begin_expr"
the expression at time 16 = __mul__(value, 4)

then the expression at time 17 = __mul__(value, 4)

Do Variables At Unchanged 16

if the following are true:

expression state at time 16 = "begin_expr"
Variables Map at time 16 = [ entry numbers: (Python reference 0), [ entry value: 4, [ ] ] ]

then Variables Map at time 17 = [ entry numbers: (Python reference 0), [ entry value: 4, [ ] ] ]

Do Line At Unchanged 16

if the following are true:

expression state at time 16 = "begin_expr"
the line at time 16 = 3

then the line at time 17 = 3

Do Tab At Unchanged 16

if the following are true:

expression state at time 16 = "begin_expr"
the tab at time 16 = 1

then the tab at time 17 = 1

Do Stack At Unchanged 16

if the following are true:

expression state at time 16 = "begin_expr"
stack at time 16 = [ ]

then stack at time 17 = [ ]

Do Object Store At Unchanged 16

if the following are true:

expression state at time 16 = "begin_expr"
Python Object Store at time 16 = [ [4, 7], [ ] ]

then Python Object Store at time 17 = [ [4, 7], [ ] ]

Do Control Map At Unchanged 16

if the following are true:

expression state at time 16 = "begin_expr"
Control Map at time 16 = [ entry 0: (trio ("for", 2, [ 7, [ ] ])), [ ] ]

then Control Map at time 17 = [ entry 0: (trio ("for", 2, [ 7, [ ] ])), [ ] ]

Do Class Defs At Unchanged 16

if the following are true:

expression state at time 16 = "begin_expr"
Class Map at time 16 = [ ]

then Class Map at time 17 = [ ]

Get Iterate Expr 17

if the following are true:

expression state at time 17 = "iterate_args"
arguments stack at time 17 = [ [ value, [ 4, [ ] ] ], [ ] ]

then the expression at time 18 = value

Get Iterate Params 17

if the following are true:

expression state at time 17 = "iterate_args"
arguments stack at time 17 = [ [ value, [ 4, [ ] ] ], [ ] ]

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

Get Iterate State 17

if the following are true:

expression state at time 17 = "iterate_args"
arguments stack at time 17 = [ [ value, [ 4, [ ] ] ], [ ] ]

then expression state at time 18 = "begin_expr"

Get Iterate Parent 17

if the following are true:

expression state at time 17 = "iterate_args"
arguments stack at time 17 = [ [ value, [ 4, [ ] ] ], [ ] ]
parent stack at time 17 = [ __mul__(value, 4), [ ] ]

then parent stack at time 18 = [ __mul__(value, 4), [ ] ]

Do Value Stack At Unchanged 17

if the following are true:

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

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

Do Line At Unchanged 17

if the following are true:

expression state at time 17 = "iterate_args"
the line at time 17 = 3

then the line at time 18 = 3

Do Tab At Unchanged 17

if the following are true:

expression state at time 17 = "iterate_args"
the tab at time 17 = 1

then the tab at time 18 = 1

Do Stack At Unchanged 17

if the following are true:

expression state at time 17 = "iterate_args"
stack at time 17 = [ ]

then stack at time 18 = [ ]

Do Object Store At Unchanged 17

if the following are true:

expression state at time 17 = "iterate_args"
Python Object Store at time 17 = [ [4, 7], [ ] ]

then Python Object Store at time 18 = [ [4, 7], [ ] ]

Do Control Map At Unchanged 17

if the following are true:

expression state at time 17 = "iterate_args"
Control Map at time 17 = [ entry 0: (trio ("for", 2, [ 7, [ ] ])), [ ] ]

then Control Map at time 18 = [ entry 0: (trio ("for", 2, [ 7, [ ] ])), [ ] ]

Do Variables At Unchanged 17

if the following are true:

expression state at time 17 = "iterate_args"
Variables Map at time 17 = [ entry numbers: (Python reference 0), [ entry value: 4, [ ] ] ]

then Variables Map at time 18 = [ entry numbers: (Python reference 0), [ entry value: 4, [ ] ] ]

Do Class Defs At Unchanged 17

if the following are true:

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

then Class Map at time 18 = [ ]

Do Get Key Value 18 0

value at value in map [ entry numbers: (Python reference 0), [ entry value: 4, [ ] ] ] = 4

Do Variables At Unchanged 18

if the following are true:

expression state at time 18 = "begin_expr"
Variables Map at time 18 = [ entry numbers: (Python reference 0), [ entry value: 4, [ ] ] ]

then Variables Map at time 19 = [ entry numbers: (Python reference 0), [ entry value: 4, [ ] ] ]

Get Begin Expr State Name 18

if the following are true:

the expression at time 18 = value
expression state at time 18 = "begin_expr"
value is a variable
parent stack at time 18 = [ __mul__(value, 4), [ ] ]

then expression state at time 19 = "return"

Get Begin Expr Value Unchaged Name 18

if the following are true:

the expression at time 18 = value
expression state at time 18 = "begin_expr"
value is a variable
Value Stack at time 18 = [ [ ], [ ] ]

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

Get Begin Expr Params Unchanged Name18

if the following are true:

the expression at time 18 = value
expression state at time 18 = "begin_expr"
value is a variable
arguments stack at time 18 = [ [ 4, [ ] ], [ ] ]

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

Get Begin Expr Return Name 18

if the following are true:

expression state at time 18 = "begin_expr"
the expression at time 18 = value
value is a variable
Variables Map at time 18 = [ entry numbers: (Python reference 0), [ entry value: 4, [ ] ] ]