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.

Returning Property

if the following are true:

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


Call End Object

if the following are true:

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


Not expression

if expression state at time t = "end_expr", then expression state at time (t + 1) = "not_expr"


Computer ADDI Instruction, Concise

if the following are true:

then byte at ID: c, cell #dst at time (t + 1) = (byte at ID: c, cell #src at time t) + imm


Computer ADDI Instruction, Others

if the following are true:

then byte at ID: c, cell #other at time (t + 1) = byte at ID: c, cell #other at time t


Computer SUBTRACTI Instruction

if the following are true:

then byte at ID: c, cell #dst at time (t + 1) = (byte at ID: c, cell #src at time t) - imm


Computer SUBTRACTI Instruction, Others

if the following are true:

then byte at ID: c, cell #other at time (t + 1) = byte at ID: c, cell #other at time t


Computer ADD Instruction

if the following are true:

then byte at ID: c, cell #d at time (t + 1) = (byte at ID: c, cell #s1 at time t) + (byte at ID: c, cell #s2 at time t)


Computer ADD Instruction, Others

if the following are true:

then byte at ID: c, cell #other at time (t + 1) = byte at ID: c, cell #other at time t


Computer STORE Instruction

if the following are true:

then byte at ID: c, cell #((byte at ID: c, cell #addr at time t) + imm) at time (t + 1) = byte at ID: c, cell #src at time t


Computer STORE Instruction, Others

if the following are true:

then byte at ID: c, cell #other at time (t + 1) = byte at ID: c, cell #other at time t


Computer Load Instruction

if the following are true:

then byte at ID: c, cell #dst at time (t + 1) = byte at ID: c, cell #((byte at ID: c, cell #addr at time t) + imm) at time t


Computer LOAD Instruction, Others

if the following are true:

then byte at ID: c, cell #other at time (t + 1) = byte at ID: c, cell #other at time t


Computer BEQ on Memory

if the following are true:

then byte at ID: c, cell #x at time (t + 1) = byte at ID: c, cell #x at time t


Computer BEQ on Equal

if the following are true:

then the PC at computer c and time (t + 1) = (i + 1) + imm


Computer BEQ on Not Equal

if the following are true:

then the PC at computer c and time (t + 1) = i + 1


Computer J Instruction

if the following are true:

then the PC at computer c and time (t + 1) = jump_to


Computer J on Memory

if the following are true:

then byte at ID: c, cell #x at time (t + 1) = byte at ID: c, cell #x at time t


Computer JR Instruction

if the following are true:

then the PC at computer c and time (t + 1) = byte at ID: c, cell #addr at time t


Computer JR on Memory

if the following are true:

then byte at ID: c, cell #x at time (t + 1) = byte at ID: c, cell #x at time t


Computer JAL To

if the following are true:

then the PC at computer c and time (t + 1) = jump_to


Computer JAL Instruction, Memory

if the following are true:

then byte at ID: c, cell #x at time (t + 1) = byte at ID: c, cell #x at time t


Computer JAL Return

if the following are true:

then byte at ID: c, cell #2 at time (t + 1) = i + 1


Computer Program Counter on ADDI

if the following are true:

then the PC at computer c and time (t + 1) = x + 1


Computer Program Counter on ADD

if the following are true:

then the PC at computer c and time (t + 1) = x + 1


Computer Program Counter on SUBTRACTI

if the following are true:

then the PC at computer c and time (t + 1) = x + 1


Computer Program Counter on STORE

if the following are true:

then the PC at computer c and time (t + 1) = x + 1


Computer Program Counter on LOAD

if the following are true:

then the PC at computer c and time (t + 1) = x + 1


Computer Keyboard Interrupt

if interrupt at computer: c index: 0 time: t = 1, then the PC at computer c and time (t + 1) = 1


Computer Some Device Interrupted Computer (1)

if interrupt at computer: c index: x time: t = 1, then interrupt at computer: c index: x time: (t + 1) = 0


