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

Pc 22

if the following are true:

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

then the PC at time 23 = 5

Byte 1 Stays the Same 22

if the following are true:

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

then value of cell 1 at time 23 = 2

Byte 2 Stays the Same 22

if the following are true:

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

then value of cell 2 at time 23 = 3

Byte 4 Stays the Same 22

if the following are true:

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

then value of cell 4 at time 23 = 3

Byte 5 Stays the Same 22

if the following are true:

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

then value of cell 5 at time 23 = 4

Addi Insn 23

if the following are true:

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

then value of cell 1 at time 24 = 3

Pc 23

if the following are true:

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

then the PC at time 24 = 6

Byte 2 Stays the Same 23

if the following are true:

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

then value of cell 2 at time 24 = 3

Byte 4 Stays the Same 23

if the following are true:

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

then value of cell 4 at time 24 = 3

Byte 5 Stays the Same 23

if the following are true:

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

then value of cell 5 at time 24 = 4

Byte 3 Stays the Same 23

if the following are true:

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

then value of cell 3 at time 24 = 5

Addi Insn 24

if the following are true:

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

then value of cell 2 at time 25 = 5

Pc 24

if the following are true:

instruction #6 is addi dst=2 src=3 imm=0
the PC at time 24 = 6

then the PC at time 25 = 7

Byte 1 Stays the Same 24

if the following are true:

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

then value of cell 1 at time 25 = 3

Byte 4 Stays the Same 24

if the following are true:

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

then value of cell 4 at time 25 = 3

Byte 5 Stays the Same 24

if the following are true:

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

then value of cell 5 at time 25 = 4

Byte 3 Stays the Same 24

if the following are true:

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

then value of cell 3 at time 25 = 5

Proof: Multiplication Example

if the following are true:

the PC at time 0 = 0
instruction #0 is addi dst=3 src=0 imm=3
instruction #1 is addi dst=4 src=0 imm=0
instruction #2 is addi dst=5 src=0 imm=0
instruction #3 is addi dst=5 src=5 imm=7
instruction #4 is addi dst=4 src=4 imm=1
instruction #5 is beq left=3 right=4 imm=1
instruction #6 is jump imm=3

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=3
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=4
instruction #10 is addi dst=1 src=0 imm=0

then value of cell 3 at time 22 = 3

Copy Example

if the following are true:

the PC at time 0 = 0
instruction #0 is addi dst=7 src=3 imm=0
instruction #1 is addi dst=8 src=4 imm=0
instruction #2 is addi dst=9 src=5 imm=0
value of cell 3 at time 0 = 13
value of cell 4 at time 0 = 11
value of cell 5 at time 0 = 20

then value of cell 8 at time 3 = 11

Addi Insn 0

if the following are true:

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

then value of cell 7 at time 1 = 13

Pc 0

if the following are true:

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

then the PC at time 1 = 1

Byte 3 Stays the Same 0

if the following are true:

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

then value of cell 3 at time 1 = 13

Byte 4 Stays the Same 0

if the following are true:

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

then value of cell 4 at time 1 = 11

Byte 5 Stays the Same 0

if the following are true:

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

then value of cell 5 at time 1 = 20

Addi Insn 1

if the following are true:

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

then value of cell 8 at time 2 = 11

Pc 1

if the following are true:

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

then the PC at time 2 = 2

Byte 3 Stays the Same 1

if the following are true:

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

then value of cell 3 at time 2 = 13

Byte 4 Stays the Same 1

if the following are true:

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

then value of cell 4 at time 2 = 11

Byte 5 Stays the Same 1

if the following are true:

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

then value of cell 5 at time 2 = 20

Byte 7 Stays the Same 1

if the following are true:

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

then value of cell 7 at time 2 = 13

Addi Insn 2

if the following are true:

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

then value of cell 9 at time 3 = 20

Pc 2

if the following are true:

instruction #2 is addi dst=9 src=5 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=9 src=5 imm=0
the PC at time 2 = 2
value of cell 3 at time 2 = 13

then value of cell 3 at time 3 = 13

Byte 4 Stays the Same 2

if the following are true:

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

then value of cell 4 at time 3 = 11

Byte 5 Stays the Same 2

if the following are true:

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

then value of cell 5 at time 3 = 20

Byte 7 Stays the Same 2

if the following are true:

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

then value of cell 7 at time 3 = 13

Byte 8 Stays the Same 2

if the following are true:

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

then value of cell 8 at time 3 = 11

Copy By Load Example

if the following are true:

