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

Proof

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

Metamath Proof Explorer

Theorem algcvg

Proof