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 Tab At on State 0

if the following are true:

the line at time 0 = 1
the tab at time 0 = 0
statement at line 1, tab 0 = locations = {"ES": "Estonia", "MX": "Mexico"}
expression state at time 0 = "not_expr"

then the tab at time 1 = 0

Write Set Name Value Stack At on State 0

if the following are true:

the line at time 0 = 1
the tab at time 0 = 0
statement at line 1, tab 0 = locations = {"ES": "Estonia", "MX": "Mexico"}
expression state at time 0 = "not_expr"

then Value Stack at time 1 = [ ]

Write Set Name Parent Stack At on State 0

if the following are true:

the line at time 0 = 1
the tab at time 0 = 0
statement at line 1, tab 0 = locations = {"ES": "Estonia", "MX": "Mexico"}
expression state at time 0 = "not_expr"

then parent stack at time 1 = [ ]

Write Set Name Arg Stack At on State 0

if the following are true:

the line at time 0 = 1
the tab at time 0 = 0
statement at line 1, tab 0 = locations = {"ES": "Estonia", "MX": "Mexico"}
expression state at time 0 = "not_expr"

then arguments stack at time 1 = [ ]

Write Stmt Variables At Unchanged Expr0

if the following are true:

the line at time 0 = 1
the tab at time 0 = 0
statement at line 1, tab 0 = locations = {"ES": "Estonia", "MX": "Mexico"}
expression state at time 0 = "not_expr"
Variables Map at time 0 = [ ]

then Variables Map at time 1 = [ ]

Write Stmt Stack At Unchanged Expr0

if the following are true:

the line at time 0 = 1
the tab at time 0 = 0
statement at line 1, tab 0 = locations = {"ES": "Estonia", "MX": "Mexico"}
expression state at time 0 = "not_expr"
stack at time 0 = [ ]

then stack at time 1 = [ ]

Write Stmt Object Store At Unchanged Expr0

if the following are true:

the line at time 0 = 1
the tab at time 0 = 0
statement at line 1, tab 0 = locations = {"ES": "Estonia", "MX": "Mexico"}
expression state at time 0 = "not_expr"
Python Object Store at time 0 = [ ]

then Python Object Store at time 1 = [ ]

Write Stmt Control Map At Unchanged 0

if the following are true:

the line at time 0 = 1
the tab at time 0 = 0
statement at line 1, tab 0 = locations = {"ES": "Estonia", "MX": "Mexico"}
Control Map at time 0 = [ ]

then Control Map at time 1 = [ ]

Write Stmt Class Defs At Unchanged 0

if the following are true:

the line at time 0 = 1
the tab at time 0 = 0
statement at line 1, tab 0 = locations = {"ES": "Estonia", "MX": "Mexico"}
Class Map at time 0 = [ ]

then Class Map at time 1 = [ ]

Get Begin Expr Value 1

if the following are true:

expression state at time 1 = "begin_expr"
the expression at time 1 = {"ES": "Estonia", "MX": "Mexico"}
Value Stack at time 1 = [ ]

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

Get Begin Expr Parent 1

if the following are true:

expression state at time 1 = "begin_expr"
the expression at time 1 = {"ES": "Estonia", "MX": "Mexico"}
parent stack at time 1 = [ ]

then parent stack at time 2 = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]

Get Begin Expr Params 1

if the following are true:

expression state at time 1 = "begin_expr"
the expression at time 1 = {"ES": "Estonia", "MX": "Mexico"}
arguments stack at time 1 = [ ]

then arguments stack at time 2 = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], [ ] ]

Get Begin Expr Call State 1

if the following are true:

expression state at time 1 = "begin_expr"
the expression at time 1 = {"ES": "Estonia", "MX": "Mexico"}

then expression state at time 2 = "iterate_args"

Do Expr At Unchanged 1

if the following are true:

expression state at time 1 = "begin_expr"
the expression at time 1 = {"ES": "Estonia", "MX": "Mexico"}

then the expression at time 2 = {"ES": "Estonia", "MX": "Mexico"}

Do Variables At Unchanged 1

if the following are true:

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

then Variables Map at time 2 = [ ]

Do Line At Unchanged 1

if the following are true:

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

then the line at time 2 = 1

Do Tab At Unchanged 1

if the following are true:

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

then the tab at time 2 = 0

Do Stack At Unchanged 1

if the following are true:

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

