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

Get Return Value 17

if the following are true:

expression state at time 17 = "return"
Value Stack at time 17 = [ [ ], [ [ entry "ES": "Estonia", [ ] ], [ ] ] ]
Return Value at time 17 = "MX"

then Value Stack at time 18 = [ [ "MX", [ ] ], [ [ entry "ES": "Estonia", [ ] ], [ ] ] ]

Do Variables At Unchanged 17

if the following are true:

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

then Variables Map at time 18 = [ ]

Do Line At Unchanged 17

if the following are true:

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

then the line at time 18 = 1

Do Tab At Unchanged 17

if the following are true:

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

then the tab at time 18 = 0

Do Arg Stack At Unchanged 17

if the following are true:

expression state at time 17 = "return"
arguments stack at time 17 = [ [ "Mexico", [ ] ], [ [ ], [ ] ] ]

then arguments stack at time 18 = [ [ "Mexico", [ ] ], [ [ ], [ ] ] ]

Do Parent Stack At Unchanged 17

if the following are true:

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

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

Do Stack At Unchanged 17

if the following are true:

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

then stack at time 18 = [ ]

Do Class Defs At Unchanged 17

if the following are true:

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

then Class Map at time 18 = [ ]

Do Object Store At Unchanged 17

if the following are true:

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

then Python Object Store at time 18 = [ ]

Do Control Map At Unchanged 17

if the following are true:

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

then Control Map at time 18 = [ ]

Get Iterate Expr 18

if the following are true:

expression state at time 18 = "iterate_args"
arguments stack at time 18 = [ [ "Mexico", [ ] ], [ [ ], [ ] ] ]

then the expression at time 19 = "Mexico"

Get Iterate Params 18

if the following are true:

expression state at time 18 = "iterate_args"
arguments stack at time 18 = [ [ "Mexico", [ ] ], [ [ ], [ ] ] ]

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

Get Iterate State 18

if the following are true:

expression state at time 18 = "iterate_args"
arguments stack at time 18 = [ [ "Mexico", [ ] ], [ [ ], [ ] ] ]

then expression state at time 19 = "begin_expr"

Get Iterate Parent 18

if the following are true:

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

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

Do Value Stack At Unchanged 18

if the following are true:

expression state at time 18 = "iterate_args"
Value Stack at time 18 = [ [ "MX", [ ] ], [ [ entry "ES": "Estonia", [ ] ], [ ] ] ]

then Value Stack at time 19 = [ [ "MX", [ ] ], [ [ entry "ES": "Estonia", [ ] ], [ ] ] ]

Do Line At Unchanged 18

if the following are true:

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

then the line at time 19 = 1

Do Tab At Unchanged 18

if the following are true:

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

then the tab at time 19 = 0

Do Stack At Unchanged 18

if the following are true:

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

then stack at time 19 = [ ]

Do Object Store At Unchanged 18

if the following are true:

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

then Python Object Store at time 19 = [ ]

Do Control Map At Unchanged 18

if the following are true:

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

then Control Map at time 19 = [ ]

Do Variables At Unchanged 18

if the following are true:

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

then Variables Map at time 19 = [ ]

Do Class Defs At Unchanged 18

if the following are true:

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

then Class Map at time 19 = [ ]

Get Begin Expr State 19

if the following are true:

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

then expression state at time 20 = "return"

Get Begin Expr Value Unchaged 19

if the following are true:

the expression at time 19 = "Mexico"
expression state at time 19 = "begin_expr"
"Mexico" is constant
Value Stack at time 19 = [ [ "MX", [ ] ], [ [ entry "ES": "Estonia", [ ] ], [ ] ] ]

then Value Stack at time 20 = [ [ "MX", [ ] ], [ [ entry "ES": "Estonia", [ ] ], [ ] ] ]

Get Begin Expr Params Unchanged19

if the following are true:

the expression at time 19 = "Mexico"
expression state at time 19 = "begin_expr"
"Mexico" is constant
arguments stack at time 19 = [ [ ], [ [ ], [ ] ] ]

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

Get Begin Expr Return 19

if the following are true:

expression state at time 19 = "begin_expr"
the expression at time 19 = "Mexico"
"Mexico" is constant

then Return Value at time 20 = "Mexico"

Get Begin Expr Const Parent 19

if the following are true:

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

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

Do Line At Unchanged 19

if the following are true:

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

then the line at time 20 = 1

Do Tab At Unchanged 19

if the following are true:

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

then the tab at time 20 = 0

Do Stack At Unchanged 19

if the following are true:

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

then stack at time 20 = [ ]

Do Object Store At Unchanged 19

if the following are true:

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

then Python Object Store at time 20 = [ ]

Do Control Map At Unchanged 19

if the following are true:

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

then Control Map at time 20 = [ ]

Do Variables At Unchanged 19

