Description: One way to prove that an algorithm halts is to construct a countdown function C : S --> NN0 whose value is guaranteed to decrease for each iteration of F until it reaches 0 . That is, if X e. S is not a fixed point of F , then ( C( FX ) ) < ( CX ) .
If C is a countdown function for algorithm F , the sequence ( C( Rk ) ) reaches 0 after at most N steps, where N is the value of C for the initial state A . (Contributed by Paul Chapman, 22-Jun-2011)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | algcvg.1 | ⊢ 𝐹 : 𝑆 ⟶ 𝑆 | |
| algcvg.2 | ⊢ 𝑅 = seq 0 ( ( 𝐹 ∘ 1st ) , ( ℕ0 × { 𝐴 } ) ) | ||
| algcvg.3 | ⊢ 𝐶 : 𝑆 ⟶ ℕ0 | ||
| algcvg.4 | ⊢ ( 𝑧 ∈ 𝑆 → ( ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) < ( 𝐶 ‘ 𝑧 ) ) ) | ||
| algcvg.5 | ⊢ 𝑁 = ( 𝐶 ‘ 𝐴 ) | ||
| Assertion | algcvg | ⊢ ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝑁 ) ) = 0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | algcvg.1 | ⊢ 𝐹 : 𝑆 ⟶ 𝑆 | |
| 2 | algcvg.2 | ⊢ 𝑅 = seq 0 ( ( 𝐹 ∘ 1st ) , ( ℕ0 × { 𝐴 } ) ) | |
| 3 | algcvg.3 | ⊢ 𝐶 : 𝑆 ⟶ ℕ0 | |
| 4 | algcvg.4 | ⊢ ( 𝑧 ∈ 𝑆 → ( ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) < ( 𝐶 ‘ 𝑧 ) ) ) | |
| 5 | algcvg.5 | ⊢ 𝑁 = ( 𝐶 ‘ 𝐴 ) | |
| 6 | nn0uz | ⊢ ℕ0 = ( ℤ≥ ‘ 0 ) | |
| 7 | 0zd | ⊢ ( 𝐴 ∈ 𝑆 → 0 ∈ ℤ ) | |
| 8 | id | ⊢ ( 𝐴 ∈ 𝑆 → 𝐴 ∈ 𝑆 ) | |
| 9 | 1 | a1i | ⊢ ( 𝐴 ∈ 𝑆 → 𝐹 : 𝑆 ⟶ 𝑆 ) |
| 10 | 6 2 7 8 9 | algrf | ⊢ ( 𝐴 ∈ 𝑆 → 𝑅 : ℕ0 ⟶ 𝑆 ) |
| 11 | 3 | ffvelcdmi | ⊢ ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ 𝐴 ) ∈ ℕ0 ) |
| 12 | 5 11 | eqeltrid | ⊢ ( 𝐴 ∈ 𝑆 → 𝑁 ∈ ℕ0 ) |
| 13 | fvco3 | ⊢ ( ( 𝑅 : ℕ0 ⟶ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐶 ∘ 𝑅 ) ‘ 𝑁 ) = ( 𝐶 ‘ ( 𝑅 ‘ 𝑁 ) ) ) | |
| 14 | 10 12 13 | syl2anc | ⊢ ( 𝐴 ∈ 𝑆 → ( ( 𝐶 ∘ 𝑅 ) ‘ 𝑁 ) = ( 𝐶 ‘ ( 𝑅 ‘ 𝑁 ) ) ) |
| 15 | fco | ⊢ ( ( 𝐶 : 𝑆 ⟶ ℕ0 ∧ 𝑅 : ℕ0 ⟶ 𝑆 ) → ( 𝐶 ∘ 𝑅 ) : ℕ0 ⟶ ℕ0 ) | |
| 16 | 3 10 15 | sylancr | ⊢ ( 𝐴 ∈ 𝑆 → ( 𝐶 ∘ 𝑅 ) : ℕ0 ⟶ ℕ0 ) |
| 17 | 0nn0 | ⊢ 0 ∈ ℕ0 | |
| 18 | fvco3 | ⊢ ( ( 𝑅 : ℕ0 ⟶ 𝑆 ∧ 0 ∈ ℕ0 ) → ( ( 𝐶 ∘ 𝑅 ) ‘ 0 ) = ( 𝐶 ‘ ( 𝑅 ‘ 0 ) ) ) | |
| 19 | 10 17 18 | sylancl | ⊢ ( 𝐴 ∈ 𝑆 → ( ( 𝐶 ∘ 𝑅 ) ‘ 0 ) = ( 𝐶 ‘ ( 𝑅 ‘ 0 ) ) ) |
| 20 | 6 2 7 8 | algr0 | ⊢ ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ 0 ) = 𝐴 ) |
| 21 | 20 | fveq2d | ⊢ ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 0 ) ) = ( 𝐶 ‘ 𝐴 ) ) |
| 22 | 19 21 | eqtrd | ⊢ ( 𝐴 ∈ 𝑆 → ( ( 𝐶 ∘ 𝑅 ) ‘ 0 ) = ( 𝐶 ‘ 𝐴 ) ) |
| 23 | 5 22 | eqtr4id | ⊢ ( 𝐴 ∈ 𝑆 → 𝑁 = ( ( 𝐶 ∘ 𝑅 ) ‘ 0 ) ) |
| 24 | 10 | ffvelcdmda | ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑅 ‘ 𝑘 ) ∈ 𝑆 ) |
| 25 | 2fveq3 | ⊢ ( 𝑧 = ( 𝑅 ‘ 𝑘 ) → ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) = ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ) | |
| 26 | 25 | neeq1d | ⊢ ( 𝑧 = ( 𝑅 ‘ 𝑘 ) → ( ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) ≠ 0 ↔ ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ≠ 0 ) ) |
| 27 | fveq2 | ⊢ ( 𝑧 = ( 𝑅 ‘ 𝑘 ) → ( 𝐶 ‘ 𝑧 ) = ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ) | |
| 28 | 25 27 | breq12d | ⊢ ( 𝑧 = ( 𝑅 ‘ 𝑘 ) → ( ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) < ( 𝐶 ‘ 𝑧 ) ↔ ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ) |
| 29 | 26 28 | imbi12d | ⊢ ( 𝑧 = ( 𝑅 ‘ 𝑘 ) → ( ( ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) < ( 𝐶 ‘ 𝑧 ) ) ↔ ( ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ) ) |
| 30 | 29 4 | vtoclga | ⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ 𝑆 → ( ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ) |
| 31 | 24 30 | syl | ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ) |
| 32 | peano2nn0 | ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 ) | |
| 33 | fvco3 | ⊢ ( ( 𝑅 : ℕ0 ⟶ 𝑆 ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( ( 𝐶 ∘ 𝑅 ) ‘ ( 𝑘 + 1 ) ) = ( 𝐶 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) ) | |
| 34 | 10 32 33 | syl2an | ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 ∘ 𝑅 ) ‘ ( 𝑘 + 1 ) ) = ( 𝐶 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) ) |
| 35 | 6 2 7 8 9 | algrp1 | ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑅 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) |
| 36 | 35 | fveq2d | ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) = ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ) |
| 37 | 34 36 | eqtrd | ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 ∘ 𝑅 ) ‘ ( 𝑘 + 1 ) ) = ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ) |
| 38 | 37 | neeq1d | ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 ∘ 𝑅 ) ‘ ( 𝑘 + 1 ) ) ≠ 0 ↔ ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ≠ 0 ) ) |
| 39 | fvco3 | ⊢ ( ( 𝑅 : ℕ0 ⟶ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 ∘ 𝑅 ) ‘ 𝑘 ) = ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ) | |
| 40 | 10 39 | sylan | ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 ∘ 𝑅 ) ‘ 𝑘 ) = ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ) |
| 41 | 37 40 | breq12d | ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 ∘ 𝑅 ) ‘ ( 𝑘 + 1 ) ) < ( ( 𝐶 ∘ 𝑅 ) ‘ 𝑘 ) ↔ ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ) |
| 42 | 31 38 41 | 3imtr4d | ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 ∘ 𝑅 ) ‘ ( 𝑘 + 1 ) ) ≠ 0 → ( ( 𝐶 ∘ 𝑅 ) ‘ ( 𝑘 + 1 ) ) < ( ( 𝐶 ∘ 𝑅 ) ‘ 𝑘 ) ) ) |
| 43 | 16 23 42 | nn0seqcvgd | ⊢ ( 𝐴 ∈ 𝑆 → ( ( 𝐶 ∘ 𝑅 ) ‘ 𝑁 ) = 0 ) |
| 44 | 14 43 | eqtr3d | ⊢ ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝑁 ) ) = 0 ) |