Proofs

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

then the PC at time 1 = 1

• instruction #1 is jump imm=8
• the PC at time 1 = 1

then the PC at time 2 = 8

• instruction #1 is jump imm=8
• the PC at time 1 = 1
• value of cell 1 at time 1 = 128

then value of cell 1 at time 2 = 128

• instruction #8 is addi dst=3 src=0 imm=2
• the PC at time 2 = 8

then value of cell 3 at time 3 = 2

• instruction #8 is addi dst=3 src=0 imm=2
• the PC at time 2 = 8

then the PC at time 3 = 9

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

then value of cell 1 at time 3 = 128

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 9
• the PC at time 3 = 9
• value of cell 1 at time 3 = 128

then value of cell 1 at time 4 = 127

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 9
• the PC at time 3 = 9

then the PC at time 4 = 10

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 9
• the PC at time 3 = 9
• value of cell 3 at time 3 = 2

then value of cell 3 at time 4 = 2

• instruction #10 is store src=3 addr=1 imm=0
• the PC at time 4 = 10
• value of cell 1 at time 4 = 127
• value of cell 3 at time 4 = 2

then value of cell 127 at time 5 = 2

• instruction #10 is store src=3 addr=1 imm=0
• the PC at time 4 = 10

then the PC at time 5 = 11

• instruction #10 is store src=3 addr=1 imm=0
• the PC at time 4 = 10
• value of cell 1 at time 4 = 127
• value of cell 1 at time 4 = 127

then value of cell 1 at time 5 = 127

• instruction #10 is store src=3 addr=1 imm=0
• the PC at time 4 = 10
• value of cell 3 at time 4 = 2
• value of cell 1 at time 4 = 127

then value of cell 3 at time 5 = 2

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

then value of cell 3 at time 6 = 3

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

then the PC at time 6 = 12

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

then value of cell 1 at time 6 = 127

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

then value of cell 127 at time 6 = 2

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 12
• the PC at time 6 = 12
• value of cell 1 at time 6 = 127

then value of cell 1 at time 7 = 126

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 12
• the PC at time 6 = 12

then the PC at time 7 = 13

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 12
• the PC at time 6 = 12
• value of cell 3 at time 6 = 3

then value of cell 3 at time 7 = 3

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 12
• the PC at time 6 = 12
• value of cell 127 at time 6 = 2

then value of cell 127 at time 7 = 2

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

then value of cell 126 at time 8 = 3

• instruction #13 is store src=3 addr=1 imm=0
• the PC at time 7 = 13

then the PC at time 8 = 14

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

then value of cell 1 at time 8 = 126

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

then value of cell 3 at time 8 = 3

• instruction #13 is store src=3 addr=1 imm=0
• the PC at time 7 = 13
• value of cell 127 at time 7 = 2
• value of cell 1 at time 7 = 126

then value of cell 127 at time 8 = 2

• instruction #14 is load dst=3 addr=1 imm=1
• the PC at time 8 = 14
• value of cell 1 at time 8 = 126
• value of cell 127 at time 8 = 2

then value of cell 3 at time 9 = 2

• instruction #14 is load dst=3 addr=1 imm=1
• the PC at time 8 = 14

then the PC at time 9 = 15

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

then value of cell 1 at time 9 = 126

• instruction #14 is load dst=3 addr=1 imm=1
• the PC at time 8 = 14
• value of cell 127 at time 8 = 2

then value of cell 127 at time 9 = 2

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

then value of cell 126 at time 9 = 3

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 15
• the PC at time 9 = 15
• value of cell 1 at time 9 = 126

then value of cell 1 at time 10 = 125

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 15
• the PC at time 9 = 15

then the PC at time 10 = 16

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 15
• the PC at time 9 = 15
• value of cell 3 at time 9 = 2

then value of cell 3 at time 10 = 2

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 15
• the PC at time 9 = 15
• value of cell 127 at time 9 = 2

then value of cell 127 at time 10 = 2

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 15
• the PC at time 9 = 15
• value of cell 126 at time 9 = 3

then value of cell 126 at time 10 = 3

• instruction #16 is store src=3 addr=1 imm=0
• the PC at time 10 = 16
• value of cell 1 at time 10 = 125
• value of cell 3 at time 10 = 2

then value of cell 125 at time 11 = 2

• instruction #16 is store src=3 addr=1 imm=0
• the PC at time 10 = 16

then the PC at time 11 = 17

• instruction #16 is store src=3 addr=1 imm=0
• the PC at time 10 = 16
• value of cell 1 at time 10 = 125
• value of cell 1 at time 10 = 125

then value of cell 1 at time 11 = 125

• instruction #16 is store src=3 addr=1 imm=0
• the PC at time 10 = 16
• value of cell 3 at time 10 = 2
• value of cell 1 at time 10 = 125