if the following are true:

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

then Variables Map at time 20 = [ ]

Do Class Defs At Unchanged 19

if the following are true:

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

then Class Map at time 20 = [ ]

Get New State 20

if expression state at time 20 = "return", then expression state at time 21 = "iterate_args"

Get Return Value 20

if the following are true:

expression state at time 20 = "return"
Value Stack at time 20 = [ [ "MX", [ ] ], [ [ entry "ES": "Estonia", [ ] ], [ ] ] ]
Return Value at time 20 = "Mexico"

then Value Stack at time 21 = [ [ "Mexico", [ "MX", [ ] ] ], [ [ entry "ES": "Estonia", [ ] ], [ ] ] ]

Do Variables At Unchanged 20

if the following are true:

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

then Variables Map at time 21 = [ ]

Do Line At Unchanged 20

if the following are true:

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

then the line at time 21 = 1

Do Tab At Unchanged 20

if the following are true:

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

then the tab at time 21 = 0

Do Arg Stack At Unchanged 20

if the following are true:

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

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

Do Parent Stack At Unchanged 20

if the following are true:

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

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

Do Stack At Unchanged 20

if the following are true:

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

then stack at time 21 = [ ]

Do Class Defs At Unchanged 20

if the following are true:

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

then Class Map at time 21 = [ ]

Do Object Store At Unchanged 20

if the following are true:

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

then Python Object Store at time 21 = [ ]

Do Control Map At Unchanged 20

if the following are true:

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

then Control Map at time 21 = [ ]

Get Iterate End State 21

if the following are true:

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

then expression state at time 22 = "call_function_begin"

Get Iterate End Expr 21

if the following are true:

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

then the expression at time 22 = entry "MX": "Mexico"

Get Iterate End Parent 21

if the following are true:

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

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

Get Iterate End Params 21

if the following are true:

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

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

Do Value Stack At Unchanged 21

if the following are true:

expression state at time 21 = "iterate_args"
Value Stack at time 21 = [ [ "Mexico", [ "MX", [ ] ] ], [ [ entry "ES": "Estonia", [ ] ], [ ] ] ]

then Value Stack at time 22 = [ [ "Mexico", [ "MX", [ ] ] ], [ [ entry "ES": "Estonia", [ ] ], [ ] ] ]

Do Line At Unchanged 21

if the following are true:

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

then the line at time 22 = 1

Do Tab At Unchanged 21

if the following are true:

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

then the tab at time 22 = 0

Do Stack At Unchanged 21

if the following are true:

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

then stack at time 22 = [ ]

Do Object Store At Unchanged 21

if the following are true:

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

then Python Object Store at time 22 = [ ]

Do Control Map At Unchanged 21

if the following are true:

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

then Control Map at time 22 = [ ]

Do Variables At Unchanged 21

if the following are true:

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

then Variables Map at time 22 = [ ]

Do Class Defs At Unchanged 21

if the following are true:

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

then Class Map at time 22 = [ ]

Do Object Store At Unchanged 22

if the following are true:

expression state at time 22 = "call_function_begin"
the expression at time 22 = entry "MX": "Mexico"
Python Object Store at time 22 = [ ]

then Python Object Store at time 23 = [ ]

Do Reverse 22 0

reverse of [ "Mexico", [ "MX", [ ] ] ] = [ "MX", [ "Mexico", [ ] ] ]

Write Call Function Begin Entry Return Val 22

if the following are true:

expression state at time 22 = "call_function_begin"
Value Stack at time 22 = [ [ "Mexico", [ "MX", [ ] ] ], [ [ entry "ES": "Estonia", [ ] ], [ ] ] ]
the expression at time 22 = entry "MX": "Mexico"

then Return Value at time 23 = entry "MX": "Mexico"

Write Call Function Begin Next State 22

if the following are true:

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

then expression state at time 23 = "return"

Write Call Function Begin Value Stack 22

if the following are true:

expression state at time 22 = "call_function_begin"
Value Stack at time 22 = [ [ "Mexico", [ "MX", [ ] ] ], [ [ entry "ES": "Estonia", [ ] ], [ ] ] ]
the expression at time 22 = entry "MX": "Mexico"

then Value Stack at time 23 = [ [ entry "ES": "Estonia", [ ] ], [ ] ]

Do Arg Stack At Unchanged 22

if the following are true:

expression state at time 22 = "call_function_begin"
arguments stack at time 22 = [ [ ], [ ] ]

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

Do Parent Stack At Unchanged 22

if the following are true:

expression state at time 22 = "call_function_begin"
parent stack at time 22 = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]

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

Do Control Map At Unchanged 22

if the following are true:

expression state at time 22 = "call_function_begin"
Control Map at time 22 = [ ]

then Control Map at time 23 = [ ]

Do Variables At Unchanged 22

