Proof: Pop At Index 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, the resulting list is

[3, [2, []]]

We use the "Begin Pop At Index Property" to set things up then rely on "Pop At Index Induction Example" to do most of the actual proof.

Proof:

Proof Table

#	Claim	Reason
1	remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 = remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 and visited stack is [ ]	remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 = remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 and visited stack is [ ] (Begin Pop At Index Property)
2	remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 and visited stack is [ ] = [ 3, [ 2, [ ] ] ]	remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 and visited stack is [ ] = [ 3, [ 2, [ ] ] ] (Pop At Index Induction Example)
3	remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 = [ 3, [ 2, [ ] ] ]	if remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 = remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 and visited stack is [ ] and remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 and visited stack is [ ] = [ 3, [ 2, [ ] ] ], then remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 2 = [ 3, [ 2, [ ] ] ] (Transitive Property of Equality)

Comments

Please log in to add comments