Proof: Pop At Index Induction Example

Let's prove the following theorem:

In this example, we prove that if we pop the following list

[3, [2, [1, []]]]

At index 2, and the "visited" list is empty, the resulting list is

[3, [2, []]]

First, we use the induction step to pop 3, then 2, from the list and add them to the "visited" list. The index is also decremented twice. Then in step 7, we claim that we need to 1) reverse and insert the remaining list to the "visited" list, then 2) reverse the resulting list. Since the remaining list is empty, we really just need to reverse the "visited" list.

And in the remaining steps, we use the Transitive Property to reach the conclusion.

Proof:

Proof Table

#	Claim	Reason
1	remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 and visited stack is [ ] = remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (2 - 1) and visited stack is [ 3, [ ] ]	remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 and visited stack is [ ] = remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (2 - 1) and visited stack is [ 3, [ ] ] (Pop At Index Induction Step)
2	2 - 1 = 1	2 - 1 = 1 (Fixed Value Statement)
3	remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (2 - 1) and visited stack is [ 3, [ ] ] = remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 1 and visited stack is [ 3, [ ] ]	if 2 - 1 = 1, then remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (2 - 1) and visited stack is [ 3, [ ] ] = remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 1 and visited stack is [ 3, [ ] ] (Substitution)
4	remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 1 and visited stack is [ 3, [ ] ] = remaining elements after [ 1, [ ] ] is popped at index (1 - 1) and visited stack is [ 2, [ 3, [ ] ] ]	remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 1 and visited stack is [ 3, [ ] ] = remaining elements after [ 1, [ ] ] is popped at index (1 - 1) and visited stack is [ 2, [ 3, [ ] ] ] (Pop At Index Induction Step)
5	1 - 1 = 0	1 - 1 = 0 (Fixed Value Statement)
6	remaining elements after [ 1, [ ] ] is popped at index (1 - 1) and visited stack is [ 2, [ 3, [ ] ] ] = remaining elements after [ 1, [ ] ] is popped at index 0 and visited stack is [ 2, [ 3, [ ] ] ]	if 1 - 1 = 0, then remaining elements after [ 1, [ ] ] is popped at index (1 - 1) and visited stack is [ 2, [ 3, [ ] ] ] = remaining elements after [ 1, [ ] ] is popped at index 0 and visited stack is [ 2, [ 3, [ ] ] ] (Substitution)
7	remaining elements after [ 1, [ ] ] is popped at index 0 and visited stack is [ 2, [ 3, [ ] ] ] = reverse of (result of dumping [ ] to [ 2, [ 3, [ ] ] ])	remaining elements after [ 1, [ ] ] is popped at index 0 and visited stack is [ 2, [ 3, [ ] ] ] = reverse of (result of dumping [ ] to [ 2, [ 3, [ ] ] ]) (Pop At Index Zero Property)
8	result of dumping [ ] to [ 2, [ 3, [ ] ] ] = [ 2, [ 3, [ ] ] ]	result of dumping [ ] to [ 2, [ 3, [ ] ] ] = [ 2, [ 3, [ ] ] ] (Pre-extend (3))
9	reverse of (result of dumping [ ] to [ 2, [ 3, [ ] ] ]) = reverse of [ 2, [ 3, [ ] ] ]	if result of dumping [ ] to [ 2, [ 3, [ ] ] ] = [ 2, [ 3, [ ] ] ], then reverse of (result of dumping [ ] to [ 2, [ 3, [ ] ] ]) = reverse of [ 2, [ 3, [ ] ] ] (Substitution)
10	reverse of [ 2, [ 3, [ ] ] ] = [ 3, [ 2, [ ] ] ]	reverse of [ 2, [ 3, [ ] ] ] = [ 3, [ 2, [ ] ] ] (reverse_list_two_example)
11	reverse of (result of dumping [ ] to [ 2, [ 3, [ ] ] ]) = [ 3, [ 2, [ ] ] ]	if reverse of (result of dumping [ ] to [ 2, [ 3, [ ] ] ]) = reverse of [ 2, [ 3, [ ] ] ] and reverse of [ 2, [ 3, [ ] ] ] = [ 3, [ 2, [ ] ] ], then reverse of (result of dumping [ ] to [ 2, [ 3, [ ] ] ]) = [ 3, [ 2, [ ] ] ] (Transitive Property of Equality)
12	remaining elements after [ 1, [ ] ] is popped at index 0 and visited stack is [ 2, [ 3, [ ] ] ] = [ 3, [ 2, [ ] ] ]	if remaining elements after [ 1, [ ] ] is popped at index 0 and visited stack is [ 2, [ 3, [ ] ] ] = reverse of (result of dumping [ ] to [ 2, [ 3, [ ] ] ]) and reverse of (result of dumping [ ] to [ 2, [ 3, [ ] ] ]) = [ 3, [ 2, [ ] ] ], then remaining elements after [ 1, [ ] ] is popped at index 0 and visited stack is [ 2, [ 3, [ ] ] ] = [ 3, [ 2, [ ] ] ] (Transitive Property of Equality)
13	remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 1 and visited stack is [ 3, [ ] ] = [ 3, [ 2, [ ] ] ]	if remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 1 and visited stack is [ 3, [ ] ] = remaining elements after [ 1, [ ] ] is popped at index (1 - 1) and visited stack is [ 2, [ 3, [ ] ] ] and remaining elements after [ 1, [ ] ] is popped at index (1 - 1) and visited stack is [ 2, [ 3, [ ] ] ] = remaining elements after [ 1, [ ] ] is popped at index 0 and visited stack is [ 2, [ 3, [ ] ] ] and remaining elements after [ 1, [ ] ] is popped at index 0 and visited stack is [ 2, [ 3, [ ] ] ] = [ 3, [ 2, [ ] ] ], then remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 1 and visited stack is [ 3, [ ] ] = [ 3, [ 2, [ ] ] ] (Transitive Property Application 1)
14	remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 and visited stack is [ ] = [ 3, [ 2, [ ] ] ]	if remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 and visited stack is [ ] = remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (2 - 1) and visited stack is [ 3, [ ] ] and remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (2 - 1) and visited stack is [ 3, [ ] ] = remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 1 and visited stack is [ 3, [ ] ] and remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 1 and visited stack is [ 3, [ ] ] = [ 3, [ 2, [ ] ] ], then remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 and visited stack is [ ] = [ 3, [ 2, [ ] ] ] (Transitive Property Application 1)

Comments

Please log in to add comments