Commutative Property Variation 1
Substitution 2
Substitution 6
Zero Plus a
Addi to Zero

Proof: Addi to Zero

Let's prove the following theorem:

if the following are true:
  • instruction #i is addi dst=dst src=0 imm=imm
  • the PC at time t = i

then value of cell dst at time (t + 1) = imm

Instructions
Memory Cells
Program Counter Time
0 0
LW Computer Simulator

Proof:

View as a tree | View dependent proofs | Try proving it

Given
1 instruction #i is addi dst=dst src=0 imm=imm
2 the PC at time t = i
Proof Table
# Claim Reason
1 value of cell dst at time (t + 1) = (value of cell 0 at time t) + imm if instruction #i is addi dst=dst src=0 imm=imm and the PC at time t = i, then value of cell dst at time (t + 1) = (value of cell 0 at time t) + imm
2 value of cell 0 at time t = 0 value of cell 0 at time t = 0
3 value of cell dst at time (t + 1) = 0 + imm if value of cell dst at time (t + 1) = (value of cell 0 at time t) + imm and value of cell 0 at time t = 0, then value of cell dst at time (t + 1) = 0 + imm
4 0 + imm = imm 0 + imm = imm
5 value of cell dst at time (t + 1) = imm if value of cell dst at time (t + 1) = 0 + imm and 0 + imm = imm, then value of cell dst at time (t + 1) = imm
Previous Lesson

Comments

Please log in to add comments