Proof: Fibonacci
Let's prove the following theorem:
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
Proof:
Given
| 1 | the PC at time 0 = 0 |
|---|---|
| 2 | instruction #0 is addi dst=1 src=0 imm=0 |
| 3 | instruction #1 is addi dst=2 src=0 imm=1 |
| 4 | instruction #2 is addi dst=4 src=0 imm=0 |
| 5 | instruction #3 is addi dst=5 src=0 imm=3 |
| 6 | instruction #4 is add dst=3 src1=1 src2=2 |
| 7 | instruction #5 is addi dst=1 src=2 imm=0 |
| 8 | instruction #6 is addi dst=2 src=3 imm=0 |
| 9 | instruction #7 is addi dst=4 src=4 imm=1 |
| 10 | instruction #8 is beq left=4 right=5 imm=1 |
| 11 | instruction #9 is jump imm=4 |
| 12 | instruction #10 is addi dst=1 src=0 imm=0 |
| # | Claim | Reason |
|---|---|---|
| 1 | value of cell 1 at time 1 = 0 | if instruction #0 is addi dst=1 src=0 imm=0 and the PC at time 0 = 0, then value of cell 1 at time 1 = 0 |
| 2 | the PC at time 1 = 1 | if instruction #0 is addi dst=1 src=0 imm=0 and the PC at time 0 = 0, then the PC at time 1 = 1 |
| 3 | value of cell 2 at time 2 = 1 | if instruction #1 is addi dst=2 src=0 imm=1 and the PC at time 1 = 1, then value of cell 2 at time 2 = 1 |
| 4 | value of cell 1 at time 2 = 0 | if instruction #1 is addi dst=2 src=0 imm=1 and the PC at time 1 = 1 and value of cell 1 at time 1 = 0, then value of cell 1 at time 2 = 0 |
| 5 | the PC at time 2 = 2 | if instruction #1 is addi dst=2 src=0 imm=1 and the PC at time 1 = 1, then the PC at time 2 = 2 |
| 6 | value of cell 4 at time 3 = 0 | if instruction #2 is addi dst=4 src=0 imm=0 and the PC at time 2 = 2, then value of cell 4 at time 3 = 0 |
| 7 | value of cell 1 at time 3 = 0 | if instruction #2 is addi dst=4 src=0 imm=0 and the PC at time 2 = 2 and value of cell 1 at time 2 = 0, then value of cell 1 at time 3 = 0 |
| 8 | value of cell 2 at time 3 = 1 | if instruction #2 is addi dst=4 src=0 imm=0 and the PC at time 2 = 2 and value of cell 2 at time 2 = 1, then value of cell 2 at time 3 = 1 |
| 9 | the PC at time 3 = 3 | if instruction #2 is addi dst=4 src=0 imm=0 and the PC at time 2 = 2, then the PC at time 3 = 3 |
| 10 | value of cell 5 at time 4 = 3 | if instruction #3 is addi dst=5 src=0 imm=3 and the PC at time 3 = 3, then value of cell 5 at time 4 = 3 |
| 11 | value of cell 1 at time 4 = 0 | if instruction #3 is addi dst=5 src=0 imm=3 and the PC at time 3 = 3 and value of cell 1 at time 3 = 0, then value of cell 1 at time 4 = 0 |
| 12 | value of cell 2 at time 4 = 1 | if instruction #3 is addi dst=5 src=0 imm=3 and the PC at time 3 = 3 and value of cell 2 at time 3 = 1, then value of cell 2 at time 4 = 1 |
| 13 | value of cell 4 at time 4 = 0 | if instruction #3 is addi dst=5 src=0 imm=3 and the PC at time 3 = 3 and value of cell 4 at time 3 = 0, then value of cell 4 at time 4 = 0 |
| 14 | the PC at time 4 = 4 | if instruction #3 is addi dst=5 src=0 imm=3 and the PC at time 3 = 3, then the PC at time 4 = 4 |
| 15 | value of cell 3 at time 5 = (value of cell 1 at time 4) + (value of cell 2 at time 4) | if the PC at time 4 = 4 and 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) |
| 16 | value of cell 3 at time 5 = 1 | if value of cell 3 at time 5 = (value of cell 1 at time 4) + (value of cell 2 at time 4) and value of cell 1 at time 4 = 0 and value of cell 2 at time 4 = 1, then value of cell 3 at time 5 = 1 |
| 17 | value of cell 2 at time 5 = 1 | if instruction #4 is add dst=3 src1=1 src2=2 and the PC at time 4 = 4 and value of cell 2 at time 4 = 1, then value of cell 2 at time 5 = 1 |
| 18 | value of cell 4 at time 5 = 0 | if instruction #4 is add dst=3 src1=1 src2=2 and the PC at time 4 = 4 and value of cell 4 at time 4 = 0, then value of cell 4 at time 5 = 0 |
| 19 | value of cell 5 at time 5 = 3 | if instruction #4 is add dst=3 src1=1 src2=2 and the PC at time 4 = 4 and value of cell 5 at time 4 = 3, then value of cell 5 at time 5 = 3 |
| 20 | the PC at time 5 = 5 | if instruction #4 is add dst=3 src1=1 src2=2 and the PC at time 4 = 4, then the PC at time 5 = 5 |
| 21 | value of cell 1 at time 6 = 1 | if instruction #5 is addi dst=1 src=2 imm=0 and the PC at time 5 = 5 and value of cell 2 at time 5 = 1, then value of cell 1 at time 6 = 1 |
| 22 | value of cell 3 at time 6 = 1 | if instruction #5 is addi dst=1 src=2 imm=0 and the PC at time 5 = 5 and value of cell 3 at time 5 = 1, then value of cell 3 at time 6 = 1 |
| 23 | value of cell 4 at time 6 = 0 | if instruction #5 is addi dst=1 src=2 imm=0 and the PC at time 5 = 5 and value of cell 4 at time 5 = 0, then value of cell 4 at time 6 = 0 |
| 24 | value of cell 5 at time 6 = 3 | if instruction #5 is addi dst=1 src=2 imm=0 and the PC at time 5 = 5 and value of cell 5 at time 5 = 3, then value of cell 5 at time 6 = 3 |
| 25 | the PC at time 6 = 6 | if instruction #5 is addi dst=1 src=2 imm=0 and the PC at time 5 = 5, then the PC at time 6 = 6 |
| 26 | value of cell 1 at time 7 = 1 | if instruction #6 is addi dst=2 src=3 imm=0 and the PC at time 6 = 6 and value of cell 1 at time 6 = 1, then value of cell 1 at time 7 = 1 |
| 27 | value of cell 2 at time 7 = 1 | if instruction #6 is addi dst=2 src=3 imm=0 and the PC at time 6 = 6 and value of cell 3 at time 6 = 1, then value of cell 2 at time 7 = 1 |
| 28 | value of cell 4 at time 7 = 0 | if instruction #6 is addi dst=2 src=3 imm=0 and the PC at time 6 = 6 and value of cell 4 at time 6 = 0, then value of cell 4 at time 7 = 0 |
| 29 | value of cell 5 at time 7 = 3 | if instruction #6 is addi dst=2 src=3 imm=0 and the PC at time 6 = 6 and value of cell 5 at time 6 = 3, then value of cell 5 at time 7 = 3 |
| 30 | the PC at time 7 = 7 | if instruction #6 is addi dst=2 src=3 imm=0 and the PC at time 6 = 6, then the PC at time 7 = 7 |
| 31 | value of cell 1 at time 8 = 1 | if instruction #7 is addi dst=4 src=4 imm=1 and the PC at time 7 = 7 and value of cell 1 at time 7 = 1, then value of cell 1 at time 8 = 1 |
| 32 | value of cell 2 at time 8 = 1 | if instruction #7 is addi dst=4 src=4 imm=1 and the PC at time 7 = 7 and value of cell 2 at time 7 = 1, then value of cell 2 at time 8 = 1 |
| 33 | value of cell 4 at time 8 = 1 | if instruction #7 is addi dst=4 src=4 imm=1 and the PC at time 7 = 7 and value of cell 4 at time 7 = 0, then value of cell 4 at time 8 = 1 |
| 34 | value of cell 5 at time 8 = 3 | if instruction #7 is addi dst=4 src=4 imm=1 and the PC at time 7 = 7 and value of cell 5 at time 7 = 3, then value of cell 5 at time 8 = 3 |
| 35 | the PC at time 8 = 8 | if instruction #7 is addi dst=4 src=4 imm=1 and the PC at time 7 = 7, then the PC at time 8 = 8 |
| 36 | value of cell 1 at time 9 = 1 | if instruction #8 is beq left=4 right=5 imm=1 and the PC at time 8 = 8 and value of cell 1 at time 8 = 1, then value of cell 1 at time 9 = 1 |
| 37 | value of cell 2 at time 9 = 1 | if instruction #8 is beq left=4 right=5 imm=1 and the PC at time 8 = 8 and value of cell 2 at time 8 = 1, then value of cell 2 at time 9 = 1 |
| 38 | value of cell 4 at time 9 = 1 | if instruction #8 is beq left=4 right=5 imm=1 and the PC at time 8 = 8 and value of cell 4 at time 8 = 1, then value of cell 4 at time 9 = 1 |
| 39 | value of cell 5 at time 9 = 3 | if instruction #8 is beq left=4 right=5 imm=1 and the PC at time 8 = 8 and value of cell 5 at time 8 = 3, then value of cell 5 at time 9 = 3 |
| 40 | the PC at time 9 = 9 | if instruction #8 is beq left=4 right=5 imm=1 and the PC at time 8 = 8 and value of cell 4 at time 8 = 1 and value of cell 5 at time 8 = 3, then the PC at time 9 = 9 |
| 41 | the PC at time 10 = 4 | if instruction #9 is jump imm=4 and the PC at time 9 = 9, then the PC at time 10 = 4 |
| 42 | value of cell 1 at time 10 = 1 | if instruction #9 is jump imm=4 and the PC at time 9 = 9 and value of cell 1 at time 9 = 1, then value of cell 1 at time 10 = 1 |
| 43 | value of cell 2 at time 10 = 1 | if instruction #9 is jump imm=4 and the PC at time 9 = 9 and value of cell 2 at time 9 = 1, then value of cell 2 at time 10 = 1 |
| 44 | value of cell 4 at time 10 = 1 | if instruction #9 is jump imm=4 and the PC at time 9 = 9 and value of cell 4 at time 9 = 1, then value of cell 4 at time 10 = 1 |
| 45 | value of cell 5 at time 10 = 3 | if instruction #9 is jump imm=4 and the PC at time 9 = 9 and value of cell 5 at time 9 = 3, then value of cell 5 at time 10 = 3 |
| 46 | the PC at time 11 = 5 | if instruction #4 is add dst=3 src1=1 src2=2 and the PC at time 10 = 4, then the PC at time 11 = 5 |
| 47 | value of cell 2 at time 11 = 1 | if instruction #4 is add dst=3 src1=1 src2=2 and the PC at time 10 = 4 and value of cell 2 at time 10 = 1, then value of cell 2 at time 11 = 1 |
| 48 | value of cell 3 at time 11 = (value of cell 1 at time 10) + (value of cell 2 at time 10) | if the PC at time 10 = 4 and instruction #4 is add dst=3 src1=1 src2=2, then value of cell 3 at time 11 = (value of cell 1 at time 10) + (value of cell 2 at time 10) |
| 49 | value of cell 3 at time 11 = 2 | if value of cell 3 at time 11 = (value of cell 1 at time 10) + (value of cell 2 at time 10) and value of cell 1 at time 10 = 1 and value of cell 2 at time 10 = 1, then value of cell 3 at time 11 = 2 |
| 50 | value of cell 4 at time 11 = 1 | if instruction #4 is add dst=3 src1=1 src2=2 and the PC at time 10 = 4 and value of cell 4 at time 10 = 1, then value of cell 4 at time 11 = 1 |
| 51 | value of cell 5 at time 11 = 3 | if instruction #4 is add dst=3 src1=1 src2=2 and the PC at time 10 = 4 and value of cell 5 at time 10 = 3, then value of cell 5 at time 11 = 3 |
| 52 | the PC at time 12 = 6 | if instruction #5 is addi dst=1 src=2 imm=0 and the PC at time 11 = 5, then the PC at time 12 = 6 |
| 53 | value of cell 1 at time 12 = 1 | if instruction #5 is addi dst=1 src=2 imm=0 and the PC at time 11 = 5 and value of cell 2 at time 11 = 1, then value of cell 1 at time 12 = 1 |
| 54 | value of cell 3 at time 12 = 2 | if instruction #5 is addi dst=1 src=2 imm=0 and the PC at time 11 = 5 and value of cell 3 at time 11 = 2, then value of cell 3 at time 12 = 2 |
| 55 | value of cell 4 at time 12 = 1 | if instruction #5 is addi dst=1 src=2 imm=0 and the PC at time 11 = 5 and value of cell 4 at time 11 = 1, then value of cell 4 at time 12 = 1 |
| 56 | value of cell 5 at time 12 = 3 | if instruction #5 is addi dst=1 src=2 imm=0 and the PC at time 11 = 5 and value of cell 5 at time 11 = 3, then value of cell 5 at time 12 = 3 |
| 57 | the PC at time 13 = 7 | if instruction #6 is addi dst=2 src=3 imm=0 and the PC at time 12 = 6, then the PC at time 13 = 7 |
| 58 | value of cell 1 at time 13 = 1 | if instruction #6 is addi dst=2 src=3 imm=0 and the PC at time 12 = 6 and value of cell 1 at time 12 = 1, then value of cell 1 at time 13 = 1 |
| 59 | value of cell 2 at time 13 = 2 | if instruction #6 is addi dst=2 src=3 imm=0 and the PC at time 12 = 6 and value of cell 3 at time 12 = 2, then value of cell 2 at time 13 = 2 |
| 60 | value of cell 4 at time 13 = 1 | if instruction #6 is addi dst=2 src=3 imm=0 and the PC at time 12 = 6 and value of cell 4 at time 12 = 1, then value of cell 4 at time 13 = 1 |
| 61 | value of cell 5 at time 13 = 3 | if instruction #6 is addi dst=2 src=3 imm=0 and the PC at time 12 = 6 and value of cell 5 at time 12 = 3, then value of cell 5 at time 13 = 3 |
| 62 | the PC at time 14 = 8 | if instruction #7 is addi dst=4 src=4 imm=1 and the PC at time 13 = 7, then the PC at time 14 = 8 |
| 63 | value of cell 1 at time 14 = 1 | if instruction #7 is addi dst=4 src=4 imm=1 and the PC at time 13 = 7 and value of cell 1 at time 13 = 1, then value of cell 1 at time 14 = 1 |
| 64 | value of cell 2 at time 14 = 2 | if instruction #7 is addi dst=4 src=4 imm=1 and the PC at time 13 = 7 and value of cell 2 at time 13 = 2, then value of cell 2 at time 14 = 2 |
| 65 | value of cell 4 at time 14 = 2 | if instruction #7 is addi dst=4 src=4 imm=1 and the PC at time 13 = 7 and value of cell 4 at time 13 = 1, then value of cell 4 at time 14 = 2 |
| 66 | value of cell 5 at time 14 = 3 | if instruction #7 is addi dst=4 src=4 imm=1 and the PC at time 13 = 7 and value of cell 5 at time 13 = 3, then value of cell 5 at time 14 = 3 |
| 67 | the PC at time 15 = 9 | if instruction #8 is beq left=4 right=5 imm=1 and the PC at time 14 = 8 and value of cell 4 at time 14 = 2 and value of cell 5 at time 14 = 3, then the PC at time 15 = 9 |
| 68 | value of cell 1 at time 15 = 1 | if instruction #8 is beq left=4 right=5 imm=1 and the PC at time 14 = 8 and value of cell 1 at time 14 = 1, then value of cell 1 at time 15 = 1 |
| 69 | value of cell 2 at time 15 = 2 | if instruction #8 is beq left=4 right=5 imm=1 and the PC at time 14 = 8 and value of cell 2 at time 14 = 2, then value of cell 2 at time 15 = 2 |
| 70 | value of cell 4 at time 15 = 2 | if instruction #8 is beq left=4 right=5 imm=1 and the PC at time 14 = 8 and value of cell 4 at time 14 = 2, then value of cell 4 at time 15 = 2 |
| 71 | value of cell 5 at time 15 = 3 | if instruction #8 is beq left=4 right=5 imm=1 and the PC at time 14 = 8 and value of cell 5 at time 14 = 3, then value of cell 5 at time 15 = 3 |
| 72 | the PC at time 16 = 4 | if instruction #9 is jump imm=4 and the PC at time 15 = 9, then the PC at time 16 = 4 |
| 73 | value of cell 1 at time 16 = 1 | if instruction #9 is jump imm=4 and the PC at time 15 = 9 and value of cell 1 at time 15 = 1, then value of cell 1 at time 16 = 1 |
| 74 | value of cell 2 at time 16 = 2 | if instruction #9 is jump imm=4 and the PC at time 15 = 9 and value of cell 2 at time 15 = 2, then value of cell 2 at time 16 = 2 |
| 75 | value of cell 4 at time 16 = 2 | if instruction #9 is jump imm=4 and the PC at time 15 = 9 and value of cell 4 at time 15 = 2, then value of cell 4 at time 16 = 2 |
| 76 | value of cell 5 at time 16 = 3 | if instruction #9 is jump imm=4 and the PC at time 15 = 9 and value of cell 5 at time 15 = 3, then value of cell 5 at time 16 = 3 |
| 77 | the PC at time 17 = 5 | if instruction #4 is add dst=3 src1=1 src2=2 and the PC at time 16 = 4, then the PC at time 17 = 5 |
| 78 | value of cell 3 at time 17 = (value of cell 1 at time 16) + (value of cell 2 at time 16) | if the PC at time 16 = 4 and instruction #4 is add dst=3 src1=1 src2=2, then value of cell 3 at time 17 = (value of cell 1 at time 16) + (value of cell 2 at time 16) |
| 79 | value of cell 3 at time 17 = 3 | if value of cell 3 at time 17 = (value of cell 1 at time 16) + (value of cell 2 at time 16) and value of cell 1 at time 16 = 1 and value of cell 2 at time 16 = 2, then value of cell 3 at time 17 = 3 |
| 80 | value of cell 4 at time 17 = 2 | if instruction #4 is add dst=3 src1=1 src2=2 and the PC at time 16 = 4 and value of cell 4 at time 16 = 2, then value of cell 4 at time 17 = 2 |
| 81 | value of cell 5 at time 17 = 3 | if instruction #4 is add dst=3 src1=1 src2=2 and the PC at time 16 = 4 and value of cell 5 at time 16 = 3, then value of cell 5 at time 17 = 3 |
| 82 | the PC at time 18 = 6 | if instruction #5 is addi dst=1 src=2 imm=0 and the PC at time 17 = 5, then the PC at time 18 = 6 |
| 83 | value of cell 3 at time 18 = 3 | if instruction #5 is addi dst=1 src=2 imm=0 and the PC at time 17 = 5 and value of cell 3 at time 17 = 3, then value of cell 3 at time 18 = 3 |
| 84 | value of cell 4 at time 18 = 2 | if instruction #5 is addi dst=1 src=2 imm=0 and the PC at time 17 = 5 and value of cell 4 at time 17 = 2, then value of cell 4 at time 18 = 2 |
| 85 | value of cell 5 at time 18 = 3 | if instruction #5 is addi dst=1 src=2 imm=0 and the PC at time 17 = 5 and value of cell 5 at time 17 = 3, then value of cell 5 at time 18 = 3 |
| 86 | the PC at time 19 = 7 | if instruction #6 is addi dst=2 src=3 imm=0 and the PC at time 18 = 6, then the PC at time 19 = 7 |
| 87 | value of cell 3 at time 19 = 3 | if instruction #6 is addi dst=2 src=3 imm=0 and the PC at time 18 = 6 and value of cell 3 at time 18 = 3, then value of cell 3 at time 19 = 3 |
| 88 | value of cell 4 at time 19 = 2 | if instruction #6 is addi dst=2 src=3 imm=0 and the PC at time 18 = 6 and value of cell 4 at time 18 = 2, then value of cell 4 at time 19 = 2 |
| 89 | value of cell 5 at time 19 = 3 | if instruction #6 is addi dst=2 src=3 imm=0 and the PC at time 18 = 6 and value of cell 5 at time 18 = 3, then value of cell 5 at time 19 = 3 |
| 90 | the PC at time 20 = 8 | if instruction #7 is addi dst=4 src=4 imm=1 and the PC at time 19 = 7, then the PC at time 20 = 8 |
| 91 | value of cell 3 at time 20 = 3 | if instruction #7 is addi dst=4 src=4 imm=1 and the PC at time 19 = 7 and value of cell 3 at time 19 = 3, then value of cell 3 at time 20 = 3 |
| 92 | value of cell 4 at time 20 = 3 | if instruction #7 is addi dst=4 src=4 imm=1 and the PC at time 19 = 7 and value of cell 4 at time 19 = 2, then value of cell 4 at time 20 = 3 |
| 93 | value of cell 5 at time 20 = 3 | if instruction #7 is addi dst=4 src=4 imm=1 and the PC at time 19 = 7 and value of cell 5 at time 19 = 3, then value of cell 5 at time 20 = 3 |
| 94 | the PC at time 21 = 10 | if instruction #8 is beq left=4 right=5 imm=1 and the PC at time 20 = 8 and value of cell 4 at time 20 = 3 and value of cell 5 at time 20 = 3, then the PC at time 21 = 10 |
| 95 | value of cell 3 at time 21 = 3 | if instruction #8 is beq left=4 right=5 imm=1 and the PC at time 20 = 8 and value of cell 3 at time 20 = 3, then value of cell 3 at time 21 = 3 |
| 96 | value of cell 3 at time 22 = 3 | if instruction #10 is addi dst=1 src=0 imm=0 and the PC at time 21 = 10 and value of cell 3 at time 21 = 3, then value of cell 3 at time 22 = 3 |
Comments
Please log in to add comments