Proof: Pop At Example

Let's prove the following theorem:

Proof:

Proof Table

#	Claim	Reason
1	stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 = reverse of (stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 in traversed elements: [ ])	stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 = reverse of (stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 in traversed elements: [ ]) (Pop At List)
2	stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 in traversed elements: [ ] = stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index (1 - 1) in traversed elements: [ 10, [ ] ]	stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 in traversed elements: [ ] = stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index (1 - 1) in traversed elements: [ 10, [ ] ] (Pop At List 2)
3	1 - 1 = 0	1 - 1 = 0 (Fixed Value Statement)
4	stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index (1 - 1) in traversed elements: [ 10, [ ] ] = stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index 0 in traversed elements: [ 10, [ ] ]	if 1 - 1 = 0, then stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index (1 - 1) in traversed elements: [ 10, [ ] ] = stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index 0 in traversed elements: [ 10, [ ] ] (Substitution)
5	stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index 0 in traversed elements: [ 10, [ ] ] = result of dumping [ 14, [ ] ] to [ 10, [ ] ]	stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index 0 in traversed elements: [ 10, [ ] ] = result of dumping [ 14, [ ] ] to [ 10, [ ] ] (Pop At List End)
6	result of dumping [ 14, [ ] ] to [ 10, [ ] ] = [ 14, [ 10, [ ] ] ]	result of dumping [ 14, [ ] ] to [ 10, [ ] ] = [ 14, [ 10, [ ] ] ] (Pre-extend (2))
7	stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index 0 in traversed elements: [ 10, [ ] ] = [ 14, [ 10, [ ] ] ]	if stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index 0 in traversed elements: [ 10, [ ] ] = result of dumping [ 14, [ ] ] to [ 10, [ ] ] and result of dumping [ 14, [ ] ] to [ 10, [ ] ] = [ 14, [ 10, [ ] ] ], then stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index 0 in traversed elements: [ 10, [ ] ] = [ 14, [ 10, [ ] ] ] (Transitive Property of Equality)
8	stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index (1 - 1) in traversed elements: [ 10, [ ] ] = [ 14, [ 10, [ ] ] ]	if stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index (1 - 1) in traversed elements: [ 10, [ ] ] = stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index 0 in traversed elements: [ 10, [ ] ] and stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index 0 in traversed elements: [ 10, [ ] ] = [ 14, [ 10, [ ] ] ], then stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index (1 - 1) in traversed elements: [ 10, [ ] ] = [ 14, [ 10, [ ] ] ] (Transitive Property of Equality)
9	stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 in traversed elements: [ ] = [ 14, [ 10, [ ] ] ]	if stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 in traversed elements: [ ] = stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index (1 - 1) in traversed elements: [ 10, [ ] ] and stack after popping a value from stack [ 12, [ 14, [ ] ] ] at index (1 - 1) in traversed elements: [ 10, [ ] ] = [ 14, [ 10, [ ] ] ], then stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 in traversed elements: [ ] = [ 14, [ 10, [ ] ] ] (Transitive Property of Equality)
10	reverse of (stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 in traversed elements: [ ]) = reverse of [ 14, [ 10, [ ] ] ]	if stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 in traversed elements: [ ] = [ 14, [ 10, [ ] ] ], then reverse of (stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 in traversed elements: [ ]) = reverse of [ 14, [ 10, [ ] ] ] (Substitution)
11	stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 = reverse of [ 14, [ 10, [ ] ] ]	if stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 = reverse of (stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 in traversed elements: [ ]) and reverse of (stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 in traversed elements: [ ]) = reverse of [ 14, [ 10, [ ] ] ], then stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 = reverse of [ 14, [ 10, [ ] ] ] (Transitive Property of Equality)
12	reverse of [ 14, [ 10, [ ] ] ] = [ 10, [ 14, [ ] ] ]	reverse of [ 14, [ 10, [ ] ] ] = [ 10, [ 14, [ ] ] ] (reverse_list_two_example)
13	stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 = [ 10, [ 14, [ ] ] ]	if stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 = reverse of [ 14, [ 10, [ ] ] ] and reverse of [ 14, [ 10, [ ] ] ] = [ 10, [ 14, [ ] ] ], then stack after popping a value from stack [ 10, [ 12, [ 14, [ ] ] ] ] at index 1 = [ 10, [ 14, [ ] ] ] (Transitive Property of Equality)

Comments

Please log in to add comments