# Re: Re: [PVS-Help] fixed-point theory

```Sam Owre:
In order to learn fixed-point theory and PVS. I had tried to replay the proving of the theories in http://www.informatik.uni-ulm.de/ki/PVS/fixpoints.html in the last year under PVS 5.0. But I encounter some difficulties. For example, I cannot prove the lemmata “continuous_admissible” in theory “continuous” using the pvs scripts provide in “continuous.prf”. I don’t know how to instance the following bounded variable “x”:
[-1]  C!2(x!3)
[-2]  lub?(x!1, C!1)
[-3]  FORALL (d: D): EXISTS (x: R): lub?(x, fset_image(C!1)(d))
[-4]  chain?(C!2)
[-5]  chain?(C!1)
[-6]  FORALL (x: (C!1)):
FORALL C:
lub_exists?(set_image(x)(C)) & (x(lub(C)) = lub(set_image(x)(C)))
|-------
[1]   EXISTS (x:
({M: Lub_Exists[R, le_R] |
EXISTS (f: (C!1)): M = set_image[D, R](f)(C!2)})):
lub(fset_image(C!1)(x!3)) = lub[R, le_R](x)
this is an sub-goal of the formula “continuous_admissible: LEMMA admissible?[[D -> R], pointwise.<=](continuous?)”
can you help me. Thanks in advance.

Cheers
Qingguo XU
------------------
2012-06-10
-------------------------------------------------------------

Hi Stan,
I happen to have a copy of it, I'm including it below.
Cheers,
Sam
Stan Rosenberg <stan.rosenberg@xxxxxxxxx> wrote:
> Hi,
>
> I came across this formalization of fixed-points:
> http://www.informatik.uni-ulm.de/ki/PVS/fixpoints.html
> Unfortunately, the link to the dump file is broken.  Does anyone
> happen to know of a mirror or an alternative library?
>
> Thanks,
>
> stan

```