then value of cell 3 at time 11 = 2

• instruction #16 is store src=3 addr=1 imm=0
• the PC at time 10 = 16
• value of cell 127 at time 10 = 2
• value of cell 1 at time 10 = 125

then value of cell 127 at time 11 = 2

• instruction #16 is store src=3 addr=1 imm=0
• the PC at time 10 = 16
• value of cell 126 at time 10 = 3
• value of cell 1 at time 10 = 125

then value of cell 126 at time 11 = 3

• instruction #17 is load dst=3 addr=1 imm=1
• the PC at time 11 = 17
• value of cell 1 at time 11 = 125
• value of cell 126 at time 11 = 3

then value of cell 3 at time 12 = 3

• instruction #17 is load dst=3 addr=1 imm=1
• the PC at time 11 = 17

then the PC at time 12 = 18

• instruction #17 is load dst=3 addr=1 imm=1
• the PC at time 11 = 17
• value of cell 1 at time 11 = 125

then value of cell 1 at time 12 = 125

• instruction #17 is load dst=3 addr=1 imm=1
• the PC at time 11 = 17
• value of cell 127 at time 11 = 2

then value of cell 127 at time 12 = 2

• instruction #17 is load dst=3 addr=1 imm=1
• the PC at time 11 = 17
• value of cell 126 at time 11 = 3

then value of cell 126 at time 12 = 3

• instruction #17 is load dst=3 addr=1 imm=1
• the PC at time 11 = 17
• value of cell 125 at time 11 = 2

then value of cell 125 at time 12 = 2

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 18
• the PC at time 12 = 18
• value of cell 1 at time 12 = 125

then value of cell 1 at time 13 = 124

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 18
• the PC at time 12 = 18

then the PC at time 13 = 19

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 18
• the PC at time 12 = 18
• value of cell 3 at time 12 = 3

then value of cell 3 at time 13 = 3

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 18
• the PC at time 12 = 18
• value of cell 127 at time 12 = 2

then value of cell 127 at time 13 = 2

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 18
• the PC at time 12 = 18
• value of cell 126 at time 12 = 3

then value of cell 126 at time 13 = 3

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 18
• the PC at time 12 = 18
• value of cell 125 at time 12 = 2

then value of cell 125 at time 13 = 2

• instruction #19 is store src=3 addr=1 imm=0
• the PC at time 13 = 19
• value of cell 1 at time 13 = 124
• value of cell 3 at time 13 = 3

then value of cell 124 at time 14 = 3

• instruction #19 is store src=3 addr=1 imm=0
• the PC at time 13 = 19

then the PC at time 14 = 20

• instruction #19 is store src=3 addr=1 imm=0
• the PC at time 13 = 19
• value of cell 1 at time 13 = 124
• value of cell 1 at time 13 = 124

then value of cell 1 at time 14 = 124

• instruction #19 is store src=3 addr=1 imm=0
• the PC at time 13 = 19
• value of cell 3 at time 13 = 3
• value of cell 1 at time 13 = 124

then value of cell 3 at time 14 = 3

• instruction #19 is store src=3 addr=1 imm=0
• the PC at time 13 = 19
• value of cell 127 at time 13 = 2
• value of cell 1 at time 13 = 124

then value of cell 127 at time 14 = 2

• instruction #19 is store src=3 addr=1 imm=0
• the PC at time 13 = 19
• value of cell 126 at time 13 = 3
• value of cell 1 at time 13 = 124

then value of cell 126 at time 14 = 3

• instruction #19 is store src=3 addr=1 imm=0
• the PC at time 13 = 19
• value of cell 125 at time 13 = 2
• value of cell 1 at time 13 = 124

then value of cell 125 at time 14 = 2

• instruction #20 is a JAL instruction with jump to: 2
• the PC at time 14 = 20

then the PC at time 15 = 2

• instruction #20 is a JAL instruction with jump to: 2
• the PC at time 14 = 20

then value of cell 2 at time 15 = 21

• instruction #20 is a JAL instruction with jump to: 2
• the PC at time 14 = 20
• value of cell 1 at time 14 = 124

then value of cell 1 at time 15 = 124

• instruction #20 is a JAL instruction with jump to: 2
• the PC at time 14 = 20
• value of cell 3 at time 14 = 3

then value of cell 3 at time 15 = 3

• instruction #20 is a JAL instruction with jump to: 2
• the PC at time 14 = 20
• value of cell 127 at time 14 = 2

then value of cell 127 at time 15 = 2

• instruction #20 is a JAL instruction with jump to: 2
• the PC at time 14 = 20
• value of cell 126 at time 14 = 3

then value of cell 126 at time 15 = 3

• instruction #20 is a JAL instruction with jump to: 2
• the PC at time 14 = 20
• value of cell 125 at time 14 = 2

then value of cell 125 at time 15 = 2

