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

Do Object Store At Unchanged 8
if the following are true:
  • expression state at time 8 = "begin_expr"
  • Python Object Store at time 8 = [ ]

then Python Object Store at time 9 = [ ]


Do Control Map At Unchanged 8
if the following are true:
  • expression state at time 8 = "begin_expr"
  • Control Map at time 8 = [ ]

then Control Map at time 9 = [ ]


Do Variables At Unchanged 8
if the following are true:
  • expression state at time 8 = "begin_expr"
  • Variables Map at time 8 = [ ]

then Variables Map at time 9 = [ ]


Do Class Defs At Unchanged 8
if the following are true:
  • expression state at time 8 = "begin_expr"
  • Class Map at time 8 = [ ]

then Class Map at time 9 = [ ]


Get New State 9
if expression state at time 9 = "return", then expression state at time 10 = "iterate_args"

Get Return Value 9
if the following are true:
  • expression state at time 9 = "return"
  • Value Stack at time 9 = [ [ "ES", [ ] ], [ [ ], [ ] ] ]
  • Return Value at time 9 = "Estonia"

then Value Stack at time 10 = [ [ "Estonia", [ "ES", [ ] ] ], [ [ ], [ ] ] ]


Do Variables At Unchanged 9
if the following are true:
  • expression state at time 9 = "return"
  • Variables Map at time 9 = [ ]

then Variables Map at time 10 = [ ]


Do Line At Unchanged 9
if the following are true:
  • expression state at time 9 = "return"
  • the line at time 9 = 1

then the line at time 10 = 1


Do Tab At Unchanged 9
if the following are true:
  • expression state at time 9 = "return"
  • the tab at time 9 = 0

then the tab at time 10 = 0