then stack at time 2 = [ ]

Do Object Store At Unchanged 1

if the following are true:

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

then Python Object Store at time 2 = [ ]

Do Control Map At Unchanged 1

if the following are true:

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

then Control Map at time 2 = [ ]

Do Class Defs At Unchanged 1

if the following are true:

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

then Class Map at time 2 = [ ]

Get Iterate Expr 2

if the following are true:

expression state at time 2 = "iterate_args"
arguments stack at time 2 = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], [ ] ]

then the expression at time 3 = entry "ES": "Estonia"

Get Iterate Params 2

if the following are true:

expression state at time 2 = "iterate_args"
arguments stack at time 2 = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], [ ] ]

then arguments stack at time 3 = [ [ entry "MX": "Mexico", [ ] ], [ ] ]

Get Iterate State 2

if the following are true:

expression state at time 2 = "iterate_args"
arguments stack at time 2 = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], [ ] ]

then expression state at time 3 = "begin_expr"

Get Iterate Parent 2

if the following are true:

expression state at time 2 = "iterate_args"
arguments stack at time 2 = [ [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ], [ ] ]
parent stack at time 2 = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]

then parent stack at time 3 = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]

Do Value Stack At Unchanged 2

if the following are true:

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

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

Do Line At Unchanged 2

if the following are true:

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

then the line at time 3 = 1

Do Tab At Unchanged 2

if the following are true:

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

then the tab at time 3 = 0

Do Stack At Unchanged 2

if the following are true:

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

then stack at time 3 = [ ]

Do Object Store At Unchanged 2

if the following are true:

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

then Python Object Store at time 3 = [ ]

Do Control Map At Unchanged 2

if the following are true:

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

then Control Map at time 3 = [ ]

Do Variables At Unchanged 2

if the following are true:

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

then Variables Map at time 3 = [ ]

Do Class Defs At Unchanged 2

if the following are true:

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

then Class Map at time 3 = [ ]

Get Begin Expr Value 3

if the following are true:

expression state at time 3 = "begin_expr"
the expression at time 3 = entry "ES": "Estonia"
Value Stack at time 3 = [ [ ], [ ] ]

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

Get Begin Expr Parent 3

if the following are true:

expression state at time 3 = "begin_expr"
the expression at time 3 = entry "ES": "Estonia"
parent stack at time 3 = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]

then parent stack at time 4 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

Get Begin Expr Params 3

if the following are true:

expression state at time 3 = "begin_expr"
the expression at time 3 = entry "ES": "Estonia"
arguments stack at time 3 = [ [ entry "MX": "Mexico", [ ] ], [ ] ]

