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

Byte 126 Stays the Same 18

if the following are true:

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

then value of cell 126 at time 19 = 3

Byte 125 Stays the Same 18

if the following are true:

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

then value of cell 125 at time 19 = 2

Byte 124 Stays the Same 18

if the following are true:

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

then value of cell 124 at time 19 = 3

Byte 2 Stays the Same 18

if the following are true:

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

then value of cell 2 at time 19 = 21

Byte 4 Stays the Same 18

if the following are true:

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

then value of cell 4 at time 19 = 3

Store 19

if the following are true:

instruction #6 is store src=3 addr=1 imm=0
the PC at time 19 = 6
value of cell 1 at time 19 = 123
value of cell 3 at time 19 = 5

then value of cell 123 at time 20 = 5

Pc 19

if the following are true:

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

then the PC at time 20 = 7

Byte 1 Stays the Same Store 19

if the following are true:

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

then value of cell 1 at time 20 = 123

Byte 3 Stays the Same Store 19

if the following are true:

instruction #6 is store src=3 addr=1 imm=0
the PC at time 19 = 6
value of cell 3 at time 19 = 5
value of cell 1 at time 19 = 123

then value of cell 3 at time 20 = 5

Byte 127 Stays the Same Store 19

if the following are true:

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

then value of cell 127 at time 20 = 2

Byte 126 Stays the Same Store 19

if the following are true:

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

then value of cell 126 at time 20 = 3

Byte 125 Stays the Same Store 19

if the following are true:

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

then value of cell 125 at time 20 = 2

Byte 124 Stays the Same Store 19

if the following are true:

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

then value of cell 124 at time 20 = 3

Byte 2 Stays the Same Store 19

if the following are true:

instruction #6 is store src=3 addr=1 imm=0
the PC at time 19 = 6
value of cell 2 at time 19 = 21
value of cell 1 at time 19 = 123

then value of cell 2 at time 20 = 21

Byte 4 Stays the Same Store 19

if the following are true:

instruction #6 is store src=3 addr=1 imm=0
the PC at time 19 = 6
value of cell 4 at time 19 = 3
value of cell 1 at time 19 = 123

then value of cell 4 at time 20 = 3

Jump Register Help 20

if the following are true:

instruction #7 is jumpr addr=2
the PC at time 20 = 7
value of cell 2 at time 20 = 21

then the PC at time 21 = 21

Byte 1 Stays the Same 20

if the following are true:

instruction #7 is jumpr addr=2
the PC at time 20 = 7
value of cell 1 at time 20 = 123

then value of cell 1 at time 21 = 123

Byte 3 Stays the Same 20

if the following are true:

instruction #7 is jumpr addr=2
the PC at time 20 = 7
value of cell 3 at time 20 = 5

then value of cell 3 at time 21 = 5

Byte 127 Stays the Same 20

if the following are true:

instruction #7 is jumpr addr=2
the PC at time 20 = 7
value of cell 127 at time 20 = 2

then value of cell 127 at time 21 = 2

Byte 126 Stays the Same 20

if the following are true:

instruction #7 is jumpr addr=2
the PC at time 20 = 7
value of cell 126 at time 20 = 3

then value of cell 126 at time 21 = 3

Byte 125 Stays the Same 20

if the following are true:

instruction #7 is jumpr addr=2
the PC at time 20 = 7
value of cell 125 at time 20 = 2

then value of cell 125 at time 21 = 2

Byte 124 Stays the Same 20

if the following are true:

instruction #7 is jumpr addr=2
the PC at time 20 = 7
value of cell 124 at time 20 = 3

then value of cell 124 at time 21 = 3

Byte 2 Stays the Same 20

if the following are true:

instruction #7 is jumpr addr=2
the PC at time 20 = 7
value of cell 2 at time 20 = 21

then value of cell 2 at time 21 = 21

Byte 4 Stays the Same 20

if the following are true:

instruction #7 is jumpr addr=2
the PC at time 20 = 7
value of cell 4 at time 20 = 3

then value of cell 4 at time 21 = 3

Byte 123 Stays the Same 20

if the following are true:

