Proofs

A proof is a series of claims that lead to a conclusion. Some proofs are conditional, which means that the claims can only be made under certain conditions. Click on a statement to see the proof

Addi Zero Insn 2

if the following are true:

instruction #2 is addi dst=5 src=0 imm=0
the PC at time 2 = 2

then value of cell 5 at time 3 = 0

Pc 2

if the following are true:

instruction #2 is addi dst=5 src=0 imm=0
the PC at time 2 = 2

then the PC at time 3 = 3

Byte 3 Stays the Same 2

if the following are true:

instruction #2 is addi dst=5 src=0 imm=0
the PC at time 2 = 2
value of cell 3 at time 2 = 3

then value of cell 3 at time 3 = 3

Byte 4 Stays the Same 2

if the following are true:

instruction #2 is addi dst=5 src=0 imm=0
the PC at time 2 = 2
value of cell 4 at time 2 = 0

then value of cell 4 at time 3 = 0

Addi Insn 3

if the following are true:

instruction #3 is addi dst=5 src=5 imm=7
the PC at time 3 = 3
value of cell 5 at time 3 = 0

then value of cell 5 at time 4 = 7

Pc 3

if the following are true:

instruction #3 is addi dst=5 src=5 imm=7
the PC at time 3 = 3

then the PC at time 4 = 4

Byte 3 Stays the Same 3

if the following are true:

instruction #3 is addi dst=5 src=5 imm=7
the PC at time 3 = 3
value of cell 3 at time 3 = 3

then value of cell 3 at time 4 = 3

Byte 4 Stays the Same 3

if the following are true:

instruction #3 is addi dst=5 src=5 imm=7
the PC at time 3 = 3
value of cell 4 at time 3 = 0

then value of cell 4 at time 4 = 0

Addi Insn 4

if the following are true:

instruction #4 is addi dst=4 src=4 imm=1
the PC at time 4 = 4
value of cell 4 at time 4 = 0

then value of cell 4 at time 5 = 1

Pc 4

if the following are true:

instruction #4 is addi dst=4 src=4 imm=1
the PC at time 4 = 4

then the PC at time 5 = 5

Byte 3 Stays the Same 4

if the following are true:

instruction #4 is addi dst=4 src=4 imm=1
the PC at time 4 = 4
value of cell 3 at time 4 = 3

then value of cell 3 at time 5 = 3

Byte 5 Stays the Same 4

if the following are true:

instruction #4 is addi dst=4 src=4 imm=1
the PC at time 4 = 4
value of cell 5 at time 4 = 7

then value of cell 5 at time 5 = 7

Beq No Branch 5

if the following are true:

instruction #5 is beq left=3 right=4 imm=1
the PC at time 5 = 5
value of cell 3 at time 5 = 3
value of cell 4 at time 5 = 1

then the PC at time 6 = 6

Byte 3 Stays the Same 5

if the following are true:

instruction #5 is beq left=3 right=4 imm=1
the PC at time 5 = 5
value of cell 3 at time 5 = 3

then value of cell 3 at time 6 = 3

Byte 4 Stays the Same 5

if the following are true:

instruction #5 is beq left=3 right=4 imm=1
the PC at time 5 = 5
value of cell 4 at time 5 = 1

then value of cell 4 at time 6 = 1

Byte 5 Stays the Same 5

if the following are true:

instruction #5 is beq left=3 right=4 imm=1
the PC at time 5 = 5
value of cell 5 at time 5 = 7

then value of cell 5 at time 6 = 7

Jump Help 6

if the following are true:

instruction #6 is jump imm=3
the PC at time 6 = 6

then the PC at time 7 = 3

Byte 3 Stays the Same 6

if the following are true:

instruction #6 is jump imm=3
the PC at time 6 = 6
value of cell 3 at time 6 = 3

then value of cell 3 at time 7 = 3

Byte 4 Stays the Same 6

if the following are true:

instruction #6 is jump imm=3
the PC at time 6 = 6
value of cell 4 at time 6 = 1

then value of cell 4 at time 7 = 1

Byte 5 Stays the Same 6

if the following are true:

instruction #6 is jump imm=3
the PC at time 6 = 6
value of cell 5 at time 6 = 7

then value of cell 5 at time 7 = 7

