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 = seq 0 F 1 st 0 × A
algcvg.3 C : S 0
algcvg.4 z S C F z 0 C F z < C z
algcvg.5 N = C A
Assertion algcvg A S C R N = 0

Proof

Step Hyp Ref Expression
1 algcvg.1 F : S S
2 algcvg.2 R = seq 0 F 1 st 0 × A
3 algcvg.3 C : S 0
4 algcvg.4 z S C F z 0 C F z < C z
5 algcvg.5 N = C A
6 nn0uz 0 = 0
7 0zd A S 0
8 id A S A S
9 1 a1i A S F : S S
10 6 2 7 8 9 algrf A S R : 0 S
11 3 ffvelrni A S C A 0
12 5 11 eqeltrid A S N 0
13 fvco3 R : 0 S N 0 C R N = C R N
14 10 12 13 syl2anc A S C R N = C R N
15 fco C : S 0 R : 0 S C R : 0 0
16 3 10 15 sylancr A S C R : 0 0
17 0nn0 0 0
18 fvco3 R : 0 S 0 0 C R 0 = C R 0
19 10 17 18 sylancl A S C R 0 = C R 0
20 6 2 7 8 algr0 A S R 0 = A
21 20 fveq2d A S C R 0 = C A
22 19 21 eqtrd A S C R 0 = C A
23 5 22 eqtr4id A S N = C R 0
24 10 ffvelrnda A S k 0 R k S
25 2fveq3 z = R k C F z = C F R k
26 25 neeq1d z = R k C F z 0 C F R k 0
27 fveq2 z = R k C z = C R k
28 25 27 breq12d z = R k C F z < C z C F R k < C R k
29 26 28 imbi12d z = R k C F z 0 C F z < C z C F R k 0 C F R k < C R k
30 29 4 vtoclga R k S C F R k 0 C F R k < C R k
31 24 30 syl A S k 0 C F R k 0 C F R k < C R k
32 peano2nn0 k 0 k + 1 0
33 fvco3 R : 0 S k + 1 0 C R k + 1 = C R k + 1
34 10 32 33 syl2an A S k 0 C R k + 1 = C R k + 1
35 6 2 7 8 9 algrp1 A S k 0 R k + 1 = F R k
36 35 fveq2d A S k 0 C R k + 1 = C F R k
37 34 36 eqtrd A S k 0 C R k + 1 = C F R k
38 37 neeq1d A S k 0 C R k + 1 0 C F R k 0
39 fvco3 R : 0 S k 0 C R k = C R k
40 10 39 sylan A S k 0 C R k = C R k
41 37 40 breq12d A S k 0 C R k + 1 < C R k C F R k < C R k
42 31 38 41 3imtr4d A S k 0 C R k + 1 0 C R k + 1 < C R k
43 16 23 42 nn0seqcvgd A S C R N = 0
44 14 43 eqtr3d A S C R N = 0