Proof: Pop Index One Element Example

Let's prove the following theorem:

Proof:

Proof Table

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

Comments

Please log in to add comments