Proof: Reverse List Example

Let's prove the following theorem:

In this proof, we use the reverse list properties to move elements from the initial list to the result. In each iteration, an element is removed from the front of the initial list and added to the front of the result list. The proof is complete when all elements have moved to the result list.

Proof:

Proof Table

#	Claim	Reason
1	reverse of [ 3, [ 2, [ 1, [ ] ] ] ] = reverse of remaining stack [ 3, [ 2, [ 1, [ ] ] ] ] and already reversed stack [ ]	reverse of [ 3, [ 2, [ 1, [ ] ] ] ] = reverse of remaining stack [ 3, [ 2, [ 1, [ ] ] ] ] and already reversed stack [ ] (Reversing a List Property 1)
2	reverse of remaining stack [ 3, [ 2, [ 1, [ ] ] ] ] and already reversed stack [ ] = reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ ] ]	reverse of remaining stack [ 3, [ 2, [ 1, [ ] ] ] ] and already reversed stack [ ] = reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ ] ] (Reversing a List Property 3)
3	reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ ] ] = reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ ] ] ]	reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ ] ] = reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ ] ] ] (Reversing a List Property 3)
4	reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ]	reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ] (Reversing a List Property 4)
5	reverse of [ 3, [ 2, [ 1, [ ] ] ] ] = reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ ] ]	if reverse of [ 3, [ 2, [ 1, [ ] ] ] ] = reverse of remaining stack [ 3, [ 2, [ 1, [ ] ] ] ] and already reversed stack [ ] and reverse of remaining stack [ 3, [ 2, [ 1, [ ] ] ] ] and already reversed stack [ ] = reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ ] ], then reverse of [ 3, [ 2, [ 1, [ ] ] ] ] = reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ ] ] (Transitive Property of Equality)
6	reverse of [ 3, [ 2, [ 1, [ ] ] ] ] = reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ ] ] ]	if reverse of [ 3, [ 2, [ 1, [ ] ] ] ] = reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ ] ] and reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ ] ] = reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ ] ] ], then reverse of [ 3, [ 2, [ 1, [ ] ] ] ] = reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ ] ] ] (Transitive Property of Equality)
7	reverse of [ 3, [ 2, [ 1, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ]	if reverse of [ 3, [ 2, [ 1, [ ] ] ] ] = reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ ] ] ] and reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ], then reverse of [ 3, [ 2, [ 1, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ] (Transitive Property of Equality)

Comments

Please log in to add comments