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.

On Else (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = else:
value at j in map (Control Map at time t) = pair ("if", False)

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

On Else (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = else:
value at j in map (Control Map at time t) = pair ("if", False)

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

Skip Else Block (1)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = else:
value at j in map (Control Map at time t) = pair ("if", True)

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

Skip Else Block (2)

if the following are true:

the line at time t = i
the tab at time t = j
statement at line i, tab j = else:
value at j in map (Control Map at time t) = pair ("if", True)

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

Unchanged On Else (1)

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 Variables Map at time (t + 1) = Variables Map at time t

Unchanged On Else (2)

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 Context Stack at time (t + 1) = Context Stack at time t

Unchanged On Else (3)

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 Python Object Store at time (t + 1) = Python Object Store at time t

Unchanged On Else (4)

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 Control Map at time (t + 1) = Control Map at time t

Unchanged On Else (5)

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 Class Map at time (t + 1) = Class Map at time t

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)

Pages: 16 17 18 ... 20