# Re: [isabelle] Pending sort hypotheses

```Hi all,

Ok, I solved my problem all by myself :-)

Just in case it might be useful to someone, here is the solution:

interpretation rs:product_prob_space "(λi. bernoulli bp)" "UNIV::(nat × Proc) set"
where "SORT_CONSTRAINT('a::{finite,perfect_space,real_normed_vector} )"
proof [...]

H

> Hi all,
>
> I am trying to define a randomized algorithm in order to prove it is correct. On this purpose, I defined following objects:
>
>
> "bernoulli p ≡ point_measure (UNIV :: bool set) (% True => p | False => 1 - p)"
>
>
> interpretation rs:product_prob_space "(λi. bernoulli p)" "UNIV::(nat × Proc) set" for p
> proof  (unfold_locales, auto)
> have "(UNIV :: bool set) = { True, False }" by auto
> thus "emeasure (bernoulli p) (space (bernoulli p)) = ∞ ⟹ False"
> using emeasure_point_measure_finite finite_UNIV
> proof (unfold bernoulli_def, blast) qed
> ...
>
>
>
> Proof goes fine (just ends with "no subgoals") but at "qed" I obtain the following error:
>
> Pending sort hypotheses:
> {finite,perfect_space,real_normed_vector}
>
>
> Does anyone have any idea on how to solve this issue ?
>