• instruction #20 is a JAL instruction with jump to: 2
• the PC at time 14 = 20
• value of cell 124 at time 14 = 3

then value of cell 124 at time 15 = 3

• instruction #2 is load dst=3 addr=1 imm=1
• the PC at time 15 = 2
• value of cell 1 at time 15 = 124
• value of cell 125 at time 15 = 2

then value of cell 3 at time 16 = 2

• instruction #2 is load dst=3 addr=1 imm=1
• the PC at time 15 = 2

then the PC at time 16 = 3

• instruction #2 is load dst=3 addr=1 imm=1
• the PC at time 15 = 2
• value of cell 1 at time 15 = 124

then value of cell 1 at time 16 = 124

• instruction #2 is load dst=3 addr=1 imm=1
• the PC at time 15 = 2
• value of cell 127 at time 15 = 2

then value of cell 127 at time 16 = 2

• instruction #2 is load dst=3 addr=1 imm=1
• the PC at time 15 = 2
• value of cell 126 at time 15 = 3

then value of cell 126 at time 16 = 3

• instruction #2 is load dst=3 addr=1 imm=1
• the PC at time 15 = 2
• value of cell 125 at time 15 = 2

then value of cell 125 at time 16 = 2

• instruction #2 is load dst=3 addr=1 imm=1
• the PC at time 15 = 2
• value of cell 124 at time 15 = 3

then value of cell 124 at time 16 = 3

• instruction #2 is load dst=3 addr=1 imm=1
• the PC at time 15 = 2
• value of cell 2 at time 15 = 21

then value of cell 2 at time 16 = 21

• instruction #3 is load dst=4 addr=1 imm=0
• the PC at time 16 = 3
• value of cell 1 at time 16 = 124
• value of cell 124 at time 16 = 3

then value of cell 4 at time 17 = 3

• instruction #3 is load dst=4 addr=1 imm=0
• the PC at time 16 = 3

then the PC at time 17 = 4

• instruction #3 is load dst=4 addr=1 imm=0
• the PC at time 16 = 3
• value of cell 1 at time 16 = 124

then value of cell 1 at time 17 = 124

• instruction #3 is load dst=4 addr=1 imm=0
• the PC at time 16 = 3
• value of cell 3 at time 16 = 2

then value of cell 3 at time 17 = 2

• instruction #3 is load dst=4 addr=1 imm=0
• the PC at time 16 = 3
• value of cell 127 at time 16 = 2

then value of cell 127 at time 17 = 2

• instruction #3 is load dst=4 addr=1 imm=0
• the PC at time 16 = 3
• value of cell 126 at time 16 = 3

then value of cell 126 at time 17 = 3

• instruction #3 is load dst=4 addr=1 imm=0
• the PC at time 16 = 3
• value of cell 125 at time 16 = 2

then value of cell 125 at time 17 = 2

• instruction #3 is load dst=4 addr=1 imm=0
• the PC at time 16 = 3
• value of cell 124 at time 16 = 3

then value of cell 124 at time 17 = 3

• instruction #3 is load dst=4 addr=1 imm=0
• the PC at time 16 = 3
• value of cell 2 at time 16 = 21

then value of cell 2 at time 17 = 21

• the PC at time 17 = 4
• instruction #4 is add dst=3 src1=3 src2=4

then value of cell 3 at time 18 = (value of cell 3 at time 17) + (value of cell 4 at time 17)

• value of cell 3 at time 18 = (value of cell 3 at time 17) + (value of cell 4 at time 17)
• value of cell 3 at time 17 = 2
• value of cell 4 at time 17 = 3

then value of cell 3 at time 18 = 5

• instruction #4 is add dst=3 src1=3 src2=4
• the PC at time 17 = 4

then the PC at time 18 = 5

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

then value of cell 1 at time 18 = 124

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

then value of cell 127 at time 18 = 2

• instruction #4 is add dst=3 src1=3 src2=4
• the PC at time 17 = 4
• value of cell 126 at time 17 = 3

then value of cell 126 at time 18 = 3

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

then value of cell 125 at time 18 = 2

• instruction #4 is add dst=3 src1=3 src2=4
• the PC at time 17 = 4
• value of cell 124 at time 17 = 3

then value of cell 124 at time 18 = 3

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

then value of cell 2 at time 18 = 21

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

then value of cell 4 at time 18 = 3

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 5
• the PC at time 18 = 5
• value of cell 1 at time 18 = 124

then value of cell 1 at time 19 = 123

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 5
• the PC at time 18 = 5

then the PC at time 19 = 6

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 5
• the PC at time 18 = 5
• value of cell 3 at time 18 = 5

then value of cell 3 at time 19 = 5

• subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 5
• the PC at time 18 = 5
• value of cell 127 at time 18 = 2

then value of cell 127 at time 19 = 2