Proof: Reverse List Example 3
Let's prove the following theorem:
reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = [ 1, [ 2, [ 3, [ 4, [ ] ] ] ] ]
Proof:
| # | Claim | Reason |
|---|---|---|
| 1 | reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = reverse of remaining stack [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] and already reversed stack [ ] | reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = reverse of remaining stack [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] and already reversed stack [ ] |
| 2 | reverse of remaining stack [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] and already reversed stack [ ] = reverse of remaining stack [ 3, [ 2, [ 1, [ ] ] ] ] and already reversed stack [ 4, [ ] ] | reverse of remaining stack [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] and already reversed stack [ ] = reverse of remaining stack [ 3, [ 2, [ 1, [ ] ] ] ] and already reversed stack [ 4, [ ] ] |
| 3 | reverse of remaining stack [ 3, [ 2, [ 1, [ ] ] ] ] and already reversed stack [ 4, [ ] ] = reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ 4, [ ] ] ] | reverse of remaining stack [ 3, [ 2, [ 1, [ ] ] ] ] and already reversed stack [ 4, [ ] ] = reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ 4, [ ] ] ] |
| 4 | reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ 4, [ ] ] ] = reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ 4, [ ] ] ] ] | reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ 4, [ ] ] ] = reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ 4, [ ] ] ] ] |
| 5 | reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ 4, [ ] ] ] ] = [ 1, [ 2, [ 3, [ 4, [ ] ] ] ] ] | reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ 4, [ ] ] ] ] = [ 1, [ 2, [ 3, [ 4, [ ] ] ] ] ] |
| 6 | reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = reverse of remaining stack [ 3, [ 2, [ 1, [ ] ] ] ] and already reversed stack [ 4, [ ] ] | if reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = reverse of remaining stack [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] and already reversed stack [ ] and reverse of remaining stack [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] and already reversed stack [ ] = reverse of remaining stack [ 3, [ 2, [ 1, [ ] ] ] ] and already reversed stack [ 4, [ ] ], then reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = reverse of remaining stack [ 3, [ 2, [ 1, [ ] ] ] ] and already reversed stack [ 4, [ ] ] |
| 7 | reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ 4, [ ] ] ] | if reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = reverse of remaining stack [ 3, [ 2, [ 1, [ ] ] ] ] and already reversed stack [ 4, [ ] ] and reverse of remaining stack [ 3, [ 2, [ 1, [ ] ] ] ] and already reversed stack [ 4, [ ] ] = reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ 4, [ ] ] ], then reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ 4, [ ] ] ] |
| 8 | reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ 4, [ ] ] ] ] | if reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ 4, [ ] ] ] and reverse of remaining stack [ 2, [ 1, [ ] ] ] and already reversed stack [ 3, [ 4, [ ] ] ] = reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ 4, [ ] ] ] ], then reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ 4, [ ] ] ] ] |
| 9 | reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = [ 1, [ 2, [ 3, [ 4, [ ] ] ] ] ] | if reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ 4, [ ] ] ] ] and reverse of remaining stack [ 1, [ ] ] and already reversed stack [ 2, [ 3, [ 4, [ ] ] ] ] = [ 1, [ 2, [ 3, [ 4, [ ] ] ] ] ], then reverse of [ 4, [ 3, [ 2, [ 1, [ ] ] ] ] ] = [ 1, [ 2, [ 3, [ 4, [ ] ] ] ] ] |
Comments
Please log in to add comments