1open HolKernel Parse boolLib bossLib;
2open kolmog_incomputableTheory;
3open plain_kolmog_inequalitiesTheory;
4open transcTheory;
5
6val _ = new_theory "kolmog_prior";
7
8
9
10
11Theorem univ_prior_pos:
12  ���x. 0 < 2 rpow (-&(KC U x))
13Proof
14  rw[] >> `0r < 2` by fs[] >> fs[transcTheory.RPOW_POS_LT]
15QED
16
17
18
19val _ = export_theory();
20
21