Addi Insn 7

if the following are true:

instruction #3 is addi dst=5 src=5 imm=7
the PC at time 7 = 3
value of cell 5 at time 7 = 7

then value of cell 5 at time 8 = 14

Pc 7

if the following are true:

instruction #3 is addi dst=5 src=5 imm=7
the PC at time 7 = 3

then the PC at time 8 = 4

Byte 3 Stays the Same 7

if the following are true:

instruction #3 is addi dst=5 src=5 imm=7
the PC at time 7 = 3
value of cell 3 at time 7 = 3

then value of cell 3 at time 8 = 3

Byte 4 Stays the Same 7

if the following are true:

instruction #3 is addi dst=5 src=5 imm=7
the PC at time 7 = 3
value of cell 4 at time 7 = 1

then value of cell 4 at time 8 = 1

Addi Insn 8

if the following are true:

instruction #4 is addi dst=4 src=4 imm=1
the PC at time 8 = 4
value of cell 4 at time 8 = 1

then value of cell 4 at time 9 = 2

Pc 8

if the following are true:

instruction #4 is addi dst=4 src=4 imm=1
the PC at time 8 = 4

then the PC at time 9 = 5

Byte 3 Stays the Same 8

if the following are true:

instruction #4 is addi dst=4 src=4 imm=1
the PC at time 8 = 4
value of cell 3 at time 8 = 3

then value of cell 3 at time 9 = 3

Byte 5 Stays the Same 8

if the following are true:

instruction #4 is addi dst=4 src=4 imm=1
the PC at time 8 = 4
value of cell 5 at time 8 = 14

then value of cell 5 at time 9 = 14

Beq No Branch 9

if the following are true:

instruction #5 is beq left=3 right=4 imm=1
the PC at time 9 = 5
value of cell 3 at time 9 = 3
value of cell 4 at time 9 = 2

then the PC at time 10 = 6

Byte 3 Stays the Same 9

if the following are true:

instruction #5 is beq left=3 right=4 imm=1
the PC at time 9 = 5
value of cell 3 at time 9 = 3

then value of cell 3 at time 10 = 3

Byte 4 Stays the Same 9

if the following are true:

instruction #5 is beq left=3 right=4 imm=1
the PC at time 9 = 5
value of cell 4 at time 9 = 2

then value of cell 4 at time 10 = 2

Byte 5 Stays the Same 9

if the following are true:

instruction #5 is beq left=3 right=4 imm=1
the PC at time 9 = 5
value of cell 5 at time 9 = 14

then value of cell 5 at time 10 = 14

Jump Help 10

if the following are true:

instruction #6 is jump imm=3
the PC at time 10 = 6

then the PC at time 11 = 3

Byte 3 Stays the Same 10

if the following are true:

instruction #6 is jump imm=3
the PC at time 10 = 6
value of cell 3 at time 10 = 3

then value of cell 3 at time 11 = 3

Byte 4 Stays the Same 10

if the following are true:

instruction #6 is jump imm=3
the PC at time 10 = 6
value of cell 4 at time 10 = 2

then value of cell 4 at time 11 = 2

Byte 5 Stays the Same 10

if the following are true:

instruction #6 is jump imm=3
the PC at time 10 = 6
value of cell 5 at time 10 = 14

then value of cell 5 at time 11 = 14

Addi Insn 11

if the following are true:

instruction #3 is addi dst=5 src=5 imm=7
the PC at time 11 = 3
value of cell 5 at time 11 = 14

then value of cell 5 at time 12 = 21

Pc 11

if the following are true:

instruction #3 is addi dst=5 src=5 imm=7
the PC at time 11 = 3

then the PC at time 12 = 4

Byte 3 Stays the Same 11

if the following are true:

instruction #3 is addi dst=5 src=5 imm=7
the PC at time 11 = 3
value of cell 3 at time 11 = 3

then value of cell 3 at time 12 = 3

Byte 4 Stays the Same 11

if the following are true:

instruction #3 is addi dst=5 src=5 imm=7
the PC at time 11 = 3
value of cell 4 at time 11 = 2

then value of cell 4 at time 12 = 2

Addi Insn 12

if the following are true:

instruction #4 is addi dst=4 src=4 imm=1
the PC at time 12 = 4
value of cell 4 at time 12 = 2