if the following are true:

expression state at time 22 = "call_function_begin"
Variables Map at time 22 = [ ]

then Variables Map at time 23 = [ ]

Do Line At Unchanged 22

if the following are true:

expression state at time 22 = "call_function_begin"
the line at time 22 = 1

then the line at time 23 = 1

Do Tab At Unchanged 22

if the following are true:

expression state at time 22 = "call_function_begin"
the tab at time 22 = 0

then the tab at time 23 = 0

Do Stack At Unchanged 22

if the following are true:

expression state at time 22 = "call_function_begin"
stack at time 22 = [ ]

then stack at time 23 = [ ]

Do Class Defs At Unchanged 22

if the following are true:

expression state at time 22 = "call_function_begin"
Class Map at time 22 = [ ]

then Class Map at time 23 = [ ]

Get New State 23

if expression state at time 23 = "return", then expression state at time 24 = "iterate_args"

Get Return Value 23

if the following are true:

expression state at time 23 = "return"
Value Stack at time 23 = [ [ entry "ES": "Estonia", [ ] ], [ ] ]
Return Value at time 23 = entry "MX": "Mexico"

then Value Stack at time 24 = [ [ entry "MX": "Mexico", [ entry "ES": "Estonia", [ ] ] ], [ ] ]

Do Variables At Unchanged 23

if the following are true:

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

then Variables Map at time 24 = [ ]

Do Line At Unchanged 23

if the following are true:

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

then the line at time 24 = 1

Do Tab At Unchanged 23

if the following are true:

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

then the tab at time 24 = 0

Do Arg Stack At Unchanged 23

if the following are true:

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

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

Do Parent Stack At Unchanged 23

if the following are true:

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

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

Do Stack At Unchanged 23

if the following are true:

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

then stack at time 24 = [ ]

Do Class Defs At Unchanged 23

if the following are true:

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

then Class Map at time 24 = [ ]

Do Object Store At Unchanged 23

if the following are true:

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

then Python Object Store at time 24 = [ ]

Do Control Map At Unchanged 23

if the following are true:

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

then Control Map at time 24 = [ ]

Get Iterate End State 24

if the following are true:

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

then expression state at time 25 = "call_function_begin"

Get Iterate End Expr 24

if the following are true:

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

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

Get Iterate End Parent 24

if the following are true:

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

then parent stack at time 25 = [ ]

Get Iterate End Params 24

if the following are true:

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

then arguments stack at time 25 = [ ]

Do Value Stack At Unchanged 24

if the following are true:

expression state at time 24 = "iterate_args"
Value Stack at time 24 = [ [ entry "MX": "Mexico", [ entry "ES": "Estonia", [ ] ] ], [ ] ]

then Value Stack at time 25 = [ [ entry "MX": "Mexico", [ entry "ES": "Estonia", [ ] ] ], [ ] ]

Do Line At Unchanged 24

if the following are true:

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

then the line at time 25 = 1

Do Tab At Unchanged 24

if the following are true:

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

then the tab at time 25 = 0

Do Stack At Unchanged 24

if the following are true:

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

then stack at time 25 = [ ]

Do Object Store At Unchanged 24

if the following are true:

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

then Python Object Store at time 25 = [ ]

Do Control Map At Unchanged 24

if the following are true:

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

then Control Map at time 25 = [ ]

Do Variables At Unchanged 24

if the following are true:

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

then Variables Map at time 25 = [ ]

Do Class Defs At Unchanged 24

if the following are true:

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

then Class Map at time 25 = [ ]

Do Len At 25

length of stack [ ] = 0

Do Reverse 25 0

reverse of [ ] = [ ]

Do Reverse 25 1

reverse of [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]

Do Reverse 25 2

reverse of [ entry "MX": "Mexico", [ entry "ES": "Estonia", [ ] ] ] = [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ]

Do Append 25

result of appending {"ES": "Estonia", "MX": "Mexico"} to [ ] = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]

Write Call Function Begin Py Dict Append Object 25

if the following are true:

expression state at time 25 = "call_function_begin"
Value Stack at time 25 = [ [ entry "MX": "Mexico", [ entry "ES": "Estonia", [ ] ] ], [ ] ]
the expression at time 25 = {"ES": "Estonia", "MX": "Mexico"}
Python Object Store at time 25 = [ ]

then Python Object Store at time 26 = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]

Write Call Function Begin Py List Return Val 25

if the following are true:

expression state at time 25 = "call_function_begin"
Value Stack at time 25 = [ [ entry "MX": "Mexico", [ entry "ES": "Estonia", [ ] ] ], [ ] ]
the expression at time 25 = {"ES": "Estonia", "MX": "Mexico"}
Python Object Store at time 25 = [ ]

then Return Value at time 26 = Python reference 0

Pages: 150 151 152 ... 193