Proof: List Length Example

Let's prove the following theorem:

length of stack [ 10, [ 12, [ 14, [ ] ] ] ] = 3

In this example, we prove that the length of the list [10, [12, [14,[]]]] is 3.

At each step, we pop an element from the front of the list and at the same time, increase the count by 1 (the count starts at 0). When the list is empty, we are done counting.

For instance, the following:

length of remaining stack [ 10, [ 12, [ 14, [ ] ] ] ] with count 0

is equal to:

length of remaining stack [ 12, [ 14, [ ] ] ] with count 1

which is equal to:

length of remaining stack [ 14, [ ] ] with count 2

which is equal to:

length of remaining stack [ ] with count 3

which is finally equal to 3

Proof:

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

Proof Table
# Claim Reason
1 length of stack [ 10, [ 12, [ 14, [ ] ] ] ] = length of remaining stack [ 10, [ 12, [ 14, [ ] ] ] ] with count 0 length of stack [ 10, [ 12, [ 14, [ ] ] ] ] = length of remaining stack [ 10, [ 12, [ 14, [ ] ] ] ] with count 0
2 length of remaining stack [ 10, [ 12, [ 14, [ ] ] ] ] with count 0 = length of remaining stack [ 12, [ 14, [ ] ] ] with count (0 + 1) length of remaining stack [ 10, [ 12, [ 14, [ ] ] ] ] with count 0 = length of remaining stack [ 12, [ 14, [ ] ] ] with count (0 + 1)
3 0 + 1 = 1 0 + 1 = 1
4 length of remaining stack [ 12, [ 14, [ ] ] ] with count (0 + 1) = length of remaining stack [ 12, [ 14, [ ] ] ] with count 1 if 0 + 1 = 1, then length of remaining stack [ 12, [ 14, [ ] ] ] with count (0 + 1) = length of remaining stack [ 12, [ 14, [ ] ] ] with count 1
5 length of remaining stack [ 12, [ 14, [ ] ] ] with count 1 = length of remaining stack [ 14, [ ] ] with count (1 + 1) length of remaining stack [ 12, [ 14, [ ] ] ] with count 1 = length of remaining stack [ 14, [ ] ] with count (1 + 1)
6 1 + 1 = 2 1 + 1 = 2
7 length of remaining stack [ 14, [ ] ] with count (1 + 1) = length of remaining stack [ 14, [ ] ] with count 2 if 1 + 1 = 2, then length of remaining stack [ 14, [ ] ] with count (1 + 1) = length of remaining stack [ 14, [ ] ] with count 2
8 length of remaining stack [ 14, [ ] ] with count 2 = length of remaining stack [ ] with count (2 + 1) length of remaining stack [ 14, [ ] ] with count 2 = length of remaining stack [ ] with count (2 + 1)
9 2 + 1 = 3 2 + 1 = 3
10 length of remaining stack [ ] with count (2 + 1) = length of remaining stack [ ] with count 3 if 2 + 1 = 3, then length of remaining stack [ ] with count (2 + 1) = length of remaining stack [ ] with count 3
11 length of remaining stack [ ] with count 3 = 3 length of remaining stack [ ] with count 3 = 3
12 length of remaining stack [ ] with count (2 + 1) = 3 if length of remaining stack [ ] with count (2 + 1) = length of remaining stack [ ] with count 3 and length of remaining stack [ ] with count 3 = 3, then length of remaining stack [ ] with count (2 + 1) = 3
13 length of remaining stack [ 14, [ ] ] with count 2 = 3 if length of remaining stack [ 14, [ ] ] with count 2 = length of remaining stack [ ] with count (2 + 1) and length of remaining stack [ ] with count (2 + 1) = 3, then length of remaining stack [ 14, [ ] ] with count 2 = 3
14 length of remaining stack [ 14, [ ] ] with count (1 + 1) = 3 if length of remaining stack [ 14, [ ] ] with count (1 + 1) = length of remaining stack [ 14, [ ] ] with count 2 and length of remaining stack [ 14, [ ] ] with count 2 = 3, then length of remaining stack [ 14, [ ] ] with count (1 + 1) = 3
15 length of remaining stack [ 12, [ 14, [ ] ] ] with count 1 = 3 if length of remaining stack [ 12, [ 14, [ ] ] ] with count 1 = length of remaining stack [ 14, [ ] ] with count (1 + 1) and length of remaining stack [ 14, [ ] ] with count (1 + 1) = 3, then length of remaining stack [ 12, [ 14, [ ] ] ] with count 1 = 3
16 length of remaining stack [ 12, [ 14, [ ] ] ] with count (0 + 1) = 3 if length of remaining stack [ 12, [ 14, [ ] ] ] with count (0 + 1) = length of remaining stack [ 12, [ 14, [ ] ] ] with count 1 and length of remaining stack [ 12, [ 14, [ ] ] ] with count 1 = 3, then length of remaining stack [ 12, [ 14, [ ] ] ] with count (0 + 1) = 3
17 length of remaining stack [ 10, [ 12, [ 14, [ ] ] ] ] with count 0 = 3 if length of remaining stack [ 10, [ 12, [ 14, [ ] ] ] ] with count 0 = length of remaining stack [ 12, [ 14, [ ] ] ] with count (0 + 1) and length of remaining stack [ 12, [ 14, [ ] ] ] with count (0 + 1) = 3, then length of remaining stack [ 10, [ 12, [ 14, [ ] ] ] ] with count 0 = 3
18 length of stack [ 10, [ 12, [ 14, [ ] ] ] ] = 3 if length of stack [ 10, [ 12, [ 14, [ ] ] ] ] = length of remaining stack [ 10, [ 12, [ 14, [ ] ] ] ] with count 0 and length of remaining stack [ 10, [ 12, [ 14, [ ] ] ] ] with count 0 = 3, then length of stack [ 10, [ 12, [ 14, [ ] ] ] ] = 3

Comments

Please log in to add comments