instruction #7 is jumpr addr=2
the PC at time 20 = 7
value of cell 123 at time 20 = 5

then value of cell 123 at time 21 = 5

Load 21

if the following are true:

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

then value of cell 3 at time 22 = 5

Pc 21

if the following are true:

instruction #21 is load dst=3 addr=1 imm=0
the PC at time 21 = 21

then the PC at time 22 = 22

Byte 1 Stays the Same 21

if the following are true:

instruction #21 is load dst=3 addr=1 imm=0
the PC at time 21 = 21
value of cell 1 at time 21 = 123

then value of cell 1 at time 22 = 123

Byte 127 Stays the Same 21

if the following are true:

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

then value of cell 127 at time 22 = 2

Byte 126 Stays the Same 21

if the following are true:

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

then value of cell 126 at time 22 = 3

Byte 125 Stays the Same 21

if the following are true:

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

then value of cell 125 at time 22 = 2

Byte 124 Stays the Same 21

if the following are true:

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

then value of cell 124 at time 22 = 3

Byte 2 Stays the Same 21

if the following are true:

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

then value of cell 2 at time 22 = 21

Byte 4 Stays the Same 21

if the following are true:

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

then value of cell 4 at time 22 = 3

Byte 123 Stays the Same 21

if the following are true:

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

then value of cell 123 at time 22 = 5

Addi Insn 22

if the following are true:

instruction #22 is addi dst=1 src=1 imm=3
the PC at time 22 = 22
value of cell 1 at time 22 = 123

then value of cell 1 at time 23 = 126

Pc 22

if the following are true:

instruction #22 is addi dst=1 src=1 imm=3
the PC at time 22 = 22

then the PC at time 23 = 23

Byte 3 Stays the Same 22

if the following are true:

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

then value of cell 3 at time 23 = 5

Byte 127 Stays the Same 22

if the following are true:

instruction #22 is addi dst=1 src=1 imm=3
the PC at time 22 = 22
value of cell 127 at time 22 = 2

then value of cell 127 at time 23 = 2

Byte 126 Stays the Same 22

if the following are true:

instruction #22 is addi dst=1 src=1 imm=3
the PC at time 22 = 22
value of cell 126 at time 22 = 3

then value of cell 126 at time 23 = 3

Byte 125 Stays the Same 22

if the following are true:

instruction #22 is addi dst=1 src=1 imm=3
the PC at time 22 = 22
value of cell 125 at time 22 = 2

then value of cell 125 at time 23 = 2

Byte 124 Stays the Same 22

if the following are true:

instruction #22 is addi dst=1 src=1 imm=3
the PC at time 22 = 22
value of cell 124 at time 22 = 3

then value of cell 124 at time 23 = 3

Byte 2 Stays the Same 22

if the following are true:

instruction #22 is addi dst=1 src=1 imm=3
the PC at time 22 = 22
value of cell 2 at time 22 = 21

then value of cell 2 at time 23 = 21

Byte 4 Stays the Same 22

if the following are true:

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

then value of cell 4 at time 23 = 3

Byte 123 Stays the Same 22

if the following are true:

instruction #22 is addi dst=1 src=1 imm=3
the PC at time 22 = 22
value of cell 123 at time 22 = 5

then value of cell 123 at time 23 = 5

Subtracti Insn 23

if the following are true:

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

then value of cell 1 at time 24 = 125

Pc 23

if the following are true:

subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 23
the PC at time 23 = 23

then the PC at time 24 = 24

Byte 3 Stays the Same 23

if the following are true:

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

then value of cell 3 at time 24 = 5

Byte 127 Stays the Same 23

if the following are true:

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

then value of cell 127 at time 24 = 2

Byte 126 Stays the Same 23

if the following are true:

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

then value of cell 126 at time 24 = 3

Byte 125 Stays the Same 23

if the following are true:

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

then value of cell 125 at time 24 = 2

Byte 124 Stays the Same 23

if the following are true:

subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 23
the PC at time 23 = 23
value of cell 124 at time 23 = 3

then value of cell 124 at time 24 = 3

Byte 2 Stays the Same 23

if the following are true:

subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 23
the PC at time 23 = 23
value of cell 2 at time 23 = 21

