# 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 ${⊢}{F}:{S}⟶{S}$
algcvg.2 ${⊢}{R}=seq0\left(\left({F}\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{A}\right\}\right)\right)$
algcvg.3 ${⊢}{C}:{S}⟶{ℕ}_{0}$
algcvg.4 ${⊢}{z}\in {S}\to \left({C}\left({F}\left({z}\right)\right)\ne 0\to {C}\left({F}\left({z}\right)\right)<{C}\left({z}\right)\right)$
algcvg.5 ${⊢}{N}={C}\left({A}\right)$
Assertion algcvg ${⊢}{A}\in {S}\to {C}\left({R}\left({N}\right)\right)=0$

### Proof

Step Hyp Ref Expression
1 algcvg.1 ${⊢}{F}:{S}⟶{S}$
2 algcvg.2 ${⊢}{R}=seq0\left(\left({F}\circ {1}^{st}\right),\left({ℕ}_{0}×\left\{{A}\right\}\right)\right)$
3 algcvg.3 ${⊢}{C}:{S}⟶{ℕ}_{0}$
4 algcvg.4 ${⊢}{z}\in {S}\to \left({C}\left({F}\left({z}\right)\right)\ne 0\to {C}\left({F}\left({z}\right)\right)<{C}\left({z}\right)\right)$
5 algcvg.5 ${⊢}{N}={C}\left({A}\right)$
6 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
7 0zd ${⊢}{A}\in {S}\to 0\in ℤ$
8 id ${⊢}{A}\in {S}\to {A}\in {S}$
9 1 a1i ${⊢}{A}\in {S}\to {F}:{S}⟶{S}$
10 6 2 7 8 9 algrf ${⊢}{A}\in {S}\to {R}:{ℕ}_{0}⟶{S}$
11 3 ffvelrni ${⊢}{A}\in {S}\to {C}\left({A}\right)\in {ℕ}_{0}$
12 5 11 eqeltrid ${⊢}{A}\in {S}\to {N}\in {ℕ}_{0}$
13 fvco3 ${⊢}\left({R}:{ℕ}_{0}⟶{S}\wedge {N}\in {ℕ}_{0}\right)\to \left({C}\circ {R}\right)\left({N}\right)={C}\left({R}\left({N}\right)\right)$
14 10 12 13 syl2anc ${⊢}{A}\in {S}\to \left({C}\circ {R}\right)\left({N}\right)={C}\left({R}\left({N}\right)\right)$
15 fco ${⊢}\left({C}:{S}⟶{ℕ}_{0}\wedge {R}:{ℕ}_{0}⟶{S}\right)\to \left({C}\circ {R}\right):{ℕ}_{0}⟶{ℕ}_{0}$
16 3 10 15 sylancr ${⊢}{A}\in {S}\to \left({C}\circ {R}\right):{ℕ}_{0}⟶{ℕ}_{0}$
17 0nn0 ${⊢}0\in {ℕ}_{0}$
18 fvco3 ${⊢}\left({R}:{ℕ}_{0}⟶{S}\wedge 0\in {ℕ}_{0}\right)\to \left({C}\circ {R}\right)\left(0\right)={C}\left({R}\left(0\right)\right)$
19 10 17 18 sylancl ${⊢}{A}\in {S}\to \left({C}\circ {R}\right)\left(0\right)={C}\left({R}\left(0\right)\right)$
20 6 2 7 8 algr0 ${⊢}{A}\in {S}\to {R}\left(0\right)={A}$
21 20 fveq2d ${⊢}{A}\in {S}\to {C}\left({R}\left(0\right)\right)={C}\left({A}\right)$
22 19 21 eqtrd ${⊢}{A}\in {S}\to \left({C}\circ {R}\right)\left(0\right)={C}\left({A}\right)$
23 22 5 syl6reqr ${⊢}{A}\in {S}\to {N}=\left({C}\circ {R}\right)\left(0\right)$
24 10 ffvelrnda ${⊢}\left({A}\in {S}\wedge {k}\in {ℕ}_{0}\right)\to {R}\left({k}\right)\in {S}$
25 2fveq3 ${⊢}{z}={R}\left({k}\right)\to {C}\left({F}\left({z}\right)\right)={C}\left({F}\left({R}\left({k}\right)\right)\right)$
26 25 neeq1d ${⊢}{z}={R}\left({k}\right)\to \left({C}\left({F}\left({z}\right)\right)\ne 0↔{C}\left({F}\left({R}\left({k}\right)\right)\right)\ne 0\right)$
27 fveq2 ${⊢}{z}={R}\left({k}\right)\to {C}\left({z}\right)={C}\left({R}\left({k}\right)\right)$
28 25 27 breq12d ${⊢}{z}={R}\left({k}\right)\to \left({C}\left({F}\left({z}\right)\right)<{C}\left({z}\right)↔{C}\left({F}\left({R}\left({k}\right)\right)\right)<{C}\left({R}\left({k}\right)\right)\right)$
29 26 28 imbi12d ${⊢}{z}={R}\left({k}\right)\to \left(\left({C}\left({F}\left({z}\right)\right)\ne 0\to {C}\left({F}\left({z}\right)\right)<{C}\left({z}\right)\right)↔\left({C}\left({F}\left({R}\left({k}\right)\right)\right)\ne 0\to {C}\left({F}\left({R}\left({k}\right)\right)\right)<{C}\left({R}\left({k}\right)\right)\right)\right)$
30 29 4 vtoclga ${⊢}{R}\left({k}\right)\in {S}\to \left({C}\left({F}\left({R}\left({k}\right)\right)\right)\ne 0\to {C}\left({F}\left({R}\left({k}\right)\right)\right)<{C}\left({R}\left({k}\right)\right)\right)$
31 24 30 syl ${⊢}\left({A}\in {S}\wedge {k}\in {ℕ}_{0}\right)\to \left({C}\left({F}\left({R}\left({k}\right)\right)\right)\ne 0\to {C}\left({F}\left({R}\left({k}\right)\right)\right)<{C}\left({R}\left({k}\right)\right)\right)$
32 peano2nn0 ${⊢}{k}\in {ℕ}_{0}\to {k}+1\in {ℕ}_{0}$
33 fvco3 ${⊢}\left({R}:{ℕ}_{0}⟶{S}\wedge {k}+1\in {ℕ}_{0}\right)\to \left({C}\circ {R}\right)\left({k}+1\right)={C}\left({R}\left({k}+1\right)\right)$
34 10 32 33 syl2an ${⊢}\left({A}\in {S}\wedge {k}\in {ℕ}_{0}\right)\to \left({C}\circ {R}\right)\left({k}+1\right)={C}\left({R}\left({k}+1\right)\right)$
35 6 2 7 8 9 algrp1 ${⊢}\left({A}\in {S}\wedge {k}\in {ℕ}_{0}\right)\to {R}\left({k}+1\right)={F}\left({R}\left({k}\right)\right)$
36 35 fveq2d ${⊢}\left({A}\in {S}\wedge {k}\in {ℕ}_{0}\right)\to {C}\left({R}\left({k}+1\right)\right)={C}\left({F}\left({R}\left({k}\right)\right)\right)$
37 34 36 eqtrd ${⊢}\left({A}\in {S}\wedge {k}\in {ℕ}_{0}\right)\to \left({C}\circ {R}\right)\left({k}+1\right)={C}\left({F}\left({R}\left({k}\right)\right)\right)$
38 37 neeq1d ${⊢}\left({A}\in {S}\wedge {k}\in {ℕ}_{0}\right)\to \left(\left({C}\circ {R}\right)\left({k}+1\right)\ne 0↔{C}\left({F}\left({R}\left({k}\right)\right)\right)\ne 0\right)$
39 fvco3 ${⊢}\left({R}:{ℕ}_{0}⟶{S}\wedge {k}\in {ℕ}_{0}\right)\to \left({C}\circ {R}\right)\left({k}\right)={C}\left({R}\left({k}\right)\right)$
40 10 39 sylan ${⊢}\left({A}\in {S}\wedge {k}\in {ℕ}_{0}\right)\to \left({C}\circ {R}\right)\left({k}\right)={C}\left({R}\left({k}\right)\right)$
41 37 40 breq12d ${⊢}\left({A}\in {S}\wedge {k}\in {ℕ}_{0}\right)\to \left(\left({C}\circ {R}\right)\left({k}+1\right)<\left({C}\circ {R}\right)\left({k}\right)↔{C}\left({F}\left({R}\left({k}\right)\right)\right)<{C}\left({R}\left({k}\right)\right)\right)$
42 31 38 41 3imtr4d ${⊢}\left({A}\in {S}\wedge {k}\in {ℕ}_{0}\right)\to \left(\left({C}\circ {R}\right)\left({k}+1\right)\ne 0\to \left({C}\circ {R}\right)\left({k}+1\right)<\left({C}\circ {R}\right)\left({k}\right)\right)$
43 16 23 42 nn0seqcvgd ${⊢}{A}\in {S}\to \left({C}\circ {R}\right)\left({N}\right)=0$
44 14 43 eqtr3d ${⊢}{A}\in {S}\to {C}\left({R}\left({N}\right)\right)=0$