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

Theorem algcvg 12015
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 `  ( F `  X ) )  <  ( C `
 X ).

If  C is a countdown function for algorithm  F, the sequence  ( C `  ( R `  k ) ) 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.)

Hypotheses
Ref Expression
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
Ref Expression
algcvg  |-  ( A  e.  S  ->  ( C `  ( R `  N ) )  =  0 )
Distinct variable groups:    z, C    z, F    z, R    z, S
Allowed substitution hints:    A( z)    N( z)

Proof of Theorem algcvg
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 nn0uz 9535 . . . 4  |-  NN0  =  ( ZZ>= `  0 )
2 algcvg.2 . . . 4  |-  R  =  seq 0 ( ( F  o.  1st ) ,  ( NN0  X.  { A } ) )
3 0zd 9238 . . . 4  |-  ( A  e.  S  ->  0  e.  ZZ )
4 id 19 . . . 4  |-  ( A  e.  S  ->  A  e.  S )
5 algcvg.1 . . . . 5  |-  F : S
--> S
65a1i 9 . . . 4  |-  ( A  e.  S  ->  F : S --> S )
71, 2, 3, 4, 6algrf 12012 . . 3  |-  ( A  e.  S  ->  R : NN0 --> S )
8 algcvg.5 . . . 4  |-  N  =  ( C `  A
)
9 algcvg.3 . . . . 5  |-  C : S
--> NN0
109ffvelcdmi 5642 . . . 4  |-  ( A  e.  S  ->  ( C `  A )  e.  NN0 )
118, 10eqeltrid 2262 . . 3  |-  ( A  e.  S  ->  N  e.  NN0 )
12 fvco3 5579 . . 3  |-  ( ( R : NN0 --> S  /\  N  e.  NN0 )  -> 
( ( C  o.  R ) `  N
)  =  ( C `
 ( R `  N ) ) )
137, 11, 12syl2anc 411 . 2  |-  ( A  e.  S  ->  (
( C  o.  R
) `  N )  =  ( C `  ( R `  N ) ) )
14 fco 5373 . . . 4  |-  ( ( C : S --> NN0  /\  R : NN0 --> S )  ->  ( C  o.  R ) : NN0 --> NN0 )
159, 7, 14sylancr 414 . . 3  |-  ( A  e.  S  ->  ( C  o.  R ) : NN0 --> NN0 )
16 0nn0 9164 . . . . . 6  |-  0  e.  NN0
17 fvco3 5579 . . . . . 6  |-  ( ( R : NN0 --> S  /\  0  e.  NN0 )  -> 
( ( C  o.  R ) `  0
)  =  ( C `
 ( R ` 
0 ) ) )
187, 16, 17sylancl 413 . . . . 5  |-  ( A  e.  S  ->  (
( C  o.  R
) `  0 )  =  ( C `  ( R `  0 ) ) )
191, 2, 3, 4, 6ialgr0 12011 . . . . . 6  |-  ( A  e.  S  ->  ( R `  0 )  =  A )
2019fveq2d 5511 . . . . 5  |-  ( A  e.  S  ->  ( C `  ( R `  0 ) )  =  ( C `  A ) )
2118, 20eqtrd 2208 . . . 4  |-  ( A  e.  S  ->  (
( C  o.  R
) `  0 )  =  ( C `  A ) )
228, 21eqtr4id 2227 . . 3  |-  ( A  e.  S  ->  N  =  ( ( C  o.  R ) ` 
0 ) )
237ffvelcdmda 5643 . . . . 5  |-  ( ( A  e.  S  /\  k  e.  NN0 )  -> 
( R `  k
)  e.  S )
24 2fveq3 5512 . . . . . . . 8  |-  ( z  =  ( R `  k )  ->  ( C `  ( F `  z ) )  =  ( C `  ( F `  ( R `  k ) ) ) )
2524neeq1d 2363 . . . . . . 7  |-  ( z  =  ( R `  k )  ->  (
( C `  ( F `  z )
)  =/=  0  <->  ( C `  ( F `  ( R `  k
) ) )  =/=  0 ) )
26 fveq2 5507 . . . . . . . 8  |-  ( z  =  ( R `  k )  ->  ( C `  z )  =  ( C `  ( R `  k ) ) )
2724, 26breq12d 4011 . . . . . . 7  |-  ( z  =  ( R `  k )  ->  (
( C `  ( F `  z )
)  <  ( C `  z )  <->  ( C `  ( F `  ( R `  k )
) )  <  ( C `  ( R `  k ) ) ) )
2825, 27imbi12d 234 . . . . . 6  |-  ( z  =  ( R `  k )  ->  (
( ( C `  ( F `  z ) )  =/=  0  -> 
( C `  ( F `  z )
)  <  ( C `  z ) )  <->  ( ( C `  ( F `  ( R `  k
) ) )  =/=  0  ->  ( C `  ( F `  ( R `  k )
) )  <  ( C `  ( R `  k ) ) ) ) )
29 algcvg.4 . . . . . 6  |-  ( z  e.  S  ->  (
( C `  ( F `  z )
)  =/=  0  -> 
( C `  ( F `  z )
)  <  ( C `  z ) ) )
3028, 29vtoclga 2801 . . . . 5  |-  ( ( R `  k )  e.  S  ->  (
( C `  ( F `  ( R `  k ) ) )  =/=  0  ->  ( C `  ( F `  ( R `  k
) ) )  < 
( C `  ( R `  k )
) ) )
3123, 30syl 14 . . . 4  |-  ( ( A  e.  S  /\  k  e.  NN0 )  -> 
( ( C `  ( F `  ( R `
 k ) ) )  =/=  0  -> 
( C `  ( F `  ( R `  k ) ) )  <  ( C `  ( R `  k ) ) ) )
32 peano2nn0 9189 . . . . . . 7  |-  ( k  e.  NN0  ->  ( k  +  1 )  e. 
NN0 )
33 fvco3 5579 . . . . . . 7  |-  ( ( R : NN0 --> S  /\  ( k  +  1 )  e.  NN0 )  ->  ( ( C  o.  R ) `  (
k  +  1 ) )  =  ( C `
 ( R `  ( k  +  1 ) ) ) )
347, 32, 33syl2an 289 . . . . . 6  |-  ( ( A  e.  S  /\  k  e.  NN0 )  -> 
( ( C  o.  R ) `  (
k  +  1 ) )  =  ( C `
 ( R `  ( k  +  1 ) ) ) )
351, 2, 3, 4, 6algrp1 12013 . . . . . . 7  |-  ( ( A  e.  S  /\  k  e.  NN0 )  -> 
( R `  (
k  +  1 ) )  =  ( F `
 ( R `  k ) ) )
3635fveq2d 5511 . . . . . 6  |-  ( ( A  e.  S  /\  k  e.  NN0 )  -> 
( C `  ( R `  ( k  +  1 ) ) )  =  ( C `
 ( F `  ( R `  k ) ) ) )
3734, 36eqtrd 2208 . . . . 5  |-  ( ( A  e.  S  /\  k  e.  NN0 )  -> 
( ( C  o.  R ) `  (
k  +  1 ) )  =  ( C `
 ( F `  ( R `  k ) ) ) )
3837neeq1d 2363 . . . 4  |-  ( ( A  e.  S  /\  k  e.  NN0 )  -> 
( ( ( C  o.  R ) `  ( k  +  1 ) )  =/=  0  <->  ( C `  ( F `
 ( R `  k ) ) )  =/=  0 ) )
39 fvco3 5579 . . . . . 6  |-  ( ( R : NN0 --> S  /\  k  e.  NN0 )  -> 
( ( C  o.  R ) `  k
)  =  ( C `
 ( R `  k ) ) )
407, 39sylan 283 . . . . 5  |-  ( ( A  e.  S  /\  k  e.  NN0 )  -> 
( ( C  o.  R ) `  k
)  =  ( C `
 ( R `  k ) ) )
4137, 40breq12d 4011 . . . 4  |-  ( ( A  e.  S  /\  k  e.  NN0 )  -> 
( ( ( C  o.  R ) `  ( k  +  1 ) )  <  (
( C  o.  R
) `  k )  <->  ( C `  ( F `
 ( R `  k ) ) )  <  ( C `  ( R `  k ) ) ) )
4231, 38, 413imtr4d 203 . . 3  |-  ( ( A  e.  S  /\  k  e.  NN0 )  -> 
( ( ( C  o.  R ) `  ( k  +  1 ) )  =/=  0  ->  ( ( C  o.  R ) `  (
k  +  1 ) )  <  ( ( C  o.  R ) `
 k ) ) )
4315, 22, 42nn0seqcvgd 12008 . 2  |-  ( A  e.  S  ->  (
( C  o.  R
) `  N )  =  0 )
4413, 43eqtr3d 2210 1  |-  ( A  e.  S  ->  ( C `  ( R `  N ) )  =  0 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    = wceq 1353    e. wcel 2146    =/= wne 2345   {csn 3589   class class class wbr 3998    X. cxp 4618    o. ccom 4624   -->wf 5204   ` cfv 5208  (class class class)co 5865   1stc1st 6129   0cc0 7786   1c1 7787    + caddc 7789    < clt 7966   NN0cn0 9149    seqcseq 10415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-coll 4113  ax-sep 4116  ax-nul 4124  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530  ax-iinf 4581  ax-cnex 7877  ax-resscn 7878  ax-1cn 7879  ax-1re 7880  ax-icn 7881  ax-addcl 7882  ax-addrcl 7883  ax-mulcl 7884  ax-addcom 7886  ax-addass 7888  ax-distr 7890  ax-i2m1 7891  ax-0lt1 7892  ax-0id 7894  ax-rnegex 7895  ax-cnre 7897  ax-pre-ltirr 7898  ax-pre-ltwlin 7899  ax-pre-lttrn 7900  ax-pre-apti 7901  ax-pre-ltadd 7902
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-nel 2441  df-ral 2458  df-rex 2459  df-reu 2460  df-rab 2462  df-v 2737  df-sbc 2961  df-csb 3056  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-nul 3421  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-iun 3884  df-br 3999  df-opab 4060  df-mpt 4061  df-tr 4097  df-id 4287  df-iord 4360  df-on 4362  df-ilim 4363  df-suc 4365  df-iom 4584  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-f1 5213  df-fo 5214  df-f1o 5215  df-fv 5216  df-riota 5821  df-ov 5868  df-oprab 5869  df-mpo 5870  df-1st 6131  df-2nd 6132  df-recs 6296  df-frec 6382  df-pnf 7968  df-mnf 7969  df-xr 7970  df-ltxr 7971  df-le 7972  df-sub 8104  df-neg 8105  df-inn 8893  df-n0 9150  df-z 9227  df-uz 9502  df-seqfrec 10416
This theorem is referenced by:  algcvga  12018
  Copyright terms: Public domain W3C validator