Do Arg Stack At Unchanged 9
if the following are true:
  • expression state at time 9 = "return"
  • arguments stack at time 9 = [ [ ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]

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


Do Parent Stack At Unchanged 9
if the following are true:
  • expression state at time 9 = "return"
  • parent stack at time 9 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

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


Do Stack At Unchanged 9
if the following are true:
  • expression state at time 9 = "return"
  • stack at time 9 = [ ]

then stack at time 10 = [ ]


Do Class Defs At Unchanged 9
if the following are true:
  • expression state at time 9 = "return"
  • Class Map at time 9 = [ ]

then Class Map at time 10 = [ ]


Do Object Store At Unchanged 9
if the following are true:
  • expression state at time 9 = "return"
  • Python Object Store at time 9 = [ ]

then Python Object Store at time 10 = [ ]


Do Control Map At Unchanged 9
if the following are true:
  • expression state at time 9 = "return"
  • Control Map at time 9 = [ ]

then Control Map at time 10 = [ ]


Get Iterate End State 10
if the following are true:
  • expression state at time 10 = "iterate_args"
  • arguments stack at time 10 = [ [ ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]
  • parent stack at time 10 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

then expression state at time 11 = "call_function_begin"


Get Iterate End Expr 10
if the following are true:
  • expression state at time 10 = "iterate_args"
  • arguments stack at time 10 = [ [ ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]
  • parent stack at time 10 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

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


Get Iterate End Parent 10
if the following are true:
  • expression state at time 10 = "iterate_args"
  • arguments stack at time 10 = [ [ ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]
  • parent stack at time 10 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

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


Get Iterate End Params 10
if the following are true:
  • expression state at time 10 = "iterate_args"
  • arguments stack at time 10 = [ [ ], [ [ entry "MX": "Mexico", [ ] ], [ ] ] ]
  • parent stack at time 10 = [ entry "ES": "Estonia", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

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


Do Value Stack At Unchanged 10
if the following are true:
  • expression state at time 10 = "iterate_args"
  • Value Stack at time 10 = [ [ "Estonia", [ "ES", [ ] ] ], [ [ ], [ ] ] ]

then Value Stack at time 11 = [ [ "Estonia", [ "ES", [ ] ] ], [ [ ], [ ] ] ]


Do Line At Unchanged 10
if the following are true:
  • expression state at time 10 = "iterate_args"
  • the line at time 10 = 1

then the line at time 11 = 1


Do Tab At Unchanged 10
if the following are true:
  • expression state at time 10 = "iterate_args"
  • the tab at time 10 = 0

then the tab at time 11 = 0


Do Stack At Unchanged 10
if the following are true:
  • expression state at time 10 = "iterate_args"
  • stack at time 10 = [ ]

then stack at time 11 = [ ]


Do Object Store At Unchanged 10
if the following are true:
  • expression state at time 10 = "iterate_args"
  • Python Object Store at time 10 = [ ]

then Python Object Store at time 11 = [ ]


Do Control Map At Unchanged 10
if the following are true:
  • expression state at time 10 = "iterate_args"
  • Control Map at time 10 = [ ]

then Control Map at time 11 = [ ]


Do Variables At Unchanged 10
if the following are true:
  • expression state at time 10 = "iterate_args"
  • Variables Map at time 10 = [ ]

then Variables Map at time 11 = [ ]


Do Class Defs At Unchanged 10
if the following are true:
  • expression state at time 10 = "iterate_args"
  • Class Map at time 10 = [ ]

then Class Map at time 11 = [ ]


Do Object Store At Unchanged 11
if the following are true:
  • expression state at time 11 = "call_function_begin"
  • the expression at time 11 = entry "ES": "Estonia"
  • Python Object Store at time 11 = [ ]

then Python Object Store at time 12 = [ ]


Do Reverse 11 0
reverse of [ "Estonia", [ "ES", [ ] ] ] = [ "ES", [ "Estonia", [ ] ] ]

Write Call Function Begin Entry Return Val 11
if the following are true:
  • expression state at time 11 = "call_function_begin"
  • Value Stack at time 11 = [ [ "Estonia", [ "ES", [ ] ] ], [ [ ], [ ] ] ]
  • the expression at time 11 = entry "ES": "Estonia"

then Return Value at time 12 = entry "ES": "Estonia"


Write Call Function Begin Next State 11
if the following are true:
  • expression state at time 11 = "call_function_begin"
  • parent stack at time 11 = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]
  • the expression at time 11 = entry "ES": "Estonia"

then expression state at time 12 = "return"


Write Call Function Begin Value Stack 11
if the following are true:
  • expression state at time 11 = "call_function_begin"
  • Value Stack at time 11 = [ [ "Estonia", [ "ES", [ ] ] ], [ [ ], [ ] ] ]
  • the expression at time 11 = entry "ES": "Estonia"

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


Do Arg Stack At Unchanged 11
if the following are true:
  • expression state at time 11 = "call_function_begin"
  • arguments stack at time 11 = [ [ entry "MX": "Mexico", [ ] ], [ ] ]

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


Do Parent Stack At Unchanged 11
if the following are true:
  • expression state at time 11 = "call_function_begin"
  • parent stack at time 11 = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]

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


Do Control Map At Unchanged 11
if the following are true:
  • expression state at time 11 = "call_function_begin"
  • Control Map at time 11 = [ ]

then Control Map at time 12 = [ ]


Do Variables At Unchanged 11
if the following are true:
  • expression state at time 11 = "call_function_begin"
  • Variables Map at time 11 = [ ]

then Variables Map at time 12 = [ ]


Do Line At Unchanged 11
if the following are true:
  • expression state at time 11 = "call_function_begin"
  • the line at time 11 = 1

then the line at time 12 = 1


Do Tab At Unchanged 11
if the following are true:
  • expression state at time 11 = "call_function_begin"
  • the tab at time 11 = 0

then the tab at time 12 = 0


Do Stack At Unchanged 11
if the following are true:
  • expression state at time 11 = "call_function_begin"
  • stack at time 11 = [ ]

then stack at time 12 = [ ]


Do Class Defs At Unchanged 11
if the following are true:
  • expression state at time 11 = "call_function_begin"
  • Class Map at time 11 = [ ]

then Class Map at time 12 = [ ]


Get New State 12
if expression state at time 12 = "return", then expression state at time 13 = "iterate_args"

Get Return Value 12
if the following are true:
  • expression state at time 12 = "return"
  • Value Stack at time 12 = [ [ ], [ ] ]
  • Return Value at time 12 = entry "ES": "Estonia"

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


Do Variables At Unchanged 12
if the following are true:
  • expression state at time 12 = "return"
  • Variables Map at time 12 = [ ]

then Variables Map at time 13 = [ ]


Do Line At Unchanged 12
if the following are true:
  • expression state at time 12 = "return"
  • the line at time 12 = 1

then the line at time 13 = 1


Do Tab At Unchanged 12
if the following are true:
  • expression state at time 12 = "return"
  • the tab at time 12 = 0

then the tab at time 13 = 0


Do Arg Stack At Unchanged 12
if the following are true:
  • expression state at time 12 = "return"
  • arguments stack at time 12 = [ [ entry "MX": "Mexico", [ ] ], [ ] ]

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


Do Parent Stack At Unchanged 12
if the following are true:
  • expression state at time 12 = "return"
  • parent stack at time 12 = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]

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


Do Stack At Unchanged 12
if the following are true:
  • expression state at time 12 = "return"
  • stack at time 12 = [ ]

then stack at time 13 = [ ]


Do Class Defs At Unchanged 12
if the following are true:
  • expression state at time 12 = "return"
  • Class Map at time 12 = [ ]

then Class Map at time 13 = [ ]


Do Object Store At Unchanged 12
if the following are true:
  • expression state at time 12 = "return"
  • Python Object Store at time 12 = [ ]

then Python Object Store at time 13 = [ ]


Do Control Map At Unchanged 12
if the following are true:
  • expression state at time 12 = "return"
  • Control Map at time 12 = [ ]

then Control Map at time 13 = [ ]


Get Iterate Expr 13
if the following are true:
  • expression state at time 13 = "iterate_args"
  • arguments stack at time 13 = [ [ entry "MX": "Mexico", [ ] ], [ ] ]

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


Get Iterate Params 13
if the following are true:
  • expression state at time 13 = "iterate_args"
  • arguments stack at time 13 = [ [ entry "MX": "Mexico", [ ] ], [ ] ]

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


Get Iterate State 13
if the following are true:
  • expression state at time 13 = "iterate_args"
  • arguments stack at time 13 = [ [ entry "MX": "Mexico", [ ] ], [ ] ]

then expression state at time 14 = "begin_expr"


Get Iterate Parent 13
if the following are true:
  • expression state at time 13 = "iterate_args"
  • arguments stack at time 13 = [ [ entry "MX": "Mexico", [ ] ], [ ] ]
  • parent stack at time 13 = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]

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


Do Value Stack At Unchanged 13
if the following are true:
  • expression state at time 13 = "iterate_args"
  • Value Stack at time 13 = [ [ entry "ES": "Estonia", [ ] ], [ ] ]

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


Do Line At Unchanged 13
if the following are true:
  • expression state at time 13 = "iterate_args"
  • the line at time 13 = 1

then the line at time 14 = 1


Do Tab At Unchanged 13
if the following are true:
  • expression state at time 13 = "iterate_args"
  • the tab at time 13 = 0

then the tab at time 14 = 0


Do Stack At Unchanged 13
if the following are true:
  • expression state at time 13 = "iterate_args"
  • stack at time 13 = [ ]

then stack at time 14 = [ ]


Do Object Store At Unchanged 13
if the following are true:
  • expression state at time 13 = "iterate_args"
  • Python Object Store at time 13 = [ ]

then Python Object Store at time 14 = [ ]


Do Control Map At Unchanged 13
if the following are true:
  • expression state at time 13 = "iterate_args"
  • Control Map at time 13 = [ ]

then Control Map at time 14 = [ ]


Do Variables At Unchanged 13
if the following are true:
  • expression state at time 13 = "iterate_args"
  • Variables Map at time 13 = [ ]

then Variables Map at time 14 = [ ]


Do Class Defs At Unchanged 13
if the following are true:
  • expression state at time 13 = "iterate_args"
  • Class Map at time 13 = [ ]

then Class Map at time 14 = [ ]


Get Begin Expr Value 14
if the following are true:
  • expression state at time 14 = "begin_expr"
  • the expression at time 14 = entry "MX": "Mexico"
  • Value Stack at time 14 = [ [ entry "ES": "Estonia", [ ] ], [ ] ]

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


Get Begin Expr Parent 14
if the following are true:
  • expression state at time 14 = "begin_expr"
  • the expression at time 14 = entry "MX": "Mexico"
  • parent stack at time 14 = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]

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


