Conditional Properties

In each statement, if the test expression is true, then the conclusion expression is also assumed to be true. Conditional properties are used to prove theorems.

Unchanged On Else (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = else:

then Expression Stack at time (t + 1) = [ ]

Decrement Tab At End of If (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)

then the line at time (t + 1) = i

Decrement Tab At End of If (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)

then the tab at time (t + 1) = j - 1

Decrement Tab At End of If (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)

then Variables Map at time (t + 1) = Variables Map at time t

Decrement Tab At End of If (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)

then Context Stack at time (t + 1) = Context Stack at time t

Decrement Tab At End of If (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)

then Python Object Store at time (t + 1) = Python Object Store at time t

Decrement Tab At End of If (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)

then Class Map at time (t + 1) = Class Map at time t

Decrement Tab At End of If (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab k = s
k < j
value at (j - 1) in map (Control Map at time t) = pair ("if", if_value)

then Control Map at time (t + 1) = Control Map at time t

Begin While Test (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = while test:
Expression Stack at time t = [ ]

then Expression Stack at time (t + 1) = [ [ test, [ ] ], [ ] ]

Begin While Test (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = while test:
Expression Stack at time t = [ ]

then the line at time (t + 1) = i

Begin While Test (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = while test:
Expression Stack at time t = [ ]

then the tab at time (t + 1) = j

Begin While Test (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = while test:
Expression Stack at time t = [ ]

then Value Stack at time (t + 1) = [ [ ], [ ] ]

Begin While Test (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = while test:
Expression Stack at time t = [ ]

then Python Object Store at time (t + 1) = Python Object Store at time t

Begin While Test (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = while test:
Expression Stack at time t = [ ]

then Control Map at time (t + 1) = Control Map at time t

Begin While Test (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = while test:
Expression Stack at time t = [ ]

then Variables Map at time (t + 1) = Variables Map at time t

Begin While Test (8)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = while test:
Expression Stack at time t = [ ]

then Context Stack at time (t + 1) = Context Stack at time t

Unchanged During While

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = while test:

then Class Map at time (t + 1) = Class Map at time t

While Ended (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = while test:
Expression Stack at time t = [ [ ], [ ] ]

then the line at time (t + 1) = i + 1

While Ended (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = while test:
Expression Stack at time t = [ [ ], [ ] ]

then Python Object Store at time (t + 1) = Python Object Store at time t

While Ended (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = while test:
Expression Stack at time t = [ [ ], [ ] ]

then Variables Map at time (t + 1) = Variables Map at time t

While Ended (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = while test:
Expression Stack at time t = [ [ ], [ ] ]

then Context Stack at time (t + 1) = Context Stack at time t

While Test Is True (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (function call with name: name and arguments: args)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ True, [ ] ], [ ] ]

then the tab at time (t + 1) = j + 1

While Test Is True (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (function call with name: name and arguments: args)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ True, [ ] ], [ ] ]

then Control Map at time (t + 1) = result of storing (pair ("while", i)) at key: j in map: (Control Map at time t)

While Test Is False (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (function call with name: name and arguments: args)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ False, [ ] ], [ ] ]

then the tab at time (t + 1) = j

While Test Is False (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = "while" statement with condition (function call with name: name and arguments: args)
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ False, [ ] ], [ ] ]

then Control Map at time (t + 1) = Control Map at time t

On Break Statement (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

then "break" state at (t + 1) = "breaking"

On Break Statement (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

then the line at time (t + 1) = i

On Break Statement (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

then the tab at time (t + 1) = j

On Break Statement (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

then Variables Map at time (t + 1) = Variables Map at time t

On Break Statement (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

then Context Stack at time (t + 1) = Context Stack at time t

On Break Statement (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

then Python Object Store at time (t + 1) = Python Object Store at time t

On Break Statement (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

then Control Map at time (t + 1) = Control Map at time t

On Break Statement (8)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = break

then Class Map at time (t + 1) = Class Map at time t

On Continue Statement (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

then "continue" state at (t + 1) = "continuing"

On Continue Statement (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

then the line at time (t + 1) = i

On Continue Statement (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

then the tab at time (t + 1) = j

On Continue Statement (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

then Expression Stack at time (t + 1) = [ ]

On Continue Statement (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

then Variables Map at time (t + 1) = Variables Map at time t

On Continue Statement (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

then Context Stack at time (t + 1) = Context Stack at time t

On Continue Statement (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

then Python Object Store at time (t + 1) = Python Object Store at time t

On Continue Statement (8)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

then Control Map at time (t + 1) = Control Map at time t

On Continue Statement (9)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = continue

then Class Map at time (t + 1) = Class Map at time t

On Function Definition (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = function definition where name: name and parameters: params

then there is a function named name with parameters params at line line

On Function Definition (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = function definition where name: name and parameters: params

then Variables Map at time (t + 1) = Variables Map at time t

On Function Definition (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = function definition where name: name and parameters: params

then the line at time (t + 1) = i + 1

On Function Definition (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = function definition where name: name and parameters: params

then the tab at time (t + 1) = j

On Function Definition (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = function definition where name: name and parameters: params

then Context Stack at time (t + 1) = Context Stack at time t

On Function Definition (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = function definition where name: name and parameters: params

then Python Object Store at time (t + 1) = Python Object Store at time t

On Function Definition (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = function definition where name: name and parameters: params

then Control Map at time (t + 1) = Control Map at time t

On Function Definition (8)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = function definition where name: name and parameters: params

then Class Map at time (t + 1) = Class Map at time t

Return If Stack

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return v

then Class Map at time (t + 1) = Class Map at time t

Object Store On Return Constant

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return c
c is constant

then Python Object Store at time (t + 1) = Python Object Store at time t

Variable Object Store

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return c
c is a variable

then Python Object Store at time (t + 1) = Python Object Store at time t

Return Statement Start (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Expression Stack at time t = [ ]

then Expression Stack at time (t + 1) = [ [ rex, [ ] ], [ ] ]

Return Statement Start (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Expression Stack at time t = [ ]

then Value Stack at time (t + 1) = [ [ ], [ ] ]

Return Statement Start (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Expression Stack at time t = [ ]

then the line at time (t + 1) = i

Return Statement Start (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Expression Stack at time t = [ ]

then the tab at time (t + 1) = j

Return Statement Start (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Expression Stack at time t = [ ]

then Variables Map at time (t + 1) = Variables Map at time t

Return Statement Start (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Expression Stack at time t = [ ]

then Context Stack at time (t + 1) = Context Stack at time t

Return Statement Start (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Expression Stack at time t = [ ]

then Python Object Store at time (t + 1) = Python Object Store at time t

Return Statement Start (8)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Expression Stack at time t = [ ]

then Control Map at time (t + 1) = Control Map at time t

Return Ended Pop Stack (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Context Stack at time t = [ program context with variables: vars and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
Expression Stack at time t = [ [ ], [ ] ]

then Variables Map at time (t + 1) = vars

Return Ended Pop Stack (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Context Stack at time t = [ program context with variables: vars and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
Expression Stack at time t = [ [ ], [ ] ]

then the line at time (t + 1) = line

Return Ended Pop Stack (3)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Context Stack at time t = [ program context with variables: vars and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
Expression Stack at time t = [ [ ], [ ] ]

then the tab at time (t + 1) = tab

Return Ended Pop Stack (4)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Context Stack at time t = [ program context with variables: vars and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
Expression Stack at time t = [ [ ], [ ] ]

then Control Map at time (t + 1) = control_map

Return Ended Pop Stack (5)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Context Stack at time t = [ program context with variables: vars and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
Expression Stack at time t = [ [ ], [ ] ]

then Context Stack at time (t + 1) = rest

Return Ended Pop Stack (6)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Context Stack at time t = [ program context with variables: vars and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
Expression Stack at time t = [ [ ], [ ] ]

then Expression Stack at time (t + 1) = expr_stack

Return Ended Pop Stack (7)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Context Stack at time t = [ program context with variables: vars and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
Expression Stack at time t = [ [ ], [ ] ]

then Value Stack at time (t + 1) = value_stack

Set Return Value At End Of Return Statement

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Expression Stack at time t = [ [ ], [ ] ]
Value Stack at time t = [ [ value, [ ] ], [ ] ]

then Return Value at time (t + 1) = [ value, [ ] ]

Returning Object Store

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = return rex
Expression Stack at time t = [ [ ], [ ] ]

then Python Object Store at time (t + 1) = Python Object Store at time t

Minimum Value

if a is less than (minimum value of stack xs), then minimum value of stack [ a, xs ] = a

Minimum Value Number

if a < minimum value of stack xs, then minimum value of stack [ a, xs ] = a

Minimum Value (2)

if xs is greater than (minimum value of stack xss), then minimum value of stack [ xs, xss ] = minimum value of stack xss

Minimum Value Number (2)

if a > minimum value of stack xs, then minimum value of stack [ a, xs ] = minimum value of stack xs

Maximum Value Number

if a > maximum value in stack xs, then maximum value in stack [ a, xs ] = a

Maximum Value Number (2)

if a < maximum value in stack xs, then maximum value in stack [ a, xs ] = maximum value in stack xs

Less Than Stays True

if compare bit stack xs and bit stack ys = [ 0, [ 0, [ ] ] ], then compare bit stack [ x, xs ] and bit stack [ y, ys ] = [ 0, [ 0, [ ] ] ]

Greater Than Stays True

if compare bit stack xs and bit stack ys = [ 0, [ 1, [ ] ] ], then compare bit stack [ x, xs ] and bit stack [ y, ys ] = [ 0, [ 1, [ ] ] ]

Equal Bits Could Change

if compare bit stack xs and bit stack ys = [ 1, [ 0, [ ] ] ], then compare bit stack [ x, xs ] and bit stack [ y, ys ] = compare bit x and bit y

0 is Less Than

if compare bit stack xs and bit stack ys = [ 0, [ 0, [ ] ] ], then xs is less than ys

2 is Greater Than

if compare bit stack xs and bit stack ys = [ 0, [ 1, [ ] ] ], then xs is greater than ys

Equal Lists

if (x = y) and (xs = ys), then [x,xs] = [y,ys]

Not Equal Lists

if not(x = y), then [x,xs] ≠ [y,ys]

Number is Found

if are_equal_list(number, value): find_number_index([number, remain], value, index) == index

Number is Found (2)

if el = val, then index of value val in [ el, remain ] with current index idx = idx

found value

if el = val, then output of the index_compute function where the input stack is [ el, remain ], value is val, and index is idx = idx

found node (1)

if el = val, then index of value val in [ node (el, left, right), remain ] with current index idx = idx

found node (2)

if el = val, then index of value val in [ node (el, w, p), remain ] with current index idx = idx

Number is Not Found

if are_not_equal_list(number, value): find_number_index([number, remain], value, index) == find_number_index(remain, value, add_uint(index, [1, []]))

Number is Not Found (2)

if not (el = val), then index of value val in [ el, remain ] with current index idx = index of value val in remain with current index (idx + 1)

did not find value

if not (el = val), then output of the index_compute function where the input stack is [ el, remain ], value is val, and index is idx = output of the index_compute function where the input stack is remain, value is val, and index is (idx + 1)

did not find node (1)

if not (el = val), then index of value val in [ node (el, left, right), remain ] with current index idx = index of value val in remain with current index (idx + 1)

did not find node (2)

if not (el = val), then index of value val in [ node (el, w, p), remain ] with current index idx = index of value val in remain with current index (idx + 1)

did not find parent

if the following are true:

not (left = val)
not (right = val)

then find parent index of [ node (el, left, right), remain ] = find parent index of remain

Contains

if x = value, then stack [ x, y ] contains value = True

Contains Iterate

if not (x = value), then stack [ x, y ] contains value = stack y contains value

Set Entry Replace

if entry_key = key, then output of function store_compute where input key is key, value is value, map is [ entry entry_key: entry_value, remaining ], and processed map is kvs = result of dumping kvs to [ entry key: value, remaining ]

set entry key not found

if not (entry_key = key), then output of function store_compute where input key is key, value is value, map is [ entry entry_key: entry_value, remaining ], and processed map is kvs = output of function store_compute where input key is key, value is value, map is remaining, and processed map is [ entry entry_key: entry_value, kvs ]

delete key found

if entry_key = key, then output of function delete_entry where input key is key, map is [ pair (entry_key, value), remaining ], and processed is kvs = result of dumping kvs to remaining

delete key not found

if not (entry_key = key), then output of function delete_entry where input key is key, map is [ pair (entry_key, value), remaining ], and processed is kvs = output of function delete_entry where input key is key, map is remaining, and processed is [ pair (entry_key, value), kvs ]

16 17 18