the PC at time 0 = 0
instruction #0 is load dst=7 addr=6 imm=0
instruction #1 is load dst=8 addr=6 imm=1
instruction #2 is load dst=9 addr=6 imm=2
value of cell 3 at time 0 = 13
value of cell 4 at time 0 = 11
value of cell 5 at time 0 = 20
value of cell 6 at time 0 = 3

then value of cell 8 at time 3 = 11

Store 0

if the following are true:

instruction #0 is store src=3 addr=6 imm=0
the PC at time 0 = 0
value of cell 6 at time 0 = 7
value of cell 3 at time 0 = 13

then value of cell 7 at time 1 = 13

Pc 0

if the following are true:

instruction #0 is store src=3 addr=6 imm=0
the PC at time 0 = 0

then the PC at time 1 = 1

Byte 3 Stays the Same Store 0

if the following are true:

instruction #0 is store src=3 addr=6 imm=0
the PC at time 0 = 0
value of cell 3 at time 0 = 13
value of cell 6 at time 0 = 7

then value of cell 3 at time 1 = 13

Byte 4 Stays the Same Store 0

if the following are true:

instruction #0 is store src=3 addr=6 imm=0
the PC at time 0 = 0
value of cell 4 at time 0 = 11
value of cell 6 at time 0 = 7

then value of cell 4 at time 1 = 11

Byte 5 Stays the Same Store 0

if the following are true:

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

then value of cell 5 at time 1 = 20

Byte 6 Stays the Same Store 0

if the following are true:

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

then value of cell 6 at time 1 = 7

Store 1

if the following are true:

instruction #1 is store src=4 addr=6 imm=1
the PC at time 1 = 1
value of cell 6 at time 1 = 7
value of cell 4 at time 1 = 11

then value of cell 8 at time 2 = 11

Pc 1

if the following are true:

instruction #1 is store src=4 addr=6 imm=1
the PC at time 1 = 1

then the PC at time 2 = 2

Byte 3 Stays the Same Store 1

if the following are true:

instruction #1 is store src=4 addr=6 imm=1
the PC at time 1 = 1
value of cell 3 at time 1 = 13
value of cell 6 at time 1 = 7

then value of cell 3 at time 2 = 13

Byte 4 Stays the Same Store 1

if the following are true:

instruction #1 is store src=4 addr=6 imm=1
the PC at time 1 = 1
value of cell 4 at time 1 = 11
value of cell 6 at time 1 = 7

then value of cell 4 at time 2 = 11

Byte 5 Stays the Same Store 1

if the following are true:

instruction #1 is store src=4 addr=6 imm=1
the PC at time 1 = 1
value of cell 5 at time 1 = 20
value of cell 6 at time 1 = 7

then value of cell 5 at time 2 = 20

Byte 6 Stays the Same Store 1

if the following are true:

instruction #1 is store src=4 addr=6 imm=1
the PC at time 1 = 1
value of cell 6 at time 1 = 7
value of cell 6 at time 1 = 7

then value of cell 6 at time 2 = 7

Byte 7 Stays the Same Store 1

if the following are true:

instruction #1 is store src=4 addr=6 imm=1
the PC at time 1 = 1
value of cell 7 at time 1 = 13
value of cell 6 at time 1 = 7

then value of cell 7 at time 2 = 13

Store 2

if the following are true:

instruction #2 is store src=5 addr=6 imm=2
the PC at time 2 = 2
value of cell 6 at time 2 = 7
value of cell 5 at time 2 = 20

then value of cell 9 at time 3 = 20

Pc 2

if the following are true:

instruction #2 is store src=5 addr=6 imm=2
the PC at time 2 = 2

then the PC at time 3 = 3

Byte 3 Stays the Same Store 2

if the following are true:

instruction #2 is store src=5 addr=6 imm=2
the PC at time 2 = 2
value of cell 3 at time 2 = 13
value of cell 6 at time 2 = 7

then value of cell 3 at time 3 = 13

Byte 4 Stays the Same Store 2

if the following are true:

instruction #2 is store src=5 addr=6 imm=2
the PC at time 2 = 2
value of cell 4 at time 2 = 11
value of cell 6 at time 2 = 7

then value of cell 4 at time 3 = 11

Byte 5 Stays the Same Store 2

if the following are true:

instruction #2 is store src=5 addr=6 imm=2
the PC at time 2 = 2
value of cell 5 at time 2 = 20
value of cell 6 at time 2 = 7

then value of cell 5 at time 3 = 20

Byte 6 Stays the Same Store 2

if the following are true:

instruction #2 is store src=5 addr=6 imm=2
the PC at time 2 = 2
value of cell 6 at time 2 = 7
value of cell 6 at time 2 = 7

then value of cell 6 at time 3 = 7