then value of cell 4 at time 13 = 3

Pc 12

if the following are true:

instruction #4 is addi dst=4 src=4 imm=1
the PC at time 12 = 4

then the PC at time 13 = 5

Byte 3 Stays the Same 12

if the following are true:

instruction #4 is addi dst=4 src=4 imm=1
the PC at time 12 = 4
value of cell 3 at time 12 = 3

then value of cell 3 at time 13 = 3

Byte 5 Stays the Same 12

if the following are true:

instruction #4 is addi dst=4 src=4 imm=1
the PC at time 12 = 4
value of cell 5 at time 12 = 21

then value of cell 5 at time 13 = 21

Beq Branch

if the following are true:

instruction #5 is beq left=3 right=4 imm=1
the PC at time 13 = 5
value of cell 3 at time 13 = 3
value of cell 4 at time 13 = 3

then the PC at time 14 = 7

Byte 3 Stays the Same 13

if the following are true:

instruction #5 is beq left=3 right=4 imm=1
the PC at time 13 = 5
value of cell 3 at time 13 = 3

then value of cell 3 at time 14 = 3

Byte 4 Stays the Same 13

if the following are true:

instruction #5 is beq left=3 right=4 imm=1
the PC at time 13 = 5
value of cell 4 at time 13 = 3

then value of cell 4 at time 14 = 3

Byte 5 Stays the Same 13

if the following are true:

instruction #5 is beq left=3 right=4 imm=1
the PC at time 13 = 5
value of cell 5 at time 13 = 21

then value of cell 5 at time 14 = 21

Fibonacci

if the following are true:

the PC at time 0 = 0
instruction #0 is addi dst=1 src=0 imm=0
instruction #1 is addi dst=2 src=0 imm=1
instruction #2 is addi dst=4 src=0 imm=0
instruction #3 is addi dst=5 src=0 imm=4
instruction #4 is add dst=3 src1=1 src2=2
instruction #5 is addi dst=1 src=2 imm=0
instruction #6 is addi dst=2 src=3 imm=0
instruction #7 is addi dst=4 src=4 imm=1
instruction #8 is beq left=4 right=5 imm=1
instruction #9 is jump imm=(-6)

then value of cell 3 at time 25 = 5

ADDI Instruction Example

if the following are true:

instruction #0 is addi dst=2 src=1 imm=5
the PC at time 0 = 0
value of cell 1 at time 0 = 4

then value of cell 2 at time 1 = 9

ADDI Instruction Example 2

if the following are true:

instruction #0 is addi dst=2 src=src imm=imm
the PC at time 0 = 0
value of cell 1 at time 0 = 4

then value of cell 1 at time 1 = 4

Program Counter Example

if the following are true:

instruction #1 is addi dst=dst src=src imm=imm
the PC at time 1 = 1

then the PC at time 2 = 2

ADD Instruction Example

if the following are true:

instruction #0 is add dst=3 src1=1 src2=2
the PC at time 0 = 0
value of cell 1 at time 0 = 2
value of cell 2 at time 0 = 6

then value of cell 3 at time 1 = 8

ADD Instruction Example 2

if the following are true:

instruction #0 is add dst=2 src1=src1 src2=src2
the PC at time 0 = 0
value of cell 1 at time 0 = 4

then value of cell 1 at time 1 = 4

Program Counter Example

if the following are true:

instruction #1 is add dst=dst src1=src1 src2=src2
the PC at time 1 = 1

then the PC at time 2 = 2

JUMP Instruction Example

if the following are true:

instruction #0 is jump imm=2
the PC at time 0 = 0

then the PC at time 1 = 2

JUMP Instruction Example 2

if the following are true:

instruction #0 is jump imm=jump_to
the PC at time 0 = 0

then value of cell x at time 1 = value of cell x at time 0

JUMPR Instruction Example

if the following are true:

instruction #0 is jumpr addr=1
the PC at time 0 = 0
value of cell 1 at time 0 = 3

then the PC at time 1 = 3

JUMPR Instruction Example 2

if the following are true:

instruction #0 is jumpr addr=1
the PC at time 0 = 0

then value of cell x at time 1 = value of cell x at time 0

JAL Instruction Example