Get Begin Expr Params 14
if the following are true:
  • expression state at time 14 = "begin_expr"
  • the expression at time 14 = entry "MX": "Mexico"
  • arguments stack at time 14 = [ [ ], [ ] ]

then arguments stack at time 15 = [ [ "MX", [ "Mexico", [ ] ] ], [ [ ], [ ] ] ]


Get Begin Expr Call State 14
if the following are true:
  • expression state at time 14 = "begin_expr"
  • the expression at time 14 = entry "MX": "Mexico"

then expression state at time 15 = "iterate_args"


Do Expr At Unchanged 14
if the following are true:
  • expression state at time 14 = "begin_expr"
  • the expression at time 14 = entry "MX": "Mexico"

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


Do Variables At Unchanged 14
if the following are true:
  • expression state at time 14 = "begin_expr"
  • Variables Map at time 14 = [ ]

then Variables Map at time 15 = [ ]


Do Line At Unchanged 14
if the following are true:
  • expression state at time 14 = "begin_expr"
  • the line at time 14 = 1

then the line at time 15 = 1


Do Tab At Unchanged 14
if the following are true:
  • expression state at time 14 = "begin_expr"
  • the tab at time 14 = 0

then the tab at time 15 = 0


Do Stack At Unchanged 14
if the following are true:
  • expression state at time 14 = "begin_expr"
  • stack at time 14 = [ ]