Byte 7 Stays the Same Store 2

if the following are true:

instruction #2 is store src=5 addr=6 imm=2
the PC at time 2 = 2
value of cell 7 at time 2 = 13
value of cell 6 at time 2 = 7

then value of cell 7 at time 3 = 13

Byte 8 Stays the Same Store 2

if the following are true:

instruction #2 is store src=5 addr=6 imm=2
the PC at time 2 = 2
value of cell 8 at time 2 = 11
value of cell 6 at time 2 = 7

then value of cell 8 at time 3 = 11

Flexible Copy Example

if the following are true:

the PC at time 0 = 0
instruction #0 is load dst=7 addr=5 imm=0
instruction #1 is store src=7 addr=6 imm=0
instruction #2 is addi dst=5 src=5 imm=1
instruction #3 is addi dst=6 src=6 imm=1
instruction #4 is addi dst=4 src=4 imm=1
instruction #5 is beq left=3 right=4 imm=1
instruction #6 is jump imm=0
value of cell 3 at time 0 = 3
value of cell 4 at time 0 = 0
value of cell 5 at time 0 = 8
value of cell 6 at time 0 = 12
value of cell 8 at time 0 = 24
value of cell 9 at time 0 = 31
value of cell 10 at time 0 = 45

then value of cell 14 at time 20 = 45

Copy By Store Example

if the following are true:

the PC at time 0 = 0
instruction #0 is store src=3 addr=6 imm=0
instruction #1 is store src=4 addr=6 imm=1
instruction #2 is store src=5 addr=6 imm=2
value of cell 3 at time 0 = 13
value of cell 4 at time 0 = 11
value of cell 5 at time 0 = 20
value of cell 6 at time 0 = 7

then value of cell 8 at time 3 = 11

Load 0

if the following are true:

instruction #0 is load dst=7 addr=6 imm=0
the PC at time 0 = 0
value of cell 6 at time 0 = 3
value of cell 3 at time 0 = 13

then value of cell 7 at time 1 = 13

Pc 0

if the following are true:

instruction #0 is load dst=7 addr=6 imm=0
the PC at time 0 = 0

then the PC at time 1 = 1

Byte 3 Stays the Same 0

if the following are true:

instruction #0 is load dst=7 addr=6 imm=0
the PC at time 0 = 0
value of cell 3 at time 0 = 13

then value of cell 3 at time 1 = 13

Byte 4 Stays the Same 0

if the following are true:

instruction #0 is load dst=7 addr=6 imm=0
the PC at time 0 = 0
value of cell 4 at time 0 = 11

then value of cell 4 at time 1 = 11

Byte 5 Stays the Same 0

if the following are true:

instruction #0 is load dst=7 addr=6 imm=0
the PC at time 0 = 0
value of cell 5 at time 0 = 20

then value of cell 5 at time 1 = 20

Byte 6 Stays the Same 0

if the following are true:

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

then value of cell 6 at time 1 = 3

Load 1

if the following are true:

instruction #1 is load dst=8 addr=6 imm=1
the PC at time 1 = 1
value of cell 6 at time 1 = 3
value of cell 4 at time 1 = 11

then value of cell 8 at time 2 = 11

Pc 1

if the following are true:

instruction #1 is load dst=8 addr=6 imm=1
the PC at time 1 = 1

then the PC at time 2 = 2

Byte 3 Stays the Same 1

if the following are true:

instruction #1 is load dst=8 addr=6 imm=1
the PC at time 1 = 1
value of cell 3 at time 1 = 13

then value of cell 3 at time 2 = 13

Byte 4 Stays the Same 1

if the following are true:

instruction #1 is load dst=8 addr=6 imm=1
the PC at time 1 = 1
value of cell 4 at time 1 = 11

then value of cell 4 at time 2 = 11

Byte 5 Stays the Same 1

if the following are true:

instruction #1 is load dst=8 addr=6 imm=1
the PC at time 1 = 1
value of cell 5 at time 1 = 20

then value of cell 5 at time 2 = 20

Byte 6 Stays the Same 1

if the following are true:

instruction #1 is load dst=8 addr=6 imm=1
the PC at time 1 = 1
value of cell 6 at time 1 = 3

then value of cell 6 at time 2 = 3

Byte 7 Stays the Same 1

if the following are true:

instruction #1 is load dst=8 addr=6 imm=1
the PC at time 1 = 1
value of cell 7 at time 1 = 13

then value of cell 7 at time 2 = 13

Load 2

if the following are true:

instruction #2 is load dst=9 addr=6 imm=2
the PC at time 2 = 2
value of cell 6 at time 2 = 3
value of cell 5 at time 2 = 20

