algcvgb

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 ⟶ ℕ_{0}$
Assertion	algcvgb	$⊢ X \in S \to ((C (F (X)) \neq 0 \to C (F (X)) < C (X)) \leftrightarrow ((C (X) \neq 0 \to C (F (X)) < C (X)) \land (C (X) = 0 \to C (F (X)) = 0)))$

Proof

Step	Hyp	Ref	Expression
1		algcvgb.1	$⊢ F : S ⟶ S$
2		algcvgb.2	$⊢ C : S ⟶ ℕ_{0}$
3	2	ffvelcdmi	$⊢ X \in S \to C (X) \in ℕ_{0}$
4	1	ffvelcdmi	$⊢ X \in S \to F (X) \in S$
5	2	ffvelcdmi	$⊢ F (X) \in S \to C (F (X)) \in ℕ_{0}$
6	4 5	syl	$⊢ X \in S \to C (F (X)) \in ℕ_{0}$
7		algcvgblem	$⊢ (C (X) \in ℕ_{0} \land C (F (X)) \in ℕ_{0}) \to ((C (F (X)) \neq 0 \to C (F (X)) < C (X)) \leftrightarrow ((C (X) \neq 0 \to C (F (X)) < C (X)) \land (C (X) = 0 \to C (F (X)) = 0)))$
8	3 6 7	syl2anc	$⊢ X \in S \to ((C (F (X)) \neq 0 \to C (F (X)) < C (X)) \leftrightarrow ((C (X) \neq 0 \to C (F (X)) < C (X)) \land (C (X) = 0 \to C (F (X)) = 0)))$

Metamath Proof Explorer

Theorem algcvgb

Proof