ialgcvg - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > ialgcvg		GIF version

Theorem ialgcvg 9887

Description: One way to prove that an algorithm halts is to construct a countdown function 𝐶:𝑆⟶ℕ₀ whose value is guaranteed to decrease for each iteration of 𝐹 until it reaches 0. That is, if 𝑋 ∈ 𝑆 is not a fixed point of 𝐹, then (𝐶‘(𝐹‘𝑋)) < (𝐶‘𝑋).

If 𝐶 is a countdown function for algorithm 𝐹, the sequence (𝐶‘(𝑅‘𝑘)) reaches 0 after at most 𝑁 steps, where 𝑁 is the value of 𝐶 for the initial state 𝐴. (Contributed by Paul Chapman, 22-Jun-2011.)

**Hypotheses**
Ref	Expression
algcvg.1	⊢ 𝐹:𝑆⟶𝑆
algcvg.2	⊢ 𝑅 = seq0((𝐹 ∘ 1^st ), (ℕ₀ × {𝐴}), 𝑆)
algcvg.3	⊢ 𝐶:𝑆⟶ℕ₀
algcvg.4	⊢ (𝑧 ∈ 𝑆 → ((𝐶‘(𝐹‘𝑧)) ≠ 0 → (𝐶‘(𝐹‘𝑧)) < (𝐶‘𝑧)))
algcvg.5	⊢ 𝑁 = (𝐶‘𝐴)
ialgcvg.s	⊢ 𝑆 ∈ 𝑉

**Assertion**
Ref	Expression
ialgcvg	⊢ (𝐴 ∈ 𝑆 → (𝐶‘(𝑅‘𝑁)) = 0)

Distinct variable groups: 𝑧,𝐶 𝑧,𝐹 𝑧,𝑅 𝑧,𝑆 Allowed substitution hints: 𝐴(𝑧) 𝑁(𝑧) 𝑉(𝑧)