then value of cell 2 at time 24 = 21

Byte 4 Stays the Same 23

if the following are true:

subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 23
the PC at time 23 = 23
value of cell 4 at time 23 = 3

then value of cell 4 at time 24 = 3

Byte 123 Stays the Same 23

if the following are true:

subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 23
the PC at time 23 = 23
value of cell 123 at time 23 = 5

then value of cell 123 at time 24 = 5

Store 24

if the following are true:

instruction #24 is store src=3 addr=1 imm=0
the PC at time 24 = 24
value of cell 1 at time 24 = 125
value of cell 3 at time 24 = 5

then value of cell 125 at time 25 = 5

Pc 24

if the following are true:

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

then the PC at time 25 = 25

Byte 1 Stays the Same Store 24

if the following are true:

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

then value of cell 1 at time 25 = 125

Byte 3 Stays the Same Store 24

if the following are true:

instruction #24 is store src=3 addr=1 imm=0
the PC at time 24 = 24
value of cell 3 at time 24 = 5
value of cell 1 at time 24 = 125

then value of cell 3 at time 25 = 5

Byte 127 Stays the Same Store 24

if the following are true:

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

then value of cell 127 at time 25 = 2

Byte 126 Stays the Same Store 24

if the following are true:

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

then value of cell 126 at time 25 = 3

Byte 124 Stays the Same Store 24

if the following are true:

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

then value of cell 124 at time 25 = 3

Byte 2 Stays the Same Store 24

if the following are true:

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

then value of cell 2 at time 25 = 21

Byte 4 Stays the Same Store 24

if the following are true:

instruction #24 is store src=3 addr=1 imm=0
the PC at time 24 = 24
value of cell 4 at time 24 = 3
value of cell 1 at time 24 = 125

then value of cell 4 at time 25 = 3

Byte 123 Stays the Same Store 24

if the following are true:

instruction #24 is store src=3 addr=1 imm=0
the PC at time 24 = 24
value of cell 123 at time 24 = 5
value of cell 1 at time 24 = 125

then value of cell 123 at time 25 = 5

Adder

if the following are true:

the PC at time 0 = 0
instruction #0 is addi dst=1 src=0 imm=128
instruction #1 is jump imm=8
instruction #2 is load dst=3 addr=1 imm=1
instruction #3 is load dst=4 addr=1 imm=0
instruction #4 is add dst=3 src1=3 src2=4
subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 5
instruction #6 is store src=3 addr=1 imm=0
instruction #7 is jumpr addr=2
instruction #8 is addi dst=3 src=0 imm=2
subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 9
instruction #10 is store src=3 addr=1 imm=0
instruction #11 is addi dst=3 src=0 imm=3
subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 12
instruction #13 is store src=3 addr=1 imm=0
instruction #14 is load dst=3 addr=1 imm=1
subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 15
instruction #16 is store src=3 addr=1 imm=0
instruction #17 is load dst=3 addr=1 imm=1
subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 18
instruction #19 is store src=3 addr=1 imm=0
instruction #20 is a JAL instruction with jump to: 2
instruction #21 is load dst=3 addr=1 imm=0
instruction #22 is addi dst=1 src=1 imm=3
subtract immediate instruction with dst: 1 src: 1 and immediate: 1 at 23
instruction #24 is store src=3 addr=1 imm=0

then value of cell 123 at time 25 = 5

Greater Than Substitution

if the following are true:

x is greater than y
minimum value of stack z = y

then x is greater than (minimum value of stack z)

Reversing an Empty List

reverse of [ ] = [ ]

Reverse List Example