Computer Some Device Interrupted Computer (2)

if interrupt at computer: c index: x time: t = 1, then byte at ID: c, cell #idx at time (t + 1) = byte at ID: c, cell #idx at time t


Computer Display Interrupt (1)

if the following are true:

then display text at x: (cursor x at time t), y: (cursor y at time t), and time: (t + 1) = byte at ID: c, cell #(10 + (number of characters read at t)) at time t


Computer Display Interrupt (2)

if the following are true:

then number of characters read at (t + 1) = (number of characters read at t) + 1


Computer Display Finished (1)

if the following are true:

then byte at ID: c, cell #27 at time (t + 1) = 0


Computer Display Finished (2)

if the following are true:

then number of characters read at (t + 1) = 0


Computer Display Finished (3)

if the following are true:

then cursor x at time (t + 1) = cursor x at time t


Computer Display Finished (4)

if the following are true:

then cursor y at time (t + 1) = cursor y at time t


Computer Number of Characters Read Unchanged (1)

if byte at ID: c, cell #27 at time t = 0, then number of characters read at (t + 1) = number of characters read at t


Computer Number of Characters Read Unchanged (2)

if byte at ID: c, cell #27 at time t = 0, then cursor x at time (t + 1) = cursor x at time t


Computer Number of Characters Read Unchanged (3)

if byte at ID: c, cell #27 at time t = 0, then cursor y at time (t + 1) = cursor y at time t


Computer Display Cursor X Move (1)

if the following are true:

then cursor x at time (t + 1) = (cursor x at time t) + 1


Computer Display Cursor X Move (2)

if the following are true:

then cursor y at time (t + 1) = cursor y at time t


Computer Display Cursor X New

if the following are true:

then cursor x at time (t + 1) = 0


Computer Display Cursor Y New

if the following are true:

then cursor y at time (t + 1) = (cursor y at time t) + 1


Computer Display Cursor Y Stay In Bottom

if cursor y at time t = 11, then cursor y at time (t + 1) = cursor y at time t


Computer Display Text Move Up

if the following are true:

then display text at x: x, y: y, and time: (t + 1) = display text at x: x, y: (y + 1), and time: t


Computer Cursor X on CR

if the following are true:

then cursor x at time (t + 1) = 0


Computer Cursor Y on CR

if the following are true:

then cursor y at time (t + 1) = (cursor y at time t) + 1


Computer CR move text up (1)

if the following are true:

then cursor y at time (t + 1) = cursor y at time t


Computer CR move text up (2)

if the following are true:

then display text at x: x, y: y, and time: (t + 1) = display text at x: x, y: (y + 1), and time: t


Computer Disk Interrupt

if interrupt at computer: c index: 1 time: t = 1, then the PC at computer c and time (t + 1) = 2


Computer Write To Disk

if the following are true:

then disk byte at index: ((value of cell 47 at time t) + (disk bytes read at time t)) time: (t + 1) = value of cell (30 + (disk bytes read at time t)) at time t


Computer Write To Disk Unchanged

if the following are true:

then disk byte at index: index time: (t + 1) = disk byte at index: index time: t


Computer Increment Disk Bytes Read

if the following are true:

then disk bytes read at time (t + 1) = (disk bytes read at time t) + 1


Computer Disk Write Finished (1)

if the following are true:

then byte at ID: c, cell #49 at time (t + 1) = 0


Computer Disk Write Finished (2)

if the following are true:

then disk bytes read at time (t + 1) = 0


Computer Disk Write Finished (3)

if the following are true:

then disk byte at index: index time: (t + 1) = disk byte at index: index time: t


Computer Written To Disk Unchanged (1)

if byte at ID: c, cell #49 at time t = 0, then disk bytes read at time (t + 1) = disk bytes read at time t


Computer Written To Disk Unchanged (2)

if byte at ID: c, cell #49 at time t = 0, then disk byte at index: index time: (t + 1) = disk byte at index: index time: t


Computer Read from Disk

if the following are true:

then byte at ID: c, cell #(30 + (disk bytes read at time t)) at time (t + 1) = disk byte at index: ((byte at ID: c, cell #47 at time t) + (disk bytes read at time t)) time: t


Computer Disk Read Finished

if the following are true:

then interrupt at computer: c index: 1 time: (t + 1) = 1


Computer Disk Read Unchanged

if the following are true:

then disk byte at index: index time: (t + 1) = disk byte at index: index time: t


Send To Other device on Network (1)

if the following are true:

then byte at ID: y, cell #(50 + (network bytes read from computer: x at time t)) at time (t + 1) = byte at ID: x, cell #(50 + (network bytes read from computer: x at time t)) at time t


Send To Other device on Network (2)

if the following are true:

then network bytes read from computer: x at time (t + 1) = (network bytes read from computer: x at time t) + 1


Finished sending (1)

if the following are true:

then interrupt at computer: y index: 2 time: (t + 1) = 1


Finished sending (2)

if the following are true:

then byte at ID: x, cell #68 at time (t + 1) = 0


Finished sending (3)

if the following are true:

then network bytes read from computer: x at time (t + 1) = 0


Finished sending (4)

if the following are true:

then byte at ID: y, cell #66 at time (t + 1) = byte at ID: x, cell #66 at time t


Network Interrupted Computer

if interrupt at computer: x index: 2 time: t = 1, then the PC at computer x and time (t + 1) = 3


Network Read Unchanged

if byte at ID: x, cell #68 at time t = 0, then network bytes read from computer: x at time (t + 1) = network bytes read from computer: x at time t


Begin List (1)

if the following are true:

then the expression at time (t + 1) = Python list elements


Begin List (2)

if the following are true:

then expression state at time (t + 1) = "begin_expr"


Begin List (3)

if the following are true:

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


Begin List (4)

if the following are true:

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


Begin List (5)

if the following are true:

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


Begin List (6)

if the following are true:

then parent stack at time (t + 1) = [ ]


Begin List (7)

if the following are true:

then arguments stack at time (t + 1) = [ ]


Begin List (8)

if the following are true:

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


Begin List (9)

if the following are true:

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


Begin List Elements (1)

if the following are true:

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


Begin List Elements (2)

if the following are true:

then parent stack at time (t + 1) = [ Python list elements, parent stack at time t ]


Begin List Elements (3)

if the following are true:

then arguments stack at time (t + 1) = [ elements, arguments stack at time t ]


Begin List Elements (4)

if the following are true:

then expression state at time (t + 1) = "iterate_args"


Call Func List (1)

if the following are true:

then Return Value at time (t + 1) = Python reference (length of stack (Python Object Store at time t))


Call Func List (2)

if the following are true:

then Python Object Store at time (t + 1) = result of appending (Python list (reverse of values)) to (Python Object Store at time t)


Call Func List (3)

if the following are true:

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


Call List Return

if the following are true:

then expression state at time (t + 1) = "return"


Call List End

if the following are true:

then expression state at time (t + 1) = "end_expr"


List Unchanged (1)

if the following are true:

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


List Unchanged (2)

if the following are true:

then stack at time (t + 1) = stack at time t


List Unchanged (3)

if the following are true:

then "if" map at time (t + 1) = "if" map at time t


List Unchanged (4)

if the following are true:

then 'while stack' at time (t + 1) = 'while stack' at time t


List Unchanged (5)

if the following are true:

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


Assign List (1)

if the following are true:

then the expression at time (t + 1) = Python list elements


Assign List (2)

if the following are true:

then expression state at time (t + 1) = "begin_expr"


Assign List (3)

if the following are true:

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


Assign List (4)

if the following are true:

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


Assign List (5)

if the following are true:

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


Assign List (6)

if the following are true:

then stack at time (t + 1) = stack at time t


Assign List (7)

if the following are true:

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


Pages: 9 10 11 ... 20