Try out this example in the simulator:

Notice how addr remains the same, and the imm is increased.

Instruction #0 copies cell #3 to cell #7. The source is the value stored in cell #6 (3) plus the imm (0).

Instruction #1 copies cell #4 to cell #8. The source is the value stored in cell #6 (3) plus the imm (1).

Instruction #2 copies cell #5 to cell #9. The source is the value stored in cell #6 (3) plus the imm (2).

To make claims about value of the cell #8 at time 3, we start at time 0, then make claims about the state at time 1, and use them to make claims about time 2, and so on.

Quiz (1 point)

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

• 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

Please write your proof in the table below. Each row should contain one claim. The last claim is the statement that you are trying to prove.