then value of cell 9 at time 3 = 20

Pc 2

if the following are true:

instruction #2 is load dst=9 addr=6 imm=2
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 load dst=9 addr=6 imm=2
the PC at time 2 = 2
value of cell 3 at time 2 = 13

then value of cell 3 at time 3 = 13

Byte 4 Stays the Same 2

if the following are true:

instruction #2 is load dst=9 addr=6 imm=2
the PC at time 2 = 2
value of cell 4 at time 2 = 11

then value of cell 4 at time 3 = 11

Byte 5 Stays the Same 2

if the following are true:

instruction #2 is load dst=9 addr=6 imm=2
the PC at time 2 = 2
value of cell 5 at time 2 = 20

then value of cell 5 at time 3 = 20

Byte 6 Stays the Same 2

if the following are true:

instruction #2 is load dst=9 addr=6 imm=2
the PC at time 2 = 2
value of cell 6 at time 2 = 3

then value of cell 6 at time 3 = 3

Byte 7 Stays the Same 2

if the following are true:

instruction #2 is load dst=9 addr=6 imm=2
the PC at time 2 = 2
value of cell 7 at time 2 = 13

then value of cell 7 at time 3 = 13

Byte 8 Stays the Same 2

if the following are true:

instruction #2 is load dst=9 addr=6 imm=2
the PC at time 2 = 2
value of cell 8 at time 2 = 11

then value of cell 8 at time 3 = 11

Load 0

if the following are true:

instruction #0 is load dst=7 addr=5 imm=0
the PC at time 0 = 0
value of cell 5 at time 0 = 8
value of cell 8 at time 0 = 24

then value of cell 7 at time 1 = 24

Pc 0

if the following are true:

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

then the PC at time 1 = 1

Byte 3 Stays the Same 0

if the following are true:

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

then value of cell 3 at time 1 = 3

Byte 4 Stays the Same 0

if the following are true:

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

then value of cell 4 at time 1 = 0

Byte 5 Stays the Same 0

if the following are true:

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

then value of cell 5 at time 1 = 8

Byte 6 Stays the Same 0

if the following are true:

instruction #0 is load dst=7 addr=5 imm=0
the PC at time 0 = 0
value of cell 6 at time 0 = 12

then value of cell 6 at time 1 = 12

Byte 8 Stays the Same 0

if the following are true:

instruction #0 is load dst=7 addr=5 imm=0
the PC at time 0 = 0
value of cell 8 at time 0 = 24

then value of cell 8 at time 1 = 24

Byte 9 Stays the Same 0

if the following are true:

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

then value of cell 9 at time 1 = 31

Byte 10 Stays the Same 0

if the following are true:

instruction #0 is load dst=7 addr=5 imm=0
the PC at time 0 = 0
value of cell 10 at time 0 = 45

then value of cell 10 at time 1 = 45

Store 1

if the following are true:

instruction #1 is store src=7 addr=6 imm=0
the PC at time 1 = 1
value of cell 6 at time 1 = 12
value of cell 7 at time 1 = 24

then value of cell 12 at time 2 = 24

Pc 1

if the following are true:

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

then the PC at time 2 = 2

Byte 3 Stays the Same Store 1

if the following are true:

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

then value of cell 3 at time 2 = 3

Byte 4 Stays the Same Store 1

if the following are true:

instruction #1 is store src=7 addr=6 imm=0
the PC at time 1 = 1
value of cell 4 at time 1 = 0
value of cell 6 at time 1 = 12

then value of cell 4 at time 2 = 0

Byte 5 Stays the Same Store 1

if the following are true:

instruction #1 is store src=7 addr=6 imm=0
the PC at time 1 = 1
value of cell 5 at time 1 = 8
value of cell 6 at time 1 = 12

then value of cell 5 at time 2 = 8

Byte 6 Stays the Same Store 1

if the following are true:

instruction #1 is store src=7 addr=6 imm=0
the PC at time 1 = 1
value of cell 6 at time 1 = 12
value of cell 6 at time 1 = 12

then value of cell 6 at time 2 = 12

Byte 8 Stays the Same Store 1

if the following are true:

instruction #1 is store src=7 addr=6 imm=0
the PC at time 1 = 1
value of cell 8 at time 1 = 24
value of cell 6 at time 1 = 12

then value of cell 8 at time 2 = 24

Byte 9 Stays the Same Store 1

if the following are true:

instruction #1 is store src=7 addr=6 imm=0
the PC at time 1 = 1
value of cell 9 at time 1 = 31
value of cell 6 at time 1 = 12

then value of cell 9 at time 2 = 31

Pages: 7 8 9 ... 16