Description: Two ways of expressing that C is a countdown function for algorithm F . The first is used in these theorems. The second states the condition more intuitively as a conjunction: if the countdown function's value is currently nonzero, it must decrease at the next step; if it has reached zero, it must remain zero at the next step. (Contributed by Paul Chapman, 31-Mar-2011)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | algcvgb.1 | |- F : S --> S |
|
| algcvgb.2 | |- C : S --> NN0 |
||
| Assertion | algcvgb | |- ( X e. S -> ( ( ( C ` ( F ` X ) ) =/= 0 -> ( C ` ( F ` X ) ) < ( C ` X ) ) <-> ( ( ( C ` X ) =/= 0 -> ( C ` ( F ` X ) ) < ( C ` X ) ) /\ ( ( C ` X ) = 0 -> ( C ` ( F ` X ) ) = 0 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | algcvgb.1 | |- F : S --> S |
|
| 2 | algcvgb.2 | |- C : S --> NN0 |
|
| 3 | 2 | ffvelrni | |- ( X e. S -> ( C ` X ) e. NN0 ) |
| 4 | 1 | ffvelrni | |- ( X e. S -> ( F ` X ) e. S ) |
| 5 | 2 | ffvelrni | |- ( ( F ` X ) e. S -> ( C ` ( F ` X ) ) e. NN0 ) |
| 6 | 4 5 | syl | |- ( X e. S -> ( C ` ( F ` X ) ) e. NN0 ) |
| 7 | algcvgblem | |- ( ( ( C ` X ) e. NN0 /\ ( C ` ( F ` X ) ) e. NN0 ) -> ( ( ( C ` ( F ` X ) ) =/= 0 -> ( C ` ( F ` X ) ) < ( C ` X ) ) <-> ( ( ( C ` X ) =/= 0 -> ( C ` ( F ` X ) ) < ( C ` X ) ) /\ ( ( C ` X ) = 0 -> ( C ` ( F ` X ) ) = 0 ) ) ) ) |
|
| 8 | 3 6 7 | syl2anc | |- ( X e. S -> ( ( ( C ` ( F ` X ) ) =/= 0 -> ( C ` ( F ` X ) ) < ( C ` X ) ) <-> ( ( ( C ` X ) =/= 0 -> ( C ` ( F ` X ) ) < ( C ` X ) ) /\ ( ( C ` X ) = 0 -> ( C ` ( F ` X ) ) = 0 ) ) ) ) |