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