then stack at time 15 = [ ]


Do Object Store At Unchanged 14
if the following are true:
  • expression state at time 14 = "begin_expr"
  • Python Object Store at time 14 = [ ]

then Python Object Store at time 15 = [ ]


Do Control Map At Unchanged 14
if the following are true:
  • expression state at time 14 = "begin_expr"
  • Control Map at time 14 = [ ]

then Control Map at time 15 = [ ]


Do Class Defs At Unchanged 14
if the following are true:
  • expression state at time 14 = "begin_expr"
  • Class Map at time 14 = [ ]

then Class Map at time 15 = [ ]


Get Iterate Expr 15
if the following are true:
  • expression state at time 15 = "iterate_args"
  • arguments stack at time 15 = [ [ "MX", [ "Mexico", [ ] ] ], [ [ ], [ ] ] ]

then the expression at time 16 = "MX"


Get Iterate Params 15
if the following are true:
  • expression state at time 15 = "iterate_args"
  • arguments stack at time 15 = [ [ "MX", [ "Mexico", [ ] ] ], [ [ ], [ ] ] ]

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


Get Iterate State 15
if the following are true:
  • expression state at time 15 = "iterate_args"
  • arguments stack at time 15 = [ [ "MX", [ "Mexico", [ ] ] ], [ [ ], [ ] ] ]

then expression state at time 16 = "begin_expr"


