Proof: Pop Index Example 2

Let's prove the following theorem:

remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] = [ [ 0, [ ] ], [ ] ]

Proof:

View as a tree | View dependent proofs | Try proving it

Proof Table
# Claim Reason
1 remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] = reverse of (remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] = reverse of (remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ])
2 remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ] = [ [ 0, [ ] ], [ ] ] remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ] = [ [ 0, [ ] ], [ ] ]
3 reverse of (remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) = reverse of [ [ 0, [ ] ], [ ] ] if remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ] = [ [ 0, [ ] ], [ ] ], then reverse of (remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) = reverse of [ [ 0, [ ] ], [ ] ]
4 reverse of [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ] reverse of [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ]
5 reverse of (remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) = [ [ 0, [ ] ], [ ] ] if reverse of (remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) = reverse of [ [ 0, [ ] ], [ ] ] and reverse of [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ], then reverse of (remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) = [ [ 0, [ ] ], [ ] ]
6 remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] = [ [ 0, [ ] ], [ ] ] if remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] = reverse of (remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) and reverse of (remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ]) = [ [ 0, [ ] ], [ ] ], then remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] = [ [ 0, [ ] ], [ ] ]

Comments

Please log in to add comments