Proof of Theorem ialgcvg Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nn0uz 8507	. . . 4 ⊢ ℕ₀ = (ℤ_≥‘0)
2		algcvg.2	. . . 4 ⊢ 𝑅 = seq0((𝐹 ∘ 1^st ), (ℕ₀ × {𝐴}), 𝑆)
3		0zd 8257	. . . 4 ⊢ (𝐴 ∈ 𝑆 → 0 ∈ ℤ)
4		id 19	. . . 4 ⊢ (𝐴 ∈ 𝑆 → 𝐴 ∈ 𝑆)
5		algcvg.1	. . . . 5 ⊢ 𝐹:𝑆⟶𝑆
6	5	a1i 9	. . . 4 ⊢ (𝐴 ∈ 𝑆 → 𝐹:𝑆⟶𝑆)
7		ialgcvg.s	. . . . 5 ⊢ 𝑆 ∈ 𝑉
8	7	a1i 9	. . . 4 ⊢ (𝐴 ∈ 𝑆 → 𝑆 ∈ 𝑉)
9	1, 2, 3, 4, 6, 8	ialgrf 9884	. . 3 ⊢ (𝐴 ∈ 𝑆 → 𝑅:ℕ₀⟶𝑆)
10		algcvg.5	. . . 4 ⊢ 𝑁 = (𝐶‘𝐴)
11		algcvg.3	. . . . 5 ⊢ 𝐶:𝑆⟶ℕ₀
12	11	ffvelrni 5301	. . . 4 ⊢ (𝐴 ∈ 𝑆 → (𝐶‘𝐴) ∈ ℕ₀)
13	10, 12	syl5eqel 2124	. . 3 ⊢ (𝐴 ∈ 𝑆 → 𝑁 ∈ ℕ₀)
14		fvco3 5244	. . 3 ⊢ ((𝑅:ℕ₀⟶𝑆 ∧ 𝑁 ∈ ℕ₀) → ((𝐶 ∘ 𝑅)‘𝑁) = (𝐶‘(𝑅‘𝑁)))
15	9, 13, 14	syl2anc 391	. 2 ⊢ (𝐴 ∈ 𝑆 → ((𝐶 ∘ 𝑅)‘𝑁) = (𝐶‘(𝑅‘𝑁)))
16		fco 5056	. . . 4 ⊢ ((𝐶:𝑆⟶ℕ₀ ∧ 𝑅:ℕ₀⟶𝑆) → (𝐶 ∘ 𝑅):ℕ₀⟶ℕ₀)
17	11, 9, 16	sylancr 393	. . 3 ⊢ (𝐴 ∈ 𝑆 → (𝐶 ∘ 𝑅):ℕ₀⟶ℕ₀)
18		0nn0 8196	. . . . . 6 ⊢ 0 ∈ ℕ₀
19		fvco3 5244	. . . . . 6 ⊢ ((𝑅:ℕ₀⟶𝑆 ∧ 0 ∈ ℕ₀) → ((𝐶 ∘ 𝑅)‘0) = (𝐶‘(𝑅‘0)))
20	9, 18, 19	sylancl 392	. . . . 5 ⊢ (𝐴 ∈ 𝑆 → ((𝐶 ∘ 𝑅)‘0) = (𝐶‘(𝑅‘0)))
21	1, 2, 3, 4, 6, 8	ialgr0 9883	. . . . . 6 ⊢ (𝐴 ∈ 𝑆 → (𝑅‘0) = 𝐴)
22	21	fveq2d 5182	. . . . 5 ⊢ (𝐴 ∈ 𝑆 → (𝐶‘(𝑅‘0)) = (𝐶‘𝐴))
23	20, 22	eqtrd 2072	. . . 4 ⊢ (𝐴 ∈ 𝑆 → ((𝐶 ∘ 𝑅)‘0) = (𝐶‘𝐴))
24	23, 10	syl6reqr 2091	. . 3 ⊢ (𝐴 ∈ 𝑆 → 𝑁 = ((𝐶 ∘ 𝑅)‘0))
25	9	ffvelrnda 5302	. . . . 5 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ₀) → (𝑅‘𝑘) ∈ 𝑆)
26		fveq2 5178	. . . . . . . . 9 ⊢ (𝑧 = (𝑅‘𝑘) → (𝐹‘𝑧) = (𝐹‘(𝑅‘𝑘)))
27	26	fveq2d 5182	. . . . . . . 8 ⊢ (𝑧 = (𝑅‘𝑘) → (𝐶‘(𝐹‘𝑧)) = (𝐶‘(𝐹‘(𝑅‘𝑘))))
28	27	neeq1d 2223	. . . . . . 7 ⊢ (𝑧 = (𝑅‘𝑘) → ((𝐶‘(𝐹‘𝑧)) ≠ 0 ↔ (𝐶‘(𝐹‘(𝑅‘𝑘))) ≠ 0))
29		fveq2 5178	. . . . . . . 8 ⊢ (𝑧 = (𝑅‘𝑘) → (𝐶‘𝑧) = (𝐶‘(𝑅‘𝑘)))
30	27, 29	breq12d 3777	. . . . . . 7 ⊢ (𝑧 = (𝑅‘𝑘) → ((𝐶‘(𝐹‘𝑧)) < (𝐶‘𝑧) ↔ (𝐶‘(𝐹‘(𝑅‘𝑘))) < (𝐶‘(𝑅‘𝑘))))
31	28, 30	imbi12d 223	. . . . . 6 ⊢ (𝑧 = (𝑅‘𝑘) → (((𝐶‘(𝐹‘𝑧)) ≠ 0 → (𝐶‘(𝐹‘𝑧)) < (𝐶‘𝑧)) ↔ ((𝐶‘(𝐹‘(𝑅‘𝑘))) ≠ 0 → (𝐶‘(𝐹‘(𝑅‘𝑘))) < (𝐶‘(𝑅‘𝑘)))))
32		algcvg.4	. . . . . 6 ⊢ (𝑧 ∈ 𝑆 → ((𝐶‘(𝐹‘𝑧)) ≠ 0 → (𝐶‘(𝐹‘𝑧)) < (𝐶‘𝑧)))
33	31, 32	vtoclga 2619	. . . . 5 ⊢ ((𝑅‘𝑘) ∈ 𝑆 → ((𝐶‘(𝐹‘(𝑅‘𝑘))) ≠ 0 → (𝐶‘(𝐹‘(𝑅‘𝑘))) < (𝐶‘(𝑅‘𝑘))))
34	25, 33	syl 14	. . . 4 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ₀) → ((𝐶‘(𝐹‘(𝑅‘𝑘))) ≠ 0 → (𝐶‘(𝐹‘(𝑅‘𝑘))) < (𝐶‘(𝑅‘𝑘))))
35		peano2nn0 8222	. . . . . . 7 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 + 1) ∈ ℕ₀)
36		fvco3 5244	. . . . . . 7 ⊢ ((𝑅:ℕ₀⟶𝑆 ∧ (𝑘 + 1) ∈ ℕ₀) → ((𝐶 ∘ 𝑅)‘(𝑘 + 1)) = (𝐶‘(𝑅‘(𝑘 + 1))))
37	9, 35, 36	syl2an 273	. . . . . 6 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ₀) → ((𝐶 ∘ 𝑅)‘(𝑘 + 1)) = (𝐶‘(𝑅‘(𝑘 + 1))))
38	1, 2, 3, 4, 6, 8	ialgrp1 9885	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ₀) → (𝑅‘(𝑘 + 1)) = (𝐹‘(𝑅‘𝑘)))
39	38	fveq2d 5182	. . . . . 6 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ₀) → (𝐶‘(𝑅‘(𝑘 + 1))) = (𝐶‘(𝐹‘(𝑅‘𝑘))))
40	37, 39	eqtrd 2072	. . . . 5 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ₀) → ((𝐶 ∘ 𝑅)‘(𝑘 + 1)) = (𝐶‘(𝐹‘(𝑅‘𝑘))))
41	40	neeq1d 2223	. . . 4 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ₀) → (((𝐶 ∘ 𝑅)‘(𝑘 + 1)) ≠ 0 ↔ (𝐶‘(𝐹‘(𝑅‘𝑘))) ≠ 0))
42		fvco3 5244	. . . . . 6 ⊢ ((𝑅:ℕ₀⟶𝑆 ∧ 𝑘 ∈ ℕ₀) → ((𝐶 ∘ 𝑅)‘𝑘) = (𝐶‘(𝑅‘𝑘)))
43	9, 42	sylan 267	. . . . 5 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ₀) → ((𝐶 ∘ 𝑅)‘𝑘) = (𝐶‘(𝑅‘𝑘)))
44	40, 43	breq12d 3777	. . . 4 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ₀) → (((𝐶 ∘ 𝑅)‘(𝑘 + 1)) < ((𝐶 ∘ 𝑅)‘𝑘) ↔ (𝐶‘(𝐹‘(𝑅‘𝑘))) < (𝐶‘(𝑅‘𝑘))))
45	34, 41, 44	3imtr4d 192	. . 3 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ₀) → (((𝐶 ∘ 𝑅)‘(𝑘 + 1)) ≠ 0 → ((𝐶 ∘ 𝑅)‘(𝑘 + 1)) < ((𝐶 ∘ 𝑅)‘𝑘)))
46	17, 24, 45	nn0seqcvgd 9880	. 2 ⊢ (𝐴 ∈ 𝑆 → ((𝐶 ∘ 𝑅)‘𝑁) = 0)
47	15, 46	eqtr3d 2074	1 ⊢ (𝐴 ∈ 𝑆 → (𝐶‘(𝑅‘𝑁)) = 0)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 97 = wceq 1243 ∈ wcel 1393 ≠ wne 2204 {csn 3375 class class class wbr 3764 × cxp 4343 ∘ ccom 4349 ⟶wf 4898 ‘cfv 4902 (class class class)co 5512 1^st c1st 5765 0cc0 6889 1c1 6890 + caddc 6892 < clt 7060 ℕ₀cn0 8181 seqcseq 9211

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-13 1404 ax-14 1405 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-coll 3872 ax-sep 3875 ax-nul 3883 ax-pow 3927 ax-pr 3944 ax-un 4170 ax-setind 4262 ax-iinf 4311 ax-cnex 6975 ax-resscn 6976 ax-1cn 6977 ax-1re 6978 ax-icn 6979 ax-addcl 6980 ax-addrcl 6981 ax-mulcl 6982 ax-addcom 6984 ax-addass 6986 ax-distr 6988 ax-i2m1 6989 ax-0id 6992 ax-rnegex 6993 ax-cnre 6995 ax-pre-ltirr 6996 ax-pre-ltwlin 6997 ax-pre-lttrn 6998 ax-pre-apti 6999 ax-pre-ltadd 7000

This theorem depends on definitions: df-bi 110 df-dc 743 df-3or 886 df-3an 887 df-tru 1246 df-fal 1249 df-nf 1350 df-sb 1646 df-eu 1903 df-mo 1904 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-ne 2206 df-nel 2207 df-ral 2311 df-rex 2312 df-reu 2313 df-rab 2315 df-v 2559 df-sbc 2765 df-csb 2853 df-dif 2920 df-un 2922 df-in 2924 df-ss 2931 df-nul 3225 df-pw 3361 df-sn 3381 df-pr 3382 df-op 3384 df-uni 3581 df-int 3616 df-iun 3659 df-br 3765 df-opab 3819 df-mpt 3820 df-tr 3855 df-eprel 4026 df-id 4030 df-po 4033 df-iso 4034 df-iord 4103 df-on 4105 df-suc 4108 df-iom 4314 df-xp 4351 df-rel 4352 df-cnv 4353 df-co 4354 df-dm 4355 df-rn 4356 df-res 4357 df-ima 4358 df-iota 4867 df-fun 4904 df-fn 4905 df-f 4906 df-f1 4907 df-fo 4908 df-f1o 4909 df-fv 4910 df-riota 5468 df-ov 5515 df-oprab 5516 df-mpt2 5517 df-1st 5767 df-2nd 5768 df-recs 5920 df-irdg 5957 df-frec 5978 df-1o 6001 df-2o 6002 df-oadd 6005 df-omul 6006 df-er 6106 df-ec 6108 df-qs 6112 df-ni 6402 df-pli 6403 df-mi 6404 df-lti 6405 df-plpq 6442 df-mpq 6443 df-enq 6445 df-nqqs 6446 df-plqqs 6447 df-mqqs 6448 df-1nqqs 6449 df-rq 6450 df-ltnqqs 6451 df-enq0 6522 df-nq0 6523 df-0nq0 6524 df-plq0 6525 df-mq0 6526 df-inp 6564 df-i1p 6565 df-iplp 6566 df-iltp 6568 df-enr 6811 df-nr 6812 df-ltr 6815 df-0r 6816 df-1r 6817 df-0 6896 df-1 6897 df-r 6899 df-lt 6902 df-pnf 7062 df-mnf 7063 df-xr 7064 df-ltxr 7065 df-le 7066 df-sub 7184 df-neg 7185 df-inn 7915 df-n0 8182 df-z 8246 df-uz 8474 df-iseq 9212

This theorem is referenced by: ialgcvga 9890

W3C validator