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.
- 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