reverse of [ 3, [ 2, [ 1, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ]

Setting a Key to a Value Example

result of storing "Mike" at key: "name" in map: [ entry "name": "John", [ ] ] = [ entry "name": "Mike", [ ] ]

Add Key Example

result of storing "New York" at key: "city" in map: [ entry "name": "John", [ ] ] = [ entry "name": "John", [ entry "city": "New York", [ ] ] ]

Set Key Example 2

result of storing "Denver" at key: "city" in map: [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = [ entry "name": "John", [ entry "city": "Denver", [ entry "country": "USA", [ ] ] ] ]

Get Key Example

value at "AK" in map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] = "Alaska"

Delete Key Example

result of deleting the entry with key "country" from map [ entry "name": "John", [ entry "city": "New York", [ entry "country": "USA", [ ] ] ] ] = [ entry "name": "John", [ entry "city": "New York", [ ] ] ]

Reverse List Example 2

reverse of [ 1, [ 2, [ 3, [ ] ] ] ] = [ 3, [ 2, [ 1, [ ] ] ] ]

Reverse List Example 3

reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = [ 1, [ 2, [ 3, [ 4, [ ] ] ] ] ]

Append to List Example

result of appending 4 to [ 1, [ 2, [ 3, [ ] ] ] ] = [ 1, [ 2, [ 3, [ 4, [ ] ] ] ] ]

Element At Example

the element at index 0 of stack [ 10, [ 12, [ 14, [ ] ] ] ] = 10

List Get Item Example

the element at index 2 of stack [ 10, [ 12, [ 14, [ ] ] ] ] = 14

List Length Example

length of stack [ 10, [ 12, [ 14, [ ] ] ] ] = 3

Reverse List Example 4

reverse of [ 14, [ 10, [ ] ] ] = [ 10, [ 14, [ ] ] ]

Pop At Example

stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 = [ 10, [ 14, [ ] ] ]

List Contains Element Example

stack [ 2, [ 4, [ 6, [ ] ] ] ] contains 4 = True

Map Has Key Example

map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] contains key "AK" = True

Map Does Not Have Key Example

map [ entry "OH": "Ohio", [ entry "AK": "Alaska", [ entry "IA": "Iowa", [ ] ] ] ] contains key "TX" = False

Pre Extend Example

reverse and insert [ 4, [ 0, [ ] ] ] to the beginning of [ 2, [ ] ] = [ 0, [ 4, [ 2, [ ] ] ] ]

Set List Element at Index Example

result of storing 4 at index 1 of stack [ 0, [ 1, [ 2, [ ] ] ] ] = [ 0, [ 4, [ 2, [ ] ] ] ]

Push Stack Example

result of dumping [ 4, [ 0, [ ] ] ] to [ 2, [ ] ] = [ 0, [ 4, [ 2, [ ] ] ] ]

Reverse Example

reverse of remaining stack [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] and already reversed stack [ ] = [ [ 1, [ ] ], [ [ 0, [ ] ], [ ] ] ]

Reverse List Two General

reverse of remaining stack [ [ x, [ ] ], [ [ y, [ ] ], [ ] ] ] and already reversed stack [ ] = [ [ y, [ ] ], [ [ x, [ ] ], [ ] ] ]

Reverse Two

reverse of [ [ x, [ ] ], [ [ y, [ ] ], [ ] ] ] = [ [ y, [ ] ], [ [ x, [ ] ], [ ] ] ]

Reverse One

reverse of [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ]

Reverse Example General

reverse of [ x, [ ] ] = [ x, [ ] ]

Set Key Value Example

result of storing 5 at key: a in map: [ ] = [ entry a: 5, [ ] ]

Compare Example

compare bit stack [ 0, [ ] ] and bit stack [ 1, [ ] ] = [ 0, [ 0, [ ] ] ]

Compare Example Eq

compare bit stack [ 1, [ ] ] and bit stack [ 1, [ ] ] = [ 1, [ 0, [ ] ] ]

Compare Example Gt

compare bit stack [ 1, [ ] ] and bit stack [ 0, [ ] ] = [ 0, [ 1, [ ] ] ]

Compare Example Two

compare bit stack [ 0, [ 1, [ ] ] ] and bit stack [ 1, [ 1, [ ] ] ] = [ 0, [ 0, [ ] ] ]

Compare Example Three

compare bit stack [ 1, [ 0, [ 1, [ ] ] ] ] and bit stack [ 0, [ 1, [ 1, [ ] ] ] ] = [ 0, [ 0, [ ] ] ]

Less Than Example

[ 0, [ ] ] is less than [ 1, [ ] ]

Pages: 11 12 13 ... 16