Metamath Proof Explorer


Theorem algcvg

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 )

Proof

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 ffvelrni ( 𝐴𝑆 → ( 𝐶𝐴 ) ∈ ℕ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 ffvelrnda ( ( 𝐴𝑆𝑘 ∈ ℕ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 )