Conditional Properties

• a = b
• b = c

then a = c

• a
• a = b

then b

• a < b
• b = c

then a < c

• a < b
• a = c

then c < b

• a < b
• b < c

then a < c

• a < b
• c > 0

then a ⋅ c < b ⋅ c

• a < b
• c > 0

then a / c < b / c

• a < b
• c < 0

then a ⋅ c > b ⋅ c

• a < b
• c < 0

then a / c > b / c

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

then 1 / a > 1 / b

• a = b + c
• c > 0

then a > b

• a > 0
• b > 0

then a ⋅ b > 0

• 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

• 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

• 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

• 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

• 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)

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

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

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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

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

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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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, [ ] ], [ ] ]

• 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

• 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

• 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) = [ [ ], [ ] ]

• 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

• 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

• 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

• 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