Proof: List Get Item Example

Let's prove the following theorem:

In this example, we prove that the element at index 2 of list [10, [12, [14,[]]]] is 14.

At each step, we pop an element from the front of the list and at the same time, decrease the index by 1. When the index reaches 0, we have found our element.

For instance, the following:

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

is equal to:

the element at index 1 of stack [ 12, [ 14, [ ] ] ]

which is equal to:

the element at index 0 of stack [ 14, [ ] ]

which is finally equal to 14

Proof:

Proof Table

#	Claim	Reason
1	the element at index 2 of stack [ 10, [ 12, [ 14, [ ] ] ] ] = the element at index (2 - 1) of stack [ 12, [ 14, [ ] ] ]	the element at index 2 of stack [ 10, [ 12, [ 14, [ ] ] ] ] = the element at index (2 - 1) of stack [ 12, [ 14, [ ] ] ] (List Get Item Recursive Property)
2	2 - 1 = 1	2 - 1 = 1 (Fixed Value Statement)
3	the element at index (2 - 1) of stack [ 12, [ 14, [ ] ] ] = the element at index 1 of stack [ 12, [ 14, [ ] ] ]	if 2 - 1 = 1, then the element at index (2 - 1) of stack [ 12, [ 14, [ ] ] ] = the element at index 1 of stack [ 12, [ 14, [ ] ] ] (Substitution)
4	the element at index 2 of stack [ 10, [ 12, [ 14, [ ] ] ] ] = the element at index 1 of stack [ 12, [ 14, [ ] ] ]	if the element at index 2 of stack [ 10, [ 12, [ 14, [ ] ] ] ] = the element at index (2 - 1) of stack [ 12, [ 14, [ ] ] ] and the element at index (2 - 1) of stack [ 12, [ 14, [ ] ] ] = the element at index 1 of stack [ 12, [ 14, [ ] ] ], then the element at index 2 of stack [ 10, [ 12, [ 14, [ ] ] ] ] = the element at index 1 of stack [ 12, [ 14, [ ] ] ] (Transitive Property of Equality)
5	the element at index 1 of stack [ 12, [ 14, [ ] ] ] = the element at index (1 - 1) of stack [ 14, [ ] ]	the element at index 1 of stack [ 12, [ 14, [ ] ] ] = the element at index (1 - 1) of stack [ 14, [ ] ] (List Get Item Recursive Property)
6	1 - 1 = 0	1 - 1 = 0 (Fixed Value Statement)
7	the element at index (1 - 1) of stack [ 14, [ ] ] = the element at index 0 of stack [ 14, [ ] ]	if 1 - 1 = 0, then the element at index (1 - 1) of stack [ 14, [ ] ] = the element at index 0 of stack [ 14, [ ] ] (Substitution)
8	the element at index 1 of stack [ 12, [ 14, [ ] ] ] = the element at index 0 of stack [ 14, [ ] ]	if the element at index 1 of stack [ 12, [ 14, [ ] ] ] = the element at index (1 - 1) of stack [ 14, [ ] ] and the element at index (1 - 1) of stack [ 14, [ ] ] = the element at index 0 of stack [ 14, [ ] ], then the element at index 1 of stack [ 12, [ 14, [ ] ] ] = the element at index 0 of stack [ 14, [ ] ] (Transitive Property of Equality)
9	the element at index 2 of stack [ 10, [ 12, [ 14, [ ] ] ] ] = the element at index 0 of stack [ 14, [ ] ]	if the element at index 2 of stack [ 10, [ 12, [ 14, [ ] ] ] ] = the element at index 1 of stack [ 12, [ 14, [ ] ] ] and the element at index 1 of stack [ 12, [ 14, [ ] ] ] = the element at index 0 of stack [ 14, [ ] ], then the element at index 2 of stack [ 10, [ 12, [ 14, [ ] ] ] ] = the element at index 0 of stack [ 14, [ ] ] (Transitive Property of Equality)
10	the element at index 0 of stack [ 14, [ ] ] = 14	the element at index 0 of stack [ 14, [ ] ] = 14 (Stack Item At Index Base Property)
11	the element at index 2 of stack [ 10, [ 12, [ 14, [ ] ] ] ] = 14	if the element at index 2 of stack [ 10, [ 12, [ 14, [ ] ] ] ] = the element at index 0 of stack [ 14, [ ] ] and the element at index 0 of stack [ 14, [ ] ] = 14, then the element at index 2 of stack [ 10, [ 12, [ 14, [ ] ] ] ] = 14 (Transitive Property of Equality)

Comments

Please log in to add comments