cHOL4.bool.F cHOL.False 34 204 120 2.14543087193
cHOL4.num.SUC cNat.Suc 44 487 370 1.84984193413
cHOL4.prim_rec.< cNat.ord_nat_inst.less_nat 46 699 363 1.88198954808
cHOL4.num.0 cNat.zero_nat_inst.zero_nat 57 2764 410 2.15602904399
cHOL4.arithmetic.<= cNat.ord_nat_inst.less_eq_nat 44 500 240 2.10494498001
cHOL4.bool.T cHOL.True 29 232 114 1.85846806751
cHOL4.arithmetic.+ cNat.plus_nat_inst.plus_nat 38 637 235 1.84658768758
cHOL4.list.CONS cList.list.Cons 35 709 689 1.61074102976
cHOL4.list.NIL cList.list.Nil 51 455 601 1.57332186663
cHOL4.bool.COND cHOL.If 20 551 576 1.53933002767
cHOL4.arithmetic.- cNat.minus_nat_inst.minus_nat 23 361 171 1.50893730243
cHOL4.arithmetic.* cNat.times_nat_inst.times_nat 22 221 131 1.61621951908
cHOL4.pair.|comma| cProduct_Type.Pair 28 1117 1073 1.46115624092
cHOL4.combin.o cFun.comp 14 112 154 1.1062669589
cHOL4.list.APPEND cList.append 18 187 164 1.10086396941
cHOL4.option.SOME cOption.option.Some 17 213 182 1.09297640721
cHOL4.option.NONE cOption.option.None 19 159 265 1.02384726817
cHOL4.list.MAP cList.map 20 127 233 0.957818610029
cHOL4.option.IS_NONE cOption.is_none 3 7 3 0.956786966711
cHOL4.real.real_lte cOrderings.ord_class.less_eq 38 494 809 0.798272975543
cHOL4.realax.real_lt cOrderings.ord_class.less 29 417 486 1.12070083379
cHOL4.realax.real_add cGroups.plus_class.plus 31 285 322 1.29895117168
cHOL4.real.real_sub cGroups.minus_class.minus 17 196 307 1.23731686107
cHOL4.quotient.QUOTIENT cQuotient.Quotient3 8 121 42 0.790967397712
cHOL4.sum.INR cSum_Type.Inr 13 57 82 0.745752070462
cHOL4.sum.INL cSum_Type.Inl 11 57 78 1.07145964275
cHOL4.option.OPTREL cLifting_Option.option_rel 6 15 18 0.729261431236
cHOL4.realax.real_neg cGroups.uminus_class.uminus 17 261 198 0.689432343999
cHOL4.realax.real_mul cGroups.times_class.times 20 381 378 0.928854396422
cHOL4.list.LIST_REL cList.list_all2 8 38 67 0.659501772378
cHOL4.list.FLAT cList.concat 6 20 53 0.611710852649
cHOL4.option.OPTION_MAP cOption.map 6 27 28 0.609675333212
cHOL4.combin.I cFun.id 11 139 66 0.689078725031
cHOL4.alist.ALOOKUP cMap.map_of 5 19 41 0.600548737911
cHOL4.real.abs cGroups.abs_class.abs 12 145 74 0.542505893795
cHOL4.list.FILTER cList.filter 8 49 76 0.508589672722
cHOL4.list.ALL_DISTINCT cList.distinct 7 31 71 0.513535238355
cHOL4.realax.real_0 cGroups.zero_class.zero 8 15 542 0.503376981615
cHOL4.quotient.EQUIV cEquiv_Relations.equivp 5 10 21 0.486298890228
cHOL4.sum.OUTR cSum_Type.Projr 1 3 2 0.480898346963
cHOL4.basicSize.option_size cOption.option.option_size 1 2 3 0.480898346963
cHOL4.relation.inv_image cRelation.inv_imagep 1 3 2 0.480898346963
cHOL4.arithmetic.FUNPOW cNat.semiring_1_class.of_nat_aux 2 16 4 0.477366304182
cHOL4.real.pow cPower.power_class.power 7 197 135 0.466209448058
cHOL4.list.FOLDL cList.foldl 3 61 12 0.454648161727
cHOL4.update.FIND cList.find 2 3 9 0.44546130656
cHOL4.pair.## cProduct_Type.map_pair 4 16 24 0.43841209038
cHOL4.quotient.--> cFun.map_fun 4 42 42 0.434696984662
cHOL4.sum.++ cSum_Type.sum_map 2 11 8 0.444463243232
cHOL4.sum.OUTL cSum_Type.Projl 1 4 2 0.434294481903
cHOL4.quotient.PARTIAL_EQUIV cEquiv_Relations.part_equivp 2 2 15 0.432808512267
cHOL4.list.DROP cList.drop 6 33 49 0.41848534796
cHOL4.list.TAKE cList.take 5 34 57 0.414257264297
cHOL4.realax.real_1 cGroups.one_class.one 4 6 240 0.412718240586
cHOL4.pair.FST cProduct_Type.fst 6 102 118 0.402661171343
cHOL4.pair.SND cProduct_Type.snd 5 80 77 0.487041449777
cHOL4.num.ABS_num cNat.Abs_Nat 3 4 10 0.40138603427
cHOL4.num.REP_num cNat.Rep_Nat 2 3 10 0.577078016356
cHOL4.list.EXISTS cList.list_ex 4 33 11 0.395487106554
cHOL4.list.REVERSE cList.rev 10 60 58 0.475027951495
cHOL4.realax.inv cFields.inverse_class.inverse 6 88 71 0.384338565053
cHOL4.relation.RTC cTransitive_Closure.rtranclp 7 40 42 0.365559133953
cHOL4.relation.TC cTransitive_Closure.tranclp 6 46 31 0.392974025058
cHOL4.combin.S cMeson.COMBS 1 7 2 0.360673760222
cHOL4.topology.re_compl cATP.fComp 1 3 5 0.352956123865
cHOL4.patricia.IS_EMPTY cPredicate.null 2 4 9 0.343634472178
cHOL4.arithmetic.DIV cDivides.div_nat_inst.div_nat 3 113 56 0.342737458344
cHOL4.transc.tan cNitpick.inverse_frac 1 17 1 0.339623271895
cHOL4.option.OPTION_BIND cOption.bind 2 9 9 0.339455557042
cHOL4.list.LAST cList.last 2 18 23 0.331637270673
cHOL4.pair.UNCURRY cProduct_Type.prod.prod_case 6 90 291 0.327709188761
cHOL4.pair.CURRY cProduct_Type.curry 3 6 10 0.726896611574
cHOL4.llist.LCONS cSet.insert 8 66 352 0.327419165031
cHOL4.list.FRONT cList.butlast 2 19 24 0.326430994346
cHOL4.arithmetic.MOD cDivides.div_nat_inst.mod_nat 3 144 84 0.31912193205
cHOL4.num.ZERO_REP cNat.Zero_Rep 1 3 7 0.318928988904
cHOL4.list.LIST_TO_SET cList.member 2 152 4 0.311844203472
cHOL4.list.NULL cList.null 2 33 20 0.307916586747
cHOL4.marker.AC cLattices.inf_bool_inst.inf_bool 1 1 1 0.303413075542
cHOL4.real.real_of_num cNat.semiring_1_class.of_nat 8 872 154 0.297346149115
cHOL4.list.EVERY cList.list_all 4 77 14 0.292304880126
cHOL4.relation.WFP cWellfounded.accp 2 7 140 0.290292981178
cHOL4.frac.frac_ainv cNitpick.uminus_frac 1 15 2 0.288539008178
cHOL4.quotient_pair.### cLifting_Product.prod_rel 3 15 18 0.287400641703
cHOL4.real./ cFields.inverse_class.divide 3 218 157 0.287334323107
cHOL4.min.|at| cHOL.The 4 149 36 0.27364279479
cHOL4.while.LEAST cHilbert_Choice.Eps 3 29 21 0.272794006254
cHOL4.relation.total cOrderings.class.linorder_axioms 1 5 8 0.267546386419
cHOL4.num.SUC_REP cNat.Suc_Rep 1 5 9 0.259730302172
cHOL4.rich_list.REPLICATE cList.replicate 3 6 39 0.250807568621
cHOL4.Encode.wf_pred cEnum.enum_class.enum_ex 1 4 13 0.250690398439
cHOL4.quotient.RES_EXISTS_EQUIV cQuotient.Bex1_rel 1 8 7 0.246278545814
cHOL4.divides.divides cRings.dvd_class.dvd 5 37 189 0.237966179347
cHOL4.relation.WF cWellfounded.wfP 3 134 14 0.23215822086
cHOL4.combin.K cMeson.COMBK 2 45 5 0.230416869459
cHOL4.fmapal.AP_SND cProduct_Type.apsnd 1 3 25 0.230212890055
cHOL4.relation.antisymmetric cOrderings.class.order_axioms 1 11 8 0.222231621616
cHOL4.frac.frac_dnm cNitpick.denom 1 16 6 0.218104055187
cHOL4.combin.FAIL cProduct_Type.unit.unit_case 1 11 9 0.216679065336
cHOL4.extreal.PosInf cCode_Numeral.zero_integer_inst.zero_integer 7 137 32 0.215845662014
cHOL4.extreal.Normal cCode_Numeral.Neg 4 120 24 0.258072433886
cHOL4.extreal.extreal_le cCode_Numeral.ord_integer_inst.less_eq_integer 3 199 15 0.249936740442
cHOL4.frac.abs_frac cNitpick.Abs_Frac 1 25 5 0.206432984968
cHOL4.rich_list.SPLITP cList.partition 1 13 10 0.20480044365
cHOL4.extreal.extreal_exp cCode_Numeral.dup 2 3 9 0.197982802916
cHOL4.path.pcons cQuickcheck_Narrowing.ffun.Update 4 45 25 0.197641486817
cHOL4.rich_list.PREFIX cList.takeWhile 2 5 35 0.195877040131
cHOL4.extreal.mono_increasing cOrderings.order_class.mono 1 4 43 0.19383393703
cHOL4.frac.frac_nmr cNitpick.num 1 27 7 0.190393743528
cHOL4.list.SUM cList.monoid_add_class.listsum 2 19 41 0.175160048557
cHOL4.relation.reflexive cRelation.reflp 1 13 29 0.168420025657
cHOL4.state_transformer.JOIN cQuickcheck_Random.collapse 1 6 70 0.165425826455
cHOL4.ind_type.FCONS cNat.nat.nat_case 1 15 29 0.164475491409
cHOL4.relation.transitive cRelation.transp 2 31 16 0.164111479823
cHOL4.relation.RDOM cRelation.Domainp 1 17 33 0.157896075764
cHOL4.basicSize.sum_size cSum_Type.sum.sum_rec 1 2 11 0.157328990222
cHOL4.one.one cProduct_Type.Unity 3 26 119 0.155513909227
cHOL4.list.SNOC cList.insert 1 62 10 0.155449916459
cHOL4.extreal.extreal_sub cCode_Numeral.times_integer_inst.times_integer 1 61 11 0.153568659304
cHOL4.relation.EMPTY_REL cEnum.ord_finite_1_inst.less_finite_1 1 7 1 0.151706537771
cHOL4.list.HD cList.hd 1 34 22 0.15105573138
cHOL4.patricia.Empty cPredicate.seq.Empty 5 48 42 0.140187782671
cHOL4.patricia.ptree_size cPredicate.seq.seq_size 1 3 4 0.37892318169
cHOL4.llist.LMAP cSet.image 3 8 285 0.139479926835
cHOL4.bool.?! cHOL.Ex1 1 35 41 0.137545662156
cHOL4.llist.LFINITE cFinite_Set.finite 4 26 444 0.120833352286
cHOL4.patricia_casts.SKIP1 cList.tl 1 2 31 0.120224586741
cHOL4.bool.DATATYPE cQuotient.Quot_True 1 14 7 0.108573620476
cHOL4.extreal.extreal_sqrt cCode_Numeral.uminus_integer_inst.uminus_integer 1 7 15 0.107001565371
cHOL4.combin.|colon|> cHOL.Let 1 1 106 0.106788976162
cHOL4.marker.|colon|- cCode_Evaluation.tracing 1 1 1 0.101137691847
cHOL4.transc.exp cNum.num.Bit0 2 34 582 0.10111491654
cHOL4.integer.int_neg cInt.uminus_int_inst.uminus_int 1 248 87 0.100206128454
cHOL4.bool.the_value cTYPE 1 314 196 0.090682054851
cHOL4.ieee.Un cEnum.finite_4.a\<__caret__sub>4 2 10 28 0.0889418764777
cHOL4.ieee.Gt cEnum.finite_4.a\<__caret__sub>1 4 13 31 0.185847144146
cHOL4.ieee.Lt cEnum.finite_4.a\<__caret__sub>2 4 14 36 0.24125736055
cHOL4.ieee.Eq cEnum.finite_4.a\<__caret__sub>3 4 15 36 0.635398091055
cHOL4.ieee.ccode2num cEnum.finite_4.finite_4_size 1 10 5 0.126542434639
cHOL4.prelim.LESS cEnum.finite_3.a\<__caret__sub>1 5 16 28 0.0864324028906
cHOL4.prelim.GREATER cEnum.finite_3.a\<__caret__sub>3 7 18 33 0.279695830068
cHOL4.prelim.EQUAL cEnum.finite_3.a\<__caret__sub>2 7 21 32 1.07473555836
cHOL4.prelim.ordering2num cEnum.finite_3.finite_3_size 1 9 4 0.137453788871
cHOL4.option.THE cOption.the 1 26 15 0.0837343954117
cHOL4.list.list_size cList.list.list_size 1 4 16 0.079561050697
cHOL4.gcd.lcm cOrderings.ord_class.min 1 11 89 0.0725839791822
cHOL4.string.ORD cCode_Numeral.nat_of_natural 4 24 46 0.0714381186011
cHOL4.string.char_le cCode_Numeral.ord_natural_inst.less_eq_natural 1 1 41 0.265872585675
cHOL4.string.char_lt cCode_Numeral.ord_natural_inst.less_natural 1 3 163 0.161382880145
cHOL4.string.CHR cCode_Numeral.natural_of_nat 1 68 33 0.129585611444
cHOL4.hrat.hrat_1 cHOL.undefined 1 15 104 0.0679927766559
cHOL4.ind_type.FNIL cSMT.pat 1 1 1 0.303413075542
cHOL4.bool.ARB cSMT.pattern.Pattern 1 35 20 0.152580128353
cHOL4.operator.ASSOC cGroups.semigroup 1 13 13 0.0648298609332
cHOL4.llist.fromList cList.set 2 10 357 0.0611181122846
cHOL4.poly.poly_add cList.splice 2 19 12 0.0597637477384
cHOL4.integer.int_REP cInt.Rep_Integ 1 5 16 0.0567315469791
cHOL4.integer.int_ABS cInt.Abs_Integ 1 5 22 0.21193180867
cHOL4.integer.tint_eq cInt.intrel 1 23 26 0.156324995568
cHOL4.combin.C cMeson.COMBC 1 12 2 0.0511546127384
cHOL4.arithmetic.MAX cOrderings.ord_class.max 4 23 92 0.048945883156
cHOL4.numeral.iDUB cNum.neg_numeral_class.dbl_inc 1 24 6 0.0401315784293
cHOL4.enumeral.bl_size cQuickcheck_Exhaustive.three_valued.three_valued_size 1 2 3 0.0400748622469
cHOL4.canonical.canonical_sum_size cQuickcheck_Exhaustive.unknown.unknown_size 1 2 3 0.0961796693926
cHOL4.canonical.Nil_monom cQuickcheck_Exhaustive.unknown.Unknown 1 42 24 0.144556599601
cHOL4.enumeral.nbl cQuickcheck_Exhaustive.three_valued.Unknown_value 2 15 28 0.0964983987655
cHOL4.hreal.hreal_1 cExtraction.sumbool.Left 1 7 22 0.0396050896724
cHOL4.enumeral.bt_to_list cLazy_Sequence.list_of_lazy_sequence 1 3 23 0.0390990342869
cHOL4.enumeral.nt cLazy_Sequence.empty 1 56 45 0.127668144262
cHOL4.string.IMPLODE cList.rotate1 2 14 13 0.0374382551028
cHOL4.string.EXPLODE cList.remdups_adj 2 16 24 0.0909471889618
cHOL4.arithmetic.ODD cNum.ring_1_class.iszero 1 47 19 0.036781886711
cHOL4.integer.int_mul cLattices.inf_class.inf 7 191 287 0.0366402330034
cHOL4.integer.int_add cLattices.sup_class.sup 5 212 308 0.20164961792
cHOL4.numpair.nlen cNat.nat.nat_size 1 3 3 0.026064524464
cHOL4.numeral_bit.iLOG2 cNat.nat.size_nat_inst.size_nat 1 5 4 0.046216493307
cHOL4.extreal.NegInf cOrderings.bot_class.bot 3 119 613 0.0257147774764
cHOL4.toto.zer cOrderings.top_class.top 1 13 305 0.030172227587
cHOL4.hreal.hreal_lt cRings.class.zero_neq_one 1 20 24 0.0202332681702
cHOL4.rat.rat_leq cEnum.ord_finite_2_inst.less_eq_finite_2 1 15 1 0.019608673548
cHOL4.rat.rat_les cEnum.ord_finite_2_inst.less_finite_2 1 42 2 0.224499782682
cHOL4.arithmetic.nat_elim__magic cSMT.fun_app 1 1 1 0.0182047845325
cHOL4.marker.Cong cQuickcheck_Narrowing.ensure_testable 1 1 1 0.0252844229619
cHOL4.marker.Abbrev cMeson.COMBI 1 3 2 0.0200374311235
cHOL4.marker.stmarker cprop 1 11 4 0.0186563754689
cHOL4.poly.normalize cList.remdups 1 4 25 0.0144144991459
cHOL4.toto.num2cpn cString.nibble_of_nat 2 7 24 0.0139786280577
cHOL4.toto.cpn2num cString.nat_of_nibble 3 8 24 0.191263948924
cHOL4.toto.LESS cString.nibble.Nibble0 4 98 145 0.210036240124
cHOL4.wot.mex_less_eq cCode_Numeral.ord_integer_inst.less_integer 1 2 52 0.0134021263575
cHOL4.ieee.roundmode_size cString.char.size_char_inst.size_char 1 1 3 0.0126803047869
cHOL4.toto.cpn_size cString.nibble.nibble_size 1 1 4 0.0155030729598
cHOL4.basicSize.bool_size cHOL.bool.size_bool_inst.size_bool 1 2 4 0.0173717792761
cHOL4.integer.ABS cGroups.sgn_class.sgn 1 34 18 0.011125954495
cHOL4.string.char_size cNat.size_class.size 1 1 276 0.0111059360141
cHOL4.toto.EQUAL cString.nibble.NibbleA 4 43 74 0.00946311800063
cHOL4.toto.GREATER cString.nibble.NibbleB 4 45 120 0.0332437570656
cHOL4.integer.int_sub cInt.minus_int_inst.minus_int 1 72 117 0.00921922993393
cHOL4.poly.## cList.removeAll 1 11 15 0.00348909035682
cHOL4.frac.frac_1 cCode_Evaluation.term.dummy_term 1 6 21 0.0017174940963
cHOL4.divides.prime cNum.neg_numeral_class.is_num 1 25 11 0.00107762930217
cHOL4.fixedPoint.empty cCode_Numeral.pcr_natural 1 3 19 0.000851548825729
cHOL4.ind_type.ZRECSPACE cTransfer.right_unique 1 9 26 0.000847322866961
cHOL4.enumeral.list_to_bt cLazy_Sequence.lazy_sequence.lazy_sequence_of_list 1 6 31 0.0004037407308
cHOL4.pair.REP_prod cProduct_Type.Rep_prod 1 2 7 0.000133385266354
cHOL4.pair.ABS_prod cProduct_Type.Abs_prod 1 3 7 0.318928988904
cHOL4.ieee.roundmode2num cString.nat_of_char 2 9 266 0.000105895010763
cHOL4.ieee.num2roundmode cString.char_of_nat 1 8 5 0.267546386419
cHOL4.fcp.BIT0B cQuickcheck_Narrowing.cfun.Constant 1 9 20 8.83086535363e-05
cHOL4.integer.Num cInt.ring_1_class.of_int 1 16 36 6.41809142774e-05
cHOL4.bit.BIT_REVERSE cDivides.div_class.div 0 7 47 0.
cHOL4.arithmetic.NUMERAL cNum.neg_numeral_class.dbl 0 1744 7 0.
cHOL4.bag.BAG_ALL_DISTINCT cFunDef.is_measure 0 13 9 0.
cHOL4.realax.hreal_of_real cNum.numeral_class.numeral 0 1 699 0.
cHOL4.real.min cDivides.div_class.mod 0 15 73 0.
cHOL4.gcd.is_gcd cPartial_Function.flat_ord 0 9 30 0.
cHOL4.rat.rat_ainv cNum.neg_numeral_class.dbl_dec 0 25 7 0.
cHOL4.transc.sqrt cNum.num.Bit1 0 25 388 0.
cHOL4.transc.pi cNum.num.One 0 55 644 0.
cHOL4.bag.EMPTY_BAG cCode_Evaluation.term.size_term_inst.size_term 0 72 2 0.
cHOL4.ind_type.NUMFST cMeson.skolem 0 2 4 0.
cHOL4.pred_set.SUM_SET cOrderings.ord_class.Least 0 8 17 0.
cHOL4.integer.int_0 cInt.one_int_inst.one_int 0 9 217 0.
cHOL4.integer.int_1 cInt.zero_int_inst.zero_int 0 7 338 0.
cHOL4.relation.WeakOrder cOrderings.class.wellorder_axioms 0 11 8 0.
cHOL4.integer.int_divides cInt.ord_int_inst.less_eq_int 0 40 249 0.
cHOL4.integer.int_ge cInt.ord_int_inst.less_int 0 42 271 0.
cHOL4.integer.int_max cInt.plus_int_inst.plus_int 0 4 221 0.
cHOL4.integer.int_min cInt.times_int_inst.times_int 0 4 137 0.
cHOL4.extreal.extreal_abs cCode_Numeral.abs_integer_inst.abs_integer 0 11 10 0.
cHOL4.toto.num_dt_size cSMT.pattern.size_pattern_inst.size_pattern 0 2 2 0.
cHOL4.extreal.extreal_div cCode_Numeral.div_integer_inst.div_integer 0 34 9 0.
cHOL4.lbtree.finite cPredicate.is_empty 0 9 13 0.
cHOL4.extreal.extreal_of_num cCode_Numeral.integer_of_nat 0 190 6 0.
cHOL4.llist.every cBig_Operators.comm_monoid_add_class.setsum 0 10 128 0.
cHOL4.bit.DIVMOD_2EXP cDivides.divmod_nat 0 3 13 0.
cHOL4.llist.exists cBig_Operators.comm_monoid_mult_class.setprod 0 15 63 0.
cHOL4.nets.dorder cOrderings.class.dense_order_axioms 0 14 8 0.
cHOL4.relation.symmetric cRelation.symp 0 7 16 0.
cHOL4.numeral_bit.iMOD_2EXP cNat.inf_nat_inst.inf_nat 0 4 1 0.
cHOL4.relation.equivalence cOrderings.class.no_bot_axioms 0 5 8 0.
cHOL4.operator.MONOID cRings.class.no_zero_divisors 0 7 15 0.