Proof: Pop Index Base

Let's prove the following theorem:

Proof:

Proof Table

#	Claim	Reason
1	remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] = reverse of (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ ])	remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] = reverse of (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ ]) (Begin Pop At Index Property)
2	remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ ] = result of dumping [ ] to [ ]	remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ ] = result of dumping [ ] to [ ] (Pop Index (2))
3	result of dumping [ ] to [ ] = [ ]	result of dumping [ ] to [ ] = [ ] (Pre-extend (3))
4	remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ ] = [ ]	if remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ ] = result of dumping [ ] to [ ] and result of dumping [ ] to [ ] = [ ], then remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ ] = [ ] (Transitive Property of Equality)
5	reverse of (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ ]) = reverse of [ ]	if remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ ] = [ ], then reverse of (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ ]) = reverse of [ ] (Substitution)
6	reverse of [ ] = [ ]	reverse of [ ] = [ ] (Reversing an Empty List)
7	reverse of (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ ]) = [ ]	if reverse of (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ ]) = reverse of [ ] and reverse of [ ] = [ ], then reverse of (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ ]) = [ ] (Transitive Property of Equality)
8	remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] = [ ]	if remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] = reverse of (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ ]) and reverse of (remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ ]) = [ ], then remaining elements after [ [ 0, [ ] ], [ ] ] is popped at index [ 0, [ ] ] = [ ] (Transitive Property of Equality)

Comments

Please log in to add comments