Proof: Pop Index Example

Let's prove the following theorem:

remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ] = [ [ 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, [ ] ] and visited stack is [ ] = remaining elements after [ [ 1, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ [ 0, [ ] ], [ ] ] remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ] = remaining elements after [ [ 1, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ [ 0, [ ] ], [ ] ]
2 remaining elements after [ [ 1, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ [ 0, [ ] ], [ ] ] = result of dumping [ ] to [ [ 0, [ ] ], [ ] ] remaining elements after [ [ 1, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ [ 0, [ ] ], [ ] ] = result of dumping [ ] to [ [ 0, [ ] ], [ ] ]
3 result of dumping [ ] to [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ] result of dumping [ ] to [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ]
4 remaining elements after [ [ 1, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ] if remaining elements after [ [ 1, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ [ 0, [ ] ], [ ] ] = result of dumping [ ] to [ [ 0, [ ] ], [ ] ] and result of dumping [ ] to [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ], then remaining elements after [ [ 1, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ]
5 remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ] = [ [ 0, [ ] ], [ ] ] if remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ] = remaining elements after [ [ 1, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ [ 0, [ ] ], [ ] ] and remaining elements after [ [ 1, [ ] ], [ ] ] is popped at index [ 0, [ ] ] and visited stack is [ [ 0, [ ] ], [ ] ] = [ [ 0, [ ] ], [ ] ], then remaining elements after [ [ 0, [ ] ], [ [ 1, [ ] ], [ ] ] ] is popped at index [ 1, [ ] ] and visited stack is [ ] = [ [ 0, [ ] ], [ ] ]

Comments

Please log in to add comments