then arguments stack at time 4 = [ [ "ES", [ "Estonia", [ ] ] ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

Get Begin Expr Call State 3

if the following are true:

expression state at time 3 = "begin_expr"
the expression at time 3 = entry "ES": "Estonia"

then expression state at time 4 = "iterate_args"

Do Expr At Unchanged 3

if the following are true:

expression state at time 3 = "begin_expr"
the expression at time 3 = entry "ES": "Estonia"

then the expression at time 4 = entry "ES": "Estonia"

Do Variables At Unchanged 3

if the following are true:

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

then Variables Map at time 4 = [ ]

Do Line At Unchanged 3

if the following are true:

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

then the line at time 4 = 1

Do Tab At Unchanged 3

if the following are true:

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

then the tab at time 4 = 0

Do Stack At Unchanged 3

if the following are true:

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

then stack at time 4 = [ ]

Do Object Store At Unchanged 3

if the following are true:

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

then Python Object Store at time 4 = [ ]

Do Control Map At Unchanged 3

if the following are true:

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

then Control Map at time 4 = [ ]

Do Class Defs At Unchanged 3

if the following are true:

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

then Class Map at time 4 = [ ]

Get Iterate Expr 4

if the following are true:

expression state at time 4 = "iterate_args"
arguments stack at time 4 = [ [ "ES", [ "Estonia", [ ] ] ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

then the expression at time 5 = "ES"

Get Iterate Params 4

if the following are true:

expression state at time 4 = "iterate_args"
arguments stack at time 4 = [ [ "ES", [ "Estonia", [ ] ] ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

then arguments stack at time 5 = [ [ "Estonia", [ ] ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

Get Iterate State 4

if the following are true:

expression state at time 4 = "iterate_args"
arguments stack at time 4 = [ [ "ES", [ "Estonia", [ ] ] ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

then expression state at time 5 = "begin_expr"

Get Iterate Parent 4

if the following are true:

expression state at time 4 = "iterate_args"
arguments stack at time 4 = [ [ "ES", [ "Estonia", [ ] ] ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]
parent stack at time 4 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

then parent stack at time 5 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

Do Value Stack At Unchanged 4

if the following are true:

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

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

Do Line At Unchanged 4

if the following are true:

expression state at time 4 = "iterate_args"
the line at time 4 = 1

then the line at time 5 = 1

Do Tab At Unchanged 4

if the following are true:

expression state at time 4 = "iterate_args"
the tab at time 4 = 0

then the tab at time 5 = 0

Do Stack At Unchanged 4

if the following are true:

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

then stack at time 5 = [ ]

Do Object Store At Unchanged 4

if the following are true:

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

then Python Object Store at time 5 = [ ]

Do Control Map At Unchanged 4

if the following are true:

expression state at time 4 = "iterate_args"
Control Map at time 4 = [ ]

then Control Map at time 5 = [ ]

Do Variables At Unchanged 4

if the following are true:

expression state at time 4 = "iterate_args"
Variables Map at time 4 = [ ]

then Variables Map at time 5 = [ ]

Do Class Defs At Unchanged 4

if the following are true:

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

then Class Map at time 5 = [ ]

Get Begin Expr State 5

if the following are true:

the expression at time 5 = "ES"
expression state at time 5 = "begin_expr"
"ES" is constant
parent stack at time 5 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

then expression state at time 6 = "return"

Get Begin Expr Value Unchaged 5

if the following are true:

the expression at time 5 = "ES"
expression state at time 5 = "begin_expr"
"ES" is constant
Value Stack at time 5 = [ [ ], [ [ ], [ ] ] ]

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

Get Begin Expr Params Unchanged5

if the following are true:

the expression at time 5 = "ES"
expression state at time 5 = "begin_expr"
"ES" is constant
arguments stack at time 5 = [ [ "Estonia", [ ] ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

then arguments stack at time 6 = [ [ "Estonia", [ ] ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

Get Begin Expr Return 5

if the following are true:

expression state at time 5 = "begin_expr"
the expression at time 5 = "ES"
"ES" is constant

then Return Value at time 6 = "ES"

Get Begin Expr Const Parent 5

if the following are true:

expression state at time 5 = "begin_expr"
the expression at time 5 = "ES"
"ES" is constant
parent stack at time 5 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

then parent stack at time 6 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

Do Line At Unchanged 5

if the following are true:

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

then the line at time 6 = 1

Do Tab At Unchanged 5

if the following are true:

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

then the tab at time 6 = 0

Do Stack At Unchanged 5

if the following are true:

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

then stack at time 6 = [ ]

Do Object Store At Unchanged 5

if the following are true:

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

then Python Object Store at time 6 = [ ]

Do Control Map At Unchanged 5

if the following are true:

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

then Control Map at time 6 = [ ]

Do Variables At Unchanged 5

if the following are true:

expression state at time 5 = "begin_expr"
Variables Map at time 5 = [ ]

then Variables Map at time 6 = [ ]

Do Class Defs At Unchanged 5

if the following are true:

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

then Class Map at time 6 = [ ]

Get New State 6

if expression state at time 6 = "return", then expression state at time 7 = "iterate_args"

Get Return Value 6

if the following are true:

expression state at time 6 = "return"
Value Stack at time 6 = [ [ ], [ [ ], [ ] ] ]
Return Value at time 6 = "ES"

then Value Stack at time 7 = [ [ "ES", [ ] ], [ [ ], [ ] ] ]

Do Variables At Unchanged 6

if the following are true:

expression state at time 6 = "return"
Variables Map at time 6 = [ ]

then Variables Map at time 7 = [ ]

Do Line At Unchanged 6

if the following are true:

expression state at time 6 = "return"
the line at time 6 = 1

then the line at time 7 = 1

Do Tab At Unchanged 6

if the following are true:

expression state at time 6 = "return"
the tab at time 6 = 0

then the tab at time 7 = 0

Do Arg Stack At Unchanged 6

if the following are true:

expression state at time 6 = "return"
arguments stack at time 6 = [ [ "Estonia", [ ] ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

then arguments stack at time 7 = [ [ "Estonia", [ ] ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

Do Parent Stack At Unchanged 6

if the following are true:

expression state at time 6 = "return"
parent stack at time 6 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

then parent stack at time 7 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

Do Stack At Unchanged 6

if the following are true:

expression state at time 6 = "return"
stack at time 6 = [ ]

then stack at time 7 = [ ]

Do Class Defs At Unchanged 6

if the following are true:

expression state at time 6 = "return"
Class Map at time 6 = [ ]

then Class Map at time 7 = [ ]

Do Object Store At Unchanged 6

if the following are true:

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

then Python Object Store at time 7 = [ ]

Do Control Map At Unchanged 6

if the following are true:

expression state at time 6 = "return"
Control Map at time 6 = [ ]

then Control Map at time 7 = [ ]

Get Iterate Expr 7

if the following are true:

expression state at time 7 = "iterate_args"
arguments stack at time 7 = [ [ "Estonia", [ ] ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

then the expression at time 8 = "Estonia"

Get Iterate Params 7

if the following are true:

expression state at time 7 = "iterate_args"
arguments stack at time 7 = [ [ "Estonia", [ ] ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

then arguments stack at time 8 = [ [ ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

Get Iterate State 7

if the following are true:

expression state at time 7 = "iterate_args"
arguments stack at time 7 = [ [ "Estonia", [ ] ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

then expression state at time 8 = "begin_expr"

Get Iterate Parent 7

if the following are true:

expression state at time 7 = "iterate_args"
arguments stack at time 7 = [ [ "Estonia", [ ] ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]
parent stack at time 7 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

then parent stack at time 8 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

Do Value Stack At Unchanged 7

if the following are true:

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

then Value Stack at time 8 = [ [ "ES", [ ] ], [ [ ], [ ] ] ]

Do Line At Unchanged 7

if the following are true:

expression state at time 7 = "iterate_args"
the line at time 7 = 1

then the line at time 8 = 1

Do Tab At Unchanged 7

if the following are true:

expression state at time 7 = "iterate_args"
the tab at time 7 = 0

then the tab at time 8 = 0

Do Stack At Unchanged 7

if the following are true:

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

then stack at time 8 = [ ]

Do Object Store At Unchanged 7

if the following are true:

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

then Python Object Store at time 8 = [ ]

Do Control Map At Unchanged 7

if the following are true:

expression state at time 7 = "iterate_args"
Control Map at time 7 = [ ]

then Control Map at time 8 = [ ]

Do Variables At Unchanged 7

if the following are true:

expression state at time 7 = "iterate_args"
Variables Map at time 7 = [ ]

then Variables Map at time 8 = [ ]

Do Class Defs At Unchanged 7

if the following are true:

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

then Class Map at time 8 = [ ]

Get Begin Expr State 8

if the following are true:

the expression at time 8 = "Estonia"
expression state at time 8 = "begin_expr"
"Estonia" is constant
parent stack at time 8 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

then expression state at time 9 = "return"

Get Begin Expr Value Unchaged 8

if the following are true:

the expression at time 8 = "Estonia"
expression state at time 8 = "begin_expr"
"Estonia" is constant
Value Stack at time 8 = [ [ "ES", [ ] ], [ [ ], [ ] ] ]

then Value Stack at time 9 = [ [ "ES", [ ] ], [ [ ], [ ] ] ]

Get Begin Expr Params Unchanged8

if the following are true:

the expression at time 8 = "Estonia"
expression state at time 8 = "begin_expr"
"Estonia" is constant
arguments stack at time 8 = [ [ ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

then arguments stack at time 9 = [ [ ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

Get Begin Expr Return 8

if the following are true:

expression state at time 8 = "begin_expr"
the expression at time 8 = "Estonia"
"Estonia" is constant

then Return Value at time 9 = "Estonia"

Get Begin Expr Const Parent 8

if the following are true:

expression state at time 8 = "begin_expr"
the expression at time 8 = "Estonia"
"Estonia" is constant
parent stack at time 8 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

then parent stack at time 9 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

Do Line At Unchanged 8

if the following are true:

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

then the line at time 9 = 1

Do Tab At Unchanged 8

if the following are true:

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

then the tab at time 9 = 0

Do Stack At Unchanged 8

if the following are true:

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

then stack at time 9 = [ ]

Pages: 148 149 150 ... 193