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 o. 1st ) , ( NN0 X. { A } ) ) |
||
| algcvg.3 | |- C : S --> NN0 |
||
| algcvg.4 | |- ( z e. S -> ( ( C ` ( F ` z ) ) =/= 0 -> ( C ` ( F ` z ) ) < ( C ` z ) ) ) |
||
| algcvg.5 | |- N = ( C ` A ) |
||
| Assertion | algcvg | |- ( A e. S -> ( C ` ( R ` N ) ) = 0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | algcvg.1 | |- F : S --> S |
|
| 2 | algcvg.2 | |- R = seq 0 ( ( F o. 1st ) , ( NN0 X. { A } ) ) |
|
| 3 | algcvg.3 | |- C : S --> NN0 |
|
| 4 | algcvg.4 | |- ( z e. S -> ( ( C ` ( F ` z ) ) =/= 0 -> ( C ` ( F ` z ) ) < ( C ` z ) ) ) |
|
| 5 | algcvg.5 | |- N = ( C ` A ) |
|
| 6 | nn0uz | |- NN0 = ( ZZ>= ` 0 ) |
|
| 7 | 0zd | |- ( A e. S -> 0 e. ZZ ) |
|
| 8 | id | |- ( A e. S -> A e. S ) |
|
| 9 | 1 | a1i | |- ( A e. S -> F : S --> S ) |
| 10 | 6 2 7 8 9 | algrf | |- ( A e. S -> R : NN0 --> S ) |
| 11 | 3 | ffvelrni | |- ( A e. S -> ( C ` A ) e. NN0 ) |
| 12 | 5 11 | eqeltrid | |- ( A e. S -> N e. NN0 ) |
| 13 | fvco3 | |- ( ( R : NN0 --> S /\ N e. NN0 ) -> ( ( C o. R ) ` N ) = ( C ` ( R ` N ) ) ) |
|
| 14 | 10 12 13 | syl2anc | |- ( A e. S -> ( ( C o. R ) ` N ) = ( C ` ( R ` N ) ) ) |
| 15 | fco | |- ( ( C : S --> NN0 /\ R : NN0 --> S ) -> ( C o. R ) : NN0 --> NN0 ) |
|
| 16 | 3 10 15 | sylancr | |- ( A e. S -> ( C o. R ) : NN0 --> NN0 ) |
| 17 | 0nn0 | |- 0 e. NN0 |
|
| 18 | fvco3 | |- ( ( R : NN0 --> S /\ 0 e. NN0 ) -> ( ( C o. R ) ` 0 ) = ( C ` ( R ` 0 ) ) ) |
|
| 19 | 10 17 18 | sylancl | |- ( A e. S -> ( ( C o. R ) ` 0 ) = ( C ` ( R ` 0 ) ) ) |
| 20 | 6 2 7 8 | algr0 | |- ( A e. S -> ( R ` 0 ) = A ) |
| 21 | 20 | fveq2d | |- ( A e. S -> ( C ` ( R ` 0 ) ) = ( C ` A ) ) |
| 22 | 19 21 | eqtrd | |- ( A e. S -> ( ( C o. R ) ` 0 ) = ( C ` A ) ) |
| 23 | 5 22 | eqtr4id | |- ( A e. S -> N = ( ( C o. R ) ` 0 ) ) |
| 24 | 10 | ffvelrnda | |- ( ( A e. S /\ k e. NN0 ) -> ( R ` k ) e. 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 ) e. S -> ( ( C ` ( F ` ( R ` k ) ) ) =/= 0 -> ( C ` ( F ` ( R ` k ) ) ) < ( C ` ( R ` k ) ) ) ) |
| 31 | 24 30 | syl | |- ( ( A e. S /\ k e. NN0 ) -> ( ( C ` ( F ` ( R ` k ) ) ) =/= 0 -> ( C ` ( F ` ( R ` k ) ) ) < ( C ` ( R ` k ) ) ) ) |
| 32 | peano2nn0 | |- ( k e. NN0 -> ( k + 1 ) e. NN0 ) |
|
| 33 | fvco3 | |- ( ( R : NN0 --> S /\ ( k + 1 ) e. NN0 ) -> ( ( C o. R ) ` ( k + 1 ) ) = ( C ` ( R ` ( k + 1 ) ) ) ) |
|
| 34 | 10 32 33 | syl2an | |- ( ( A e. S /\ k e. NN0 ) -> ( ( C o. R ) ` ( k + 1 ) ) = ( C ` ( R ` ( k + 1 ) ) ) ) |
| 35 | 6 2 7 8 9 | algrp1 | |- ( ( A e. S /\ k e. NN0 ) -> ( R ` ( k + 1 ) ) = ( F ` ( R ` k ) ) ) |
| 36 | 35 | fveq2d | |- ( ( A e. S /\ k e. NN0 ) -> ( C ` ( R ` ( k + 1 ) ) ) = ( C ` ( F ` ( R ` k ) ) ) ) |
| 37 | 34 36 | eqtrd | |- ( ( A e. S /\ k e. NN0 ) -> ( ( C o. R ) ` ( k + 1 ) ) = ( C ` ( F ` ( R ` k ) ) ) ) |
| 38 | 37 | neeq1d | |- ( ( A e. S /\ k e. NN0 ) -> ( ( ( C o. R ) ` ( k + 1 ) ) =/= 0 <-> ( C ` ( F ` ( R ` k ) ) ) =/= 0 ) ) |
| 39 | fvco3 | |- ( ( R : NN0 --> S /\ k e. NN0 ) -> ( ( C o. R ) ` k ) = ( C ` ( R ` k ) ) ) |
|
| 40 | 10 39 | sylan | |- ( ( A e. S /\ k e. NN0 ) -> ( ( C o. R ) ` k ) = ( C ` ( R ` k ) ) ) |
| 41 | 37 40 | breq12d | |- ( ( A e. S /\ k e. NN0 ) -> ( ( ( C o. R ) ` ( k + 1 ) ) < ( ( C o. R ) ` k ) <-> ( C ` ( F ` ( R ` k ) ) ) < ( C ` ( R ` k ) ) ) ) |
| 42 | 31 38 41 | 3imtr4d | |- ( ( A e. S /\ k e. NN0 ) -> ( ( ( C o. R ) ` ( k + 1 ) ) =/= 0 -> ( ( C o. R ) ` ( k + 1 ) ) < ( ( C o. R ) ` k ) ) ) |
| 43 | 16 23 42 | nn0seqcvgd | |- ( A e. S -> ( ( C o. R ) ` N ) = 0 ) |
| 44 | 14 43 | eqtr3d | |- ( A e. S -> ( C ` ( R ` N ) ) = 0 ) |