Proof: Set List Element at Index Example

Let's prove the following theorem:

In this example, we prove that when we set index 1 of list [0, [1, [2,[]]]] to 4, the result is [0, [4, [2, []]]].

There are two parts to this process. In part 1, we pop an element from the front of the list, store this element in a "visited" list, and decrease the index by 1. We repeat this until index is 0. At this point, we have reached the element that we want to replace.

In part 2, we pop the element to be replaced. Then we prepend the new value (4) to the "visited" list, reverse it, and then prepend the reversed list to the remaining list.

For instance, the following:

set index 1 of remaining stack [ 0, [ 1, [ 2, [ ] ] ] ] to 4 with visited : [ ]

is equal to:

set index 0 of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ]

which is equal to:

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

which is equal to:

[ 0, [ 4, [ 2, [ ] ] ] ]

Proof:

Proof Table

#	Claim	Reason
1	result of storing 4 at index 1 of stack [ 0, [ 1, [ 2, [ ] ] ] ] = set index 1 of remaining stack [ 0, [ 1, [ 2, [ ] ] ] ] to 4 with visited : [ ]	result of storing 4 at index 1 of stack [ 0, [ 1, [ 2, [ ] ] ] ] = set index 1 of remaining stack [ 0, [ 1, [ 2, [ ] ] ] ] to 4 with visited : [ ] (Set List Element at Index Property)
2	set index 1 of remaining stack [ 0, [ 1, [ 2, [ ] ] ] ] to 4 with visited : [ ] = set index (1 - 1) of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ]	set index 1 of remaining stack [ 0, [ 1, [ 2, [ ] ] ] ] to 4 with visited : [ ] = set index (1 - 1) of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] (Set List Element at Index Recurse Property)
3	1 - 1 = 0	1 - 1 = 0 (Fixed Value Statement)
4	set index (1 - 1) of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] = set index 0 of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ]	if 1 - 1 = 0, then set index (1 - 1) of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] = set index 0 of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] (Substitution)
5	set index 0 of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] = result of dumping [ 4, [ 0, [ ] ] ] to [ 2, [ ] ]	set index 0 of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] = result of dumping [ 4, [ 0, [ ] ] ] to [ 2, [ ] ] (Set List Element at Index Base Property)
6	result of dumping [ 4, [ 0, [ ] ] ] to [ 2, [ ] ] = [ 0, [ 4, [ 2, [ ] ] ] ]	result of dumping [ 4, [ 0, [ ] ] ] to [ 2, [ ] ] = [ 0, [ 4, [ 2, [ ] ] ] ] (push_stack_example)
7	set index 0 of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] = [ 0, [ 4, [ 2, [ ] ] ] ]	if set index 0 of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] = result of dumping [ 4, [ 0, [ ] ] ] to [ 2, [ ] ] and result of dumping [ 4, [ 0, [ ] ] ] to [ 2, [ ] ] = [ 0, [ 4, [ 2, [ ] ] ] ], then set index 0 of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] = [ 0, [ 4, [ 2, [ ] ] ] ] (Transitive Property of Equality)
8	set index (1 - 1) of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] = [ 0, [ 4, [ 2, [ ] ] ] ]	if set index (1 - 1) of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] = set index 0 of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] and set index 0 of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] = [ 0, [ 4, [ 2, [ ] ] ] ], then set index (1 - 1) of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] = [ 0, [ 4, [ 2, [ ] ] ] ] (Transitive Property of Equality)
9	set index 1 of remaining stack [ 0, [ 1, [ 2, [ ] ] ] ] to 4 with visited : [ ] = [ 0, [ 4, [ 2, [ ] ] ] ]	if set index 1 of remaining stack [ 0, [ 1, [ 2, [ ] ] ] ] to 4 with visited : [ ] = set index (1 - 1) of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] and set index (1 - 1) of remaining stack [ 1, [ 2, [ ] ] ] to 4 with visited : [ 0, [ ] ] = [ 0, [ 4, [ 2, [ ] ] ] ], then set index 1 of remaining stack [ 0, [ 1, [ 2, [ ] ] ] ] to 4 with visited : [ ] = [ 0, [ 4, [ 2, [ ] ] ] ] (Transitive Property of Equality)
10	result of storing 4 at index 1 of stack [ 0, [ 1, [ 2, [ ] ] ] ] = [ 0, [ 4, [ 2, [ ] ] ] ]	if result of storing 4 at index 1 of stack [ 0, [ 1, [ 2, [ ] ] ] ] = set index 1 of remaining stack [ 0, [ 1, [ 2, [ ] ] ] ] to 4 with visited : [ ] and set index 1 of remaining stack [ 0, [ 1, [ 2, [ ] ] ] ] to 4 with visited : [ ] = [ 0, [ 4, [ 2, [ ] ] ] ], then result of storing 4 at index 1 of stack [ 0, [ 1, [ 2, [ ] ] ] ] = [ 0, [ 4, [ 2, [ ] ] ] ] (Transitive Property of Equality)

Comments

Please log in to add comments