Proof: Pop Index Example 3 Extend

Let's prove the following theorem:

Proof:

Proof Table

#	Claim	Reason
1	remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ] = [ x, [ ] ]	remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ] = [ x, [ ] ] (pop_index_example_3)
2	remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] = reverse of (remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ])	remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] = reverse of (remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) (Begin Pop At Index Property)
3	reverse of (remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) = reverse of [ x, [ ] ]	if remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ] = [ x, [ ] ], then reverse of (remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) = reverse of [ x, [ ] ] (Substitution)
4	reverse of [ x, [ ] ] = [ x, [ ] ]	reverse of [ x, [ ] ] = [ x, [ ] ] (reverse_example_general)
5	reverse of (remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) = [ x, [ ] ]	if reverse of (remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) = reverse of [ x, [ ] ] and reverse of [ x, [ ] ] = [ x, [ ] ], then reverse of (remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) = [ x, [ ] ] (Transitive Property of Equality)
6	remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] = [ x, [ ] ]	if remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] = reverse of (remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) and reverse of (remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) = [ x, [ ] ], then remaining elements after [ x, [ y, [ ] ] ] is popped at index [ 1, [ ] ] = [ x, [ ] ] (Transitive Property of Equality)

Comments

Please log in to add comments