if the following are true:

instruction #5 is a JAL instruction with jump to: 1
the PC at time 2 = 5

then the PC at time 3 = 1

JAL Instruction Store Example

if the following are true:

instruction #5 is a JAL instruction with jump to: 1
the PC at time 2 = 5

then value of cell 2 at time 3 = 6

JAL Instruction Example 3

if the following are true:

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

then value of cell x at time 3 = value of cell x at time 2

BEQ Instruction Example

if the following are true:

instruction #0 is beq left=1 right=2 imm=2
the PC at time 0 = 0
value of cell 1 at time 0 = 2
value of cell 2 at time 0 = 2

then the PC at time 1 = 3

BEQ Instruction Example 2

if the following are true:

instruction #0 is beq left=1 right=2 imm=2
the PC at time 0 = 0
value of cell 1 at time 0 = 1
value of cell 2 at time 0 = 2

then the PC at time 1 = 1

BEQ Instruction Example 3

if the following are true:

instruction #0 is beq left=left right=right imm=imm
the PC at time 0 = 0

then value of cell x at time 1 = value of cell x at time 0

STORE Instruction Example

if the following are true:

instruction #0 is store src=5 addr=1 imm=0
the PC at time 0 = 0
value of cell 1 at time 0 = 3
value of cell 5 at time 0 = 9

then value of cell 3 at time 1 = 9

Proof: STORE Instruction Example

if the following are true:

instruction #0 is store src=5 addr=1 imm=1
the PC at time 0 = 0
value of cell 1 at time 0 = 3
value of cell 5 at time 0 = 9

then value of cell 4 at time 1 = 9

STORE Instruction Example 3

if the following are true:

instruction #0 is store src=5 addr=1 imm=1
the PC at time 0 = 0
value of cell 1 at time 0 = 3

then value of cell 2 at time 1 = value of cell 2 at time 0

STORE Instruction Example 4

if the following are true:

instruction #0 is store src=5 addr=1 imm=1
the PC at time 0 = 0

then the PC at time 1 = 1

LOAD Instruction Example 2

if the following are true:

instruction #0 is load dst=5 addr=1 imm=0
the PC at time 0 = 0
value of cell 1 at time 0 = 3
value of cell 3 at time 0 = 9

then value of cell 5 at time 1 = 9

LOAD Instruction Example

if the following are true:

instruction #0 is load dst=5 addr=1 imm=1
the PC at time 0 = 0
value of cell 1 at time 0 = 3
value of cell 4 at time 0 = 7

then value of cell 5 at time 1 = 7

LOAD Instruction Example 3

if the following are true:

instruction #0 is load dst=5 addr=1 imm=1
the PC at time 0 = 0

then value of cell 2 at time 1 = value of cell 2 at time 0

LOAD Instruction Example 4

if the following are true:

instruction #0 is load dst=5 addr=1 imm=1
the PC at time 0 = 0

then the PC at time 1 = 1

Addi Zero Insn 0

if the following are true:

instruction #0 is addi dst=1 src=0 imm=0
the PC at time 0 = 0

then value of cell 1 at time 1 = 0

Pc 0

if the following are true:

instruction #0 is addi dst=1 src=0 imm=0
the PC at time 0 = 0

then the PC at time 1 = 1

Addi Zero Insn 1

if the following are true:

instruction #1 is addi dst=2 src=0 imm=1
the PC at time 1 = 1

then value of cell 2 at time 2 = 1

Pc 1

if the following are true:

instruction #1 is addi dst=2 src=0 imm=1
the PC at time 1 = 1

then the PC at time 2 = 2

Byte 1 Stays the Same 1

if the following are true:

instruction #1 is addi dst=2 src=0 imm=1
the PC at time 1 = 1
value of cell 1 at time 1 = 0

then value of cell 1 at time 2 = 0

Addi Zero Insn 2

if the following are true:

instruction #2 is addi dst=4 src=0 imm=0
the PC at time 2 = 2

then value of cell 4 at time 3 = 0

Pc 2

if the following are true:

instruction #2 is addi dst=4 src=0 imm=0
the PC at time 2 = 2

then the PC at time 3 = 3

Byte 1 Stays the Same 2

if the following are true:

instruction #2 is addi dst=4 src=0 imm=0
the PC at time 2 = 2
value of cell 1 at time 2 = 0

then value of cell 1 at time 3 = 0

Byte 2 Stays the Same 2

if the following are true:

instruction #2 is addi dst=4 src=0 imm=0
the PC at time 2 = 2
value of cell 2 at time 2 = 1

then value of cell 2 at time 3 = 1

Addi Zero Insn 3

if the following are true:

instruction #3 is addi dst=5 src=0 imm=4
the PC at time 3 = 3

then value of cell 5 at time 4 = 4

Pc 3

if the following are true:

instruction #3 is addi dst=5 src=0 imm=4
the PC at time 3 = 3

then the PC at time 4 = 4

Byte 1 Stays the Same 3

if the following are true:

instruction #3 is addi dst=5 src=0 imm=4
the PC at time 3 = 3
value of cell 1 at time 3 = 0

then value of cell 1 at time 4 = 0

Byte 2 Stays the Same 3

if the following are true:

instruction #3 is addi dst=5 src=0 imm=4
the PC at time 3 = 3
value of cell 2 at time 3 = 1

then value of cell 2 at time 4 = 1

Byte 4 Stays the Same 3

if the following are true:

instruction #3 is addi dst=5 src=0 imm=4
the PC at time 3 = 3
value of cell 4 at time 3 = 0

then value of cell 4 at time 4 = 0

Add Insn 4

if the following are true:

the PC at time 4 = 4
instruction #4 is add dst=3 src1=1 src2=2

then value of cell 3 at time 5 = (value of cell 1 at time 4) + (value of cell 2 at time 4)

Substitute Add 4

if the following are true:

value of cell 3 at time 5 = (value of cell 1 at time 4) + (value of cell 2 at time 4)
value of cell 1 at time 4 = 0
value of cell 2 at time 4 = 1

then value of cell 3 at time 5 = 1

Pc 4

if the following are true:

instruction #4 is add dst=3 src1=1 src2=2
the PC at time 4 = 4

then the PC at time 5 = 5

Byte 1 Stays the Same 4

if the following are true:

instruction #4 is add dst=3 src1=1 src2=2
the PC at time 4 = 4
value of cell 1 at time 4 = 0

then value of cell 1 at time 5 = 0

Byte 2 Stays the Same 4

if the following are true:

instruction #4 is add dst=3 src1=1 src2=2
the PC at time 4 = 4
value of cell 2 at time 4 = 1

then value of cell 2 at time 5 = 1

Byte 4 Stays the Same 4

if the following are true:

instruction #4 is add dst=3 src1=1 src2=2
the PC at time 4 = 4
value of cell 4 at time 4 = 0

then value of cell 4 at time 5 = 0

Byte 5 Stays the Same 4

if the following are true:

instruction #4 is add dst=3 src1=1 src2=2
the PC at time 4 = 4
value of cell 5 at time 4 = 4

then value of cell 5 at time 5 = 4

Addi Insn 5

if the following are true:

instruction #5 is addi dst=1 src=2 imm=0
the PC at time 5 = 5
value of cell 2 at time 5 = 1

then value of cell 1 at time 6 = 1

Pc 5

if the following are true:

instruction #5 is addi dst=1 src=2 imm=0
the PC at time 5 = 5

then the PC at time 6 = 6

Byte 2 Stays the Same 5

if the following are true:

instruction #5 is addi dst=1 src=2 imm=0
the PC at time 5 = 5
value of cell 2 at time 5 = 1

then value of cell 2 at time 6 = 1

Byte 4 Stays the Same 5

if the following are true:

instruction #5 is addi dst=1 src=2 imm=0
the PC at time 5 = 5
value of cell 4 at time 5 = 0

then value of cell 4 at time 6 = 0

Byte 5 Stays the Same 5

if the following are true:

instruction #5 is addi dst=1 src=2 imm=0
the PC at time 5 = 5
value of cell 5 at time 5 = 4

then value of cell 5 at time 6 = 4

Byte 3 Stays the Same 5

if the following are true:

instruction #5 is addi dst=1 src=2 imm=0
the PC at time 5 = 5
value of cell 3 at time 5 = 1

then value of cell 3 at time 6 = 1

Pages: 5 6 7 ... 16