Get Iterate Parent 15
if the following are true:
  • expression state at time 15 = "iterate_args"
  • arguments stack at time 15 = [ [ "MX", [ "Mexico", [ ] ] ], [ [ ], [ ] ] ]
  • parent stack at time 15 = [ entry "MX": "Mexico", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

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


Do Value Stack At Unchanged 15
if the following are true:
  • expression state at time 15 = "iterate_args"
  • Value Stack at time 15 = [ [ ], [ [ entry "ES": "Estonia", [ ] ], [ ] ] ]

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


Do Line At Unchanged 15
if the following are true:
  • expression state at time 15 = "iterate_args"
  • the line at time 15 = 1

then the line at time 16 = 1


Do Tab At Unchanged 15
if the following are true:
  • expression state at time 15 = "iterate_args"
  • the tab at time 15 = 0

then the tab at time 16 = 0


Do Stack At Unchanged 15
if the following are true:
  • expression state at time 15 = "iterate_args"
  • stack at time 15 = [ ]

then stack at time 16 = [ ]


Do Object Store At Unchanged 15
if the following are true:
  • expression state at time 15 = "iterate_args"
  • Python Object Store at time 15 = [ ]

then Python Object Store at time 16 = [ ]


Do Control Map At Unchanged 15
if the following are true:
  • expression state at time 15 = "iterate_args"
  • Control Map at time 15 = [ ]

then Control Map at time 16 = [ ]


Do Variables At Unchanged 15
if the following are true:
  • expression state at time 15 = "iterate_args"
  • Variables Map at time 15 = [ ]

then Variables Map at time 16 = [ ]


Do Class Defs At Unchanged 15
if the following are true:
  • expression state at time 15 = "iterate_args"
  • Class Map at time 15 = [ ]

then Class Map at time 16 = [ ]


Get Begin Expr State 16
if the following are true:
  • the expression at time 16 = "MX"
  • expression state at time 16 = "begin_expr"
  • "MX" is constant
  • parent stack at time 16 = [ entry "MX": "Mexico", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

then expression state at time 17 = "return"


Get Begin Expr Value Unchaged 16
if the following are true:
  • the expression at time 16 = "MX"
  • expression state at time 16 = "begin_expr"
  • "MX" is constant
  • Value Stack at time 16 = [ [ ], [ [ entry "ES": "Estonia", [ ] ], [ ] ] ]

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


Get Begin Expr Params Unchanged16
if the following are true:
  • the expression at time 16 = "MX"
  • expression state at time 16 = "begin_expr"
  • "MX" is constant
  • arguments stack at time 16 = [ [ "Mexico", [ ] ], [ [ ], [ ] ] ]

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


Get Begin Expr Return 16
if the following are true:
  • expression state at time 16 = "begin_expr"
  • the expression at time 16 = "MX"
  • "MX" is constant

then Return Value at time 17 = "MX"


Get Begin Expr Const Parent 16
if the following are true:
  • expression state at time 16 = "begin_expr"
  • the expression at time 16 = "MX"
  • "MX" is constant
  • parent stack at time 16 = [ entry "MX": "Mexico", [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] ]

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


Do Line At Unchanged 16
if the following are true:
  • expression state at time 16 = "begin_expr"
  • the line at time 16 = 1

then the line at time 17 = 1


Do Tab At Unchanged 16
if the following are true:
  • expression state at time 16 = "begin_expr"
  • the tab at time 16 = 0

then the tab at time 17 = 0


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 = [ ]

then Python Object Store at time 17 = [ ]


Do Control Map At Unchanged 16
if the following are true:
  • expression state at time 16 = "begin_expr"
  • Control Map at time 16 = [ ]

then Control Map at time 17 = [ ]


Do Variables At Unchanged 16
if the following are true:
  • expression state at time 16 = "begin_expr"
  • Variables Map at time 16 = [ ]

then Variables Map at time 17 = [ ]


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 New State 17
if expression state at time 17 = "return", then expression state at time 18 = "iterate_args"


Pages: 149 150 151 ... 193