Conditional Properties

if a = b, then b = a

if the following are true:

• a = b
• b = c

then a = c

if the following are true:

• a
• a = b

then b

if a = b, then a + c = b + c

if a = b, then a ⋅ c = b ⋅ c

if not (a = 0), then 0 / a = 0

if not (a = 0), then a / a = 1

if not (b = 0), then a / b = a ⋅ (1 / b)

if a > b, then b < a

if a < b, then b > a

if the following are true:

• a < b
• b = c

then a < c

if the following are true:

• a < b
• a = c

then c < b

if the following are true:

• a < b
• b < c

then a < c

if a < b, then a + c < b + c

if a < b, then a - c < b - c

if the following are true:

• a < b
• c > 0

then a ⋅ c < b ⋅ c

if the following are true:

• a < b
• c > 0

then a / c < b / c

if the following are true:

• a < b
• c < 0

then a ⋅ c > b ⋅ c

if the following are true:

• a < b
• c < 0

then a / c > b / c

if the following are true:

• a > 0
• b > 0
• a < b

then 1 / a > 1 / b

if the following are true:

• a = b + c
• c > 0

then a > b

if a > 0, then not (a = 0)

if the following are true:

• a > 0
• b > 0

then a ⋅ b > 0

if a = b, then x + a = x + b

if the following are true:

• instruction #i is addi dst=dst src=src imm=imm
• the PC at time t = i

then value of cell dst at time (t + 1) = (value of cell src at time t) + imm

if the following are true:

• instruction #i is addi dst=dst src=src imm=imm
• the PC at time t = i
• not (other = dst)

then value of cell other at time (t + 1) = value of cell other at time t

if the following are true:

• subtract immediate instruction with dst: dst src: src and immediate: imm at i
• the PC at time t = i

then value of cell dst at time (t + 1) = (value of cell src at time t) - imm

if the following are true:

• subtract immediate instruction with dst: dst src: src and immediate: imm at i
• the PC at time t = i
• not (other = dst)

then value of cell other at time (t + 1) = value of cell other at time t

if the following are true:

• instruction #i is add dst=d src1=s1 src2=s2
• the PC at time t = i

then value of cell d at time (t + 1) = (value of cell s1 at time t) + (value of cell s2 at time t)

if the following are true:

• instruction #i is add dst=d src1=s1 src2=s2
• the PC at time t = i
• not (other = d)

then value of cell other at time (t + 1) = value of cell other at time t

if the following are true:

• instruction #i is store src=src addr=addr imm=imm
• the PC at time t = i

then value of cell ((value of cell addr at time t) + imm) at time (t + 1) = value of cell src at time t

if the following are true:

• instruction #i is store src=src addr=addr imm=imm
• the PC at time t = i
• not (other = (value of cell addr at time t) + imm)

then value of cell other at time (t + 1) = value of cell other at time t

if the following are true:

• instruction #i is load dst=dst addr=addr imm=imm
• the PC at time t = i

then value of cell dst at time (t + 1) = value of cell ((value of cell addr at time t) + imm) at time t

if the following are true:

• instruction #i is load dst=dst addr=addr imm=imm
• the PC at time t = i
• not (other = dst)

then value of cell other at time (t + 1) = value of cell other at time t

if the following are true:

• instruction #i is beq left=l right=r imm=imm
• the PC at time t = i

then value of cell x at time (t + 1) = value of cell x at time t

if the following are true:

• instruction #i is beq left=left right=right imm=imm
• the PC at time t = i
• value of cell left at time t = value of cell right at time t

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

if the following are true:

• instruction #i is beq left=left right=right imm=imm
• the PC at time t = i
• not (value of cell left at time t = value of cell right at time t)

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

if the following are true:

• instruction #i is jump imm=jump_to
• the PC at time t = i

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

if the following are true:

• instruction #i is jump imm=jump_to
• the PC at time t = i

then value of cell x at time (t + 1) = value of cell x at time t

if the following are true:

• instruction #i is jumpr addr=addr
• the PC at time t = i

then the PC at time (t + 1) = value of cell addr at time t

if the following are true:

• instruction #i is jumpr addr=addr
• the PC at time t = i

then value of cell x at time (t + 1) = value of cell x at time t

if the following are true:

• instruction #i is a JAL instruction with jump to: jump_to
• the PC at time t = i

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

if the following are true:

• instruction #i is a JAL instruction with jump to: jump_to
• the PC at time t = i
• not (x = 2)

then value of cell x at time (t + 1) = value of cell x at time t

if the following are true:

• instruction #i is a JAL instruction with jump to: jump_to
• the PC at time t = i

then value of cell 2 at time (t + 1) = i + 1

if the following are true:

• instruction #x is addi dst=s src=d imm=imm
• the PC at time t = x

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

if the following are true:

• instruction #x is add dst=s src1=d src2=imm
• the PC at time t = x

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

if the following are true:

• subtract immediate instruction with dst: s src: d and immediate: imm at x
• the PC at time t = x

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

if the following are true:

• instruction #x is store src=s addr=d imm=imm
• the PC at time t = x

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

if the following are true:

• instruction #x is load dst=s addr=d imm=imm
• the PC at time t = x

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

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

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

if interrupt at index: x time: t = 1, then value of cell idx at time (t + 1) = value of cell idx at time t

if the following are true:

• value of cell 27 at time t = 1
• number of characters read at t < value of cell 26 at time t

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

if the following are true:

• value of cell 27 at time t = 1
• number of characters read at t < value of cell 26 at time t

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

if the following are true:

• value of cell 27 at time t = 1
• number of characters read at t = value of cell 26 at time t

then value of cell 27 at time (t + 1) = 0

if the following are true:

• value of cell 27 at time t = 1
• number of characters read at t = value of cell 26 at time t

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

if the following are true:

• value of cell 27 at time t = 1
• number of characters read at t = value of cell 26 at time t

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

if the following are true:

• value of cell 27 at time t = 1
• number of characters read at t = value of cell 26 at time t

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

if value of cell 27 at time t = 0, then number of characters read at (t + 1) = number of characters read at t

if value of cell 27 at time t = 0, then cursor x at time (t + 1) = cursor x at time t

if value of cell 27 at time t = 0, then cursor y at time (t + 1) = cursor y at time t

if the following are true:

• value of cell 27 at time t = 1
• cursor x at time t < 39

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

if the following are true:

• value of cell 27 at time t = 1
• cursor x at time t < 39

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

if the following are true:

• value of cell 27 at time t = 1
• cursor x at time t = 39

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

if the following are true:

• value of cell 27 at time t = 1
• cursor x at time t = 39
• cursor y at time t < 11

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

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

if the following are true:

• value of cell 27 at time t = 1
• cursor x at time t = 39
• cursor y at time t = 11

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

if the following are true:

• value of cell 27 at time t = 1
• value of cell (10 + (number of characters read at t)) at time t = 13

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

if the following are true:

• value of cell 27 at time t = 1
• value of cell (10 + (number of characters read at t)) at time t = 13
• cursor y at time t < 11

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

if the following are true:

• value of cell 27 at time t = 1
• value of cell (10 + (number of characters read at t)) at time t = 13
• cursor y at time t = 11

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

if the following are true:

• value of cell 27 at time t = 1
• value of cell (10 + (number of characters read at t)) at time t = 13
• cursor y at time t = 11

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

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

if the following are true:

• value of cell 49 at time t = 1
• value of cell 48 at time t = 1
• disk bytes read at time t < value of cell 46 at time t

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

if the following are true:

• value of cell 49 at time t = 1
• value of cell 48 at time t = 1
• not (index = (value of cell 47 at time t) + (disk bytes read at time t))

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

if the following are true:

• value of cell 49 at time t = 1
• disk bytes read at time t < value of cell 46 at time t

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

if the following are true:

• value of cell 49 at time t = 1
• disk bytes read at time t = value of cell 46 at time t

then value of cell 49 at time (t + 1) = 0

if the following are true:

• value of cell 49 at time t = 1
• disk bytes read at time t = value of cell 46 at time t

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

if the following are true:

• value of cell 49 at time t = 1
• disk bytes read at time t = value of cell 46 at time t

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

if value of cell 49 at time t = 0, then disk bytes read at time (t + 1) = disk bytes read at time t

if value of cell 49 at time t = 0, then disk byte at index: index time: (t + 1) = disk byte at index: index time: t

if the following are true:

• value of cell 49 at time t = 1
• value of cell 48 at time t = 0
• disk bytes read at time t < value of cell 46 at time t

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

if the following are true:

• value of cell 49 at time t = 1
• disk bytes read at time t = value of cell 46 at time t
• value of cell 48 at time t = 0

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

if the following are true:

• value of cell 49 at time t = 1
• value of cell 48 at time t = 0

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

if the following are true:

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = Python list elements
• Expression Stack at time t = [ ]

then Expression Stack at time (t + 1) = [ [ Python list elements, [ ] ], [ ] ]

if the following are true:

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = Python list elements
• Expression Stack at time t = [ ]

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

if the following are true:

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = Python list elements
• Expression Stack at time t = [ ]

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

if the following are true:

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = Python list elements
• Expression Stack at time t = [ ]

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

if the following are true:

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = Python list elements
• Expression Stack at time t = [ ]

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

if the following are true:

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = Python list elements
• Expression Stack at time t = [ ]

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

if the following are true:

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = Python list elements
• Expression Stack at time t = [ ]

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

if the following are true:

• the line at time t = i
• the tab at time t = j
• statement at line i, tab j = Python list elements
• Expression Stack at time t = [ ]

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

if Expression Stack at time t = [ [ Python list elements, ys ], rest ], then Expression Stack at time (t + 1) = [ elements, [ [ Python list elements, ys ], rest ] ]

if Expression Stack at time t = [ [ Python list elements, ys ], rest ], then Value Stack at time (t + 1) = [ [ ], Value Stack at time t ]

if Expression Stack at time t = [ [ Python list elements, ys ], rest ], then Parameters List at time (t + 1) = None

if Expression Stack at time t = [ [ Python list elements, ys ], rest ], then the line at time (t + 1) = the line at time t

if Expression Stack at time t = [ [ Python list elements, ys ], rest ], then the tab at time (t + 1) = the tab at time t

if Expression Stack at time t = [ [ Python list elements, ys ], rest ], then Variables Map at time (t + 1) = Variables Map at time t

if Expression Stack at time t = [ [ Python list elements, ys ], rest ], then Control Map at time (t + 1) = Control Map at time t

if Expression Stack at time t = [ [ Python list elements, ys ], rest ], then Python Object Store at time (t + 1) = Python Object Store at time t

if Expression Stack at time t = [ [ Python list elements, ys ], rest ], then Context Stack at time (t + 1) = Context Stack at time t