Path	Lines of Code
hollight/test/aime-1983-p1.ml	9
hollight/test/aime-1983-p2.ml	1
hollight/test/aime-1983-p3.ml	6
hollight/test/aime-1984-p1.ml	7
hollight/test/aime-1984-p7.ml	1
hollight/test/aime-1994-p3.ml	6
hollight/test/aime-1995-p7.ml	8
hollight/test/algebra-2varlineareq-fp3zeq11-3tfm1m5zeqn68-feqn10-zeq7.ml	7
hollight/test/algebra-amgm-sum1toneqn-prod1tonleq1.ml	1
hollight/test/algebra-amgm-sumasqdivbgeqsuma.ml	1
hollight/test/algebra-ineq-nto1onlt2m1on.ml	1
hollight/test/algebra-others-exirrpowirrrat.ml	1
hollight/test/algebra-sqineq-at2malt1.ml	1
hollight/test/algebra-sqineq-unitcircatbpabsamblt1.ml	5
hollight/test/algebra-sqineq-unitcircatbpamblt1.ml	1
hollight/test/amc12-2000-p1.ml	1
hollight/test/amc12-2000-p12.ml	1
hollight/test/amc12-2000-p20.ml	1
hollight/test/amc12-2000-p6.ml	1
hollight/test/amc12-2001-p21.ml	1
hollight/test/amc12-2001-p5.ml	1
hollight/test/amc12a-2002-p13.ml	1
hollight/test/amc12a-2002-p6.ml	1
hollight/test/amc12a-2003-p23.ml	1
hollight/test/amc12a-2003-p5.ml	1
hollight/test/amc12a-2020-p10.ml	6
hollight/test/amc12a-2020-p15.ml	6
hollight/test/amc12a-2020-p4.ml	9
hollight/test/amc12a-2020-p7.ml	11
hollight/test/amc12a-2020-p9.ml	4
hollight/test/amc12a-2021-p12.ml	6
hollight/test/amc12a-2021-p14.ml	1
hollight/test/amc12a-2021-p18.ml	6
hollight/test/amc12a-2021-p19.ml	4
hollight/test/amc12a-2021-p22.ml	6
hollight/test/amc12a-2021-p25.ml	6
hollight/test/amc12a-2021-p3.ml	7
hollight/test/amc12a-2021-p8.ml	8
hollight/test/amc12a-2021-p9.ml	1
hollight/test/amc12b-2002-p19.ml	6
hollight/test/amc12b-2002-p2.ml	1
hollight/test/amc12b-2002-p4.ml	6
hollight/test/amc12b-2002-p7.ml	8
hollight/test/amc12b-2020-p13.ml	1
hollight/test/amc12b-2020-p2.ml	1
hollight/test/amc12b-2020-p21.ml	1
hollight/test/amc12b-2020-p22.ml	1
hollight/test/amc12b-2020-p6.ml	1
hollight/test/amc12b-2021-p1.ml	1
hollight/test/amc12b-2021-p13.ml	1
hollight/test/amc12b-2021-p18.ml	4
hollight/test/amc12b-2021-p3.ml	5
hollight/test/amc12b-2021-p4.ml	6
hollight/test/amc12b-2021-p9.ml	1
hollight/test/imo-1959-q1.ml	1
hollight/test/imo-2007-a6.ml	6
hollight/test/imo-2019-q1.ml	1
hollight/test/induction-11div10tonmn1ton.ml	1
hollight/test/induction-12dvd4expnp1p20.ml	1
hollight/test/induction-1pxpownlt1pnx.ml	1
hollight/test/induction-nfactltnexpnm1ngt3.ml	1
hollight/test/induction-sumkexp3eqsumksqsq.ml	1
hollight/test/mathb-algebra-44.ml	1
hollight/test/mathd-algebra-107.ml	1
hollight/test/mathd-algebra-113.ml	1
hollight/test/mathd-algebra-114.ml	1
hollight/test/mathd-algebra-125.ml	1
hollight/test/mathd-algebra-129.ml	6
hollight/test/mathd-algebra-137.ml	5
hollight/test/mathd-algebra-139.ml	9
hollight/test/mathd-algebra-141.ml	7
hollight/test/mathd-algebra-142.ml	6
hollight/test/mathd-algebra-143.ml	6
hollight/test/mathd-algebra-148.ml	6
hollight/test/mathd-algebra-153.ml	5
hollight/test/mathd-algebra-156.ml	1
hollight/test/mathd-algebra-158.ml	6
hollight/test/mathd-algebra-160.ml	6
hollight/test/mathd-algebra-17.ml	1
hollight/test/mathd-algebra-170.ml	1
hollight/test/mathd-algebra-171.ml	1
hollight/test/mathd-algebra-176.ml	1
hollight/test/mathd-algebra-184.ml	7
hollight/test/mathd-algebra-196.ml	1
hollight/test/mathd-algebra-208.ml	1
hollight/test/mathd-algebra-215.ml	1
hollight/test/mathd-algebra-24.ml	1
hollight/test/mathd-algebra-246.ml	6
hollight/test/mathd-algebra-263.ml	6
hollight/test/mathd-algebra-270.ml	5
hollight/test/mathd-algebra-275.ml	5
hollight/test/mathd-algebra-276.ml	5
hollight/test/mathd-algebra-288.ml	9
hollight/test/mathd-algebra-289.ml	8
hollight/test/mathd-algebra-293.ml	1
hollight/test/mathd-algebra-296.ml	1
hollight/test/mathd-algebra-302.ml	1
hollight/test/mathd-algebra-304.ml	1
hollight/test/mathd-algebra-313.ml	7
hollight/test/mathd-algebra-314.ml	5
hollight/test/mathd-algebra-320.ml	7
hollight/test/mathd-algebra-329.ml	6
hollight/test/mathd-algebra-33.ml	1
hollight/test/mathd-algebra-332.ml	7
hollight/test/mathd-algebra-338.ml	7
hollight/test/mathd-algebra-342.ml	6
hollight/test/mathd-algebra-346.ml	6
hollight/test/mathd-algebra-354.ml	6
hollight/test/mathd-algebra-362.ml	6
hollight/test/mathd-algebra-388.ml	6
hollight/test/mathd-algebra-392.ml	5
hollight/test/mathd-algebra-398.ml	7
hollight/test/mathd-algebra-400.ml	5
hollight/test/mathd-algebra-412.ml	6
hollight/test/mathd-algebra-419.ml	6
hollight/test/mathd-algebra-427.ml	7
hollight/test/mathd-algebra-432.ml	1
hollight/test/mathd-algebra-440.ml	1
hollight/test/mathd-algebra-478.ml	8
hollight/test/mathd-algebra-484.ml	1
hollight/test/mathd-algebra-487.ml	8
hollight/test/mathd-algebra-513.ml	6
hollight/test/mathd-algebra-76.ml	6
hollight/test/mathd-algebra-80.ml	1
hollight/test/mathd-numbertheory-100.ml	7
hollight/test/mathd-numbertheory-127.ml	1
hollight/test/mathd-numbertheory-135.ml	9
hollight/test/mathd-numbertheory-150.ml	1
hollight/test/mathd-numbertheory-175.ml	1
hollight/test/mathd-numbertheory-185.ml	1
hollight/test/mathd-numbertheory-207.ml	1
hollight/test/mathd-numbertheory-212.ml	1
hollight/test/mathd-numbertheory-222.ml	6
hollight/test/mathd-numbertheory-227.ml	1
hollight/test/mathd-numbertheory-229.ml	1
hollight/test/mathd-numbertheory-233.ml	6
hollight/test/mathd-numbertheory-234.ml	6
hollight/test/mathd-numbertheory-235.ml	1
hollight/test/mathd-numbertheory-237.ml	1
hollight/test/mathd-numbertheory-247.ml	1
hollight/test/mathd-numbertheory-254.ml	1
hollight/test/mathd-numbertheory-277.ml	6
hollight/test/mathd-numbertheory-299.ml	1
hollight/test/mathd-numbertheory-3.ml	1
hollight/test/mathd-numbertheory-321.ml	6
hollight/test/mathd-numbertheory-328.ml	1
hollight/test/mathd-numbertheory-34.ml	6
hollight/test/mathd-numbertheory-341.ml	6
hollight/test/mathd-numbertheory-342.ml	1
hollight/test/mathd-numbertheory-345.ml	1
hollight/test/mathd-numbertheory-427.ml	4
hollight/test/mathd-numbertheory-447.ml	1
hollight/test/mathd-numbertheory-451.ml	3
hollight/test/mathd-numbertheory-495.ml	8
hollight/test/mathd-numbertheory-551.ml	1
hollight/test/mathd-numbertheory-552.ml	8
hollight/test/mathd-numbertheory-618.ml	6
hollight/test/mathd-numbertheory-66.ml	1
hollight/test/mathd-numbertheory-85.ml	1
hollight/test/mathd-numbertheory-99.ml	1
hollight/test/numbertheory-aoddbdiv4asqpbsqmod8eq1.ml	6
hollight/test/numbertheory-notequiv2i2jasqbsqdiv8.ml	1
hollight/test/others-chickenmcnuggets.ml	1
isabelle/test/aime_1983_p1.thy	33
isabelle/test/aime_1983_p2.thy	13
isabelle/test/aime_1983_p3.thy	12
isabelle/test/aime_1984_p1.thy	32
isabelle/test/aime_1984_p7.thy	12
isabelle/test/aime_1987_p5.thy	13
isabelle/test/aime_1988_p8.thy	15
isabelle/test/aime_1989_p8.thy	15
isabelle/test/aime_1990_p15.thy	16
isabelle/test/aime_1990_p4.thy	18
isabelle/test/aime_1991_p9.thy	15
isabelle/test/aime_1994_p3.thy	12
isabelle/test/aime_1995_p7.thy	13
isabelle/test/aime_1997_p9.thy	16
isabelle/test/aime_1999_p11.thy	16
isabelle/test/algebra_2varlineareq_fp3zeq11_3tfm1m5zeqn68_feqn10_zeq7.thy	22
isabelle/test/algebra_9onxpypzleqsum2onxpy.thy	12
isabelle/test/algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2.thy	14
isabelle/test/algebra_absapbon1pabsapbleqsumabsaon1pabsa.thy	12
isabelle/test/algebra_absxm1pabsxpabsxp1eqxp2_0leqxleq1.thy	13
isabelle/test/algebra_amgm_sum1toneqn_prod1tonleq1.thy	12
isabelle/test/algebra_amgm_sumasqdivbgeqsuma.thy	12
isabelle/test/algebra_apbmpcneq0_aeq0anbeq0anceq0.thy	17
isabelle/test/algebra_apbon2pownleqapownpbpowon2.thy	14
isabelle/test/algebra_apbpceq2_abpbcpcaeq1_aleq1on3anbleq1ancleq4on3.thy	15
isabelle/test/algebra_bleqa_apbon2msqrtableqambsqon8b.thy	13
isabelle/test/algebra_cubrtrp1oncubrtreq3_rcubp1onrcubeq5778.thy	13
isabelle/test/algebra_ineq_nto1onlt2m1on.thy	11
isabelle/test/algebra_others_exirrpowirrrat.thy	10
isabelle/test/algebra_sqineq_at2malt1.thy	15
isabelle/test/algebra_sqineq_unitcircatbpabsamblt1.thy	12
isabelle/test/algebra_sqineq_unitcircatbpamblt1.thy	12
isabelle/test/algebra_sum1onsqrt2to1onsqrt10000lt198.thy	10
isabelle/test/amc12_2000_p1.thy	13
isabelle/test/amc12_2000_p12.thy	12
isabelle/test/amc12_2000_p20.thy	15
isabelle/test/amc12_2000_p6.thy	22
isabelle/test/amc12_2001_p21.thy	15
isabelle/test/amc12_2001_p5.thy	11
isabelle/test/amc12a_2002_p13.thy	15
isabelle/test/amc12a_2002_p6.thy	12
isabelle/test/amc12a_2003_p23.thy	11
isabelle/test/amc12a_2003_p5.thy	14
isabelle/test/amc12a_2008_p25.thy	16
isabelle/test/amc12a_2009_p6.thy	14
isabelle/test/amc12a_2009_p7.thy	19
isabelle/test/amc12a_2013_p4.thy	10
isabelle/test/amc12a_2019_p12.thy	15
isabelle/test/amc12a_2020_p10.thy	14
isabelle/test/amc12a_2020_p15.thy	13
isabelle/test/amc12a_2020_p25.thy	15
isabelle/test/amc12a_2020_p4.thy	15
isabelle/test/amc12a_2020_p7.thy	19
isabelle/test/amc12a_2020_p9.thy	11
isabelle/test/amc12a_2021_p12.thy	15
isabelle/test/amc12a_2021_p14.thy	12
isabelle/test/amc12a_2021_p18.thy	13
isabelle/test/amc12a_2021_p19.thy	12
isabelle/test/amc12a_2021_p22.thy	15
isabelle/test/amc12a_2021_p25.thy	14
isabelle/test/amc12a_2021_p3.thy	14
isabelle/test/amc12a_2021_p8.thy	15
isabelle/test/amc12a_2021_p9.thy	10
isabelle/test/amc12b_2002_p19.thy	27
isabelle/test/amc12b_2002_p2.thy	12
isabelle/test/amc12b_2002_p4.thy	13
isabelle/test/amc12b_2002_p7.thy	14
isabelle/test/amc12b_2020_p13.thy	11
isabelle/test/amc12b_2020_p2.thy	11
isabelle/test/amc12b_2020_p21.thy	10
isabelle/test/amc12b_2020_p22.thy	11
isabelle/test/amc12b_2020_p6.thy	13
isabelle/test/amc12b_2021_p1.thy	10
isabelle/test/amc12b_2021_p13.thy	11
isabelle/test/amc12b_2021_p18.thy	13
isabelle/test/amc12b_2021_p3.thy	13
isabelle/test/amc12b_2021_p4.thy	12
isabelle/test/amc12b_2021_p9.thy	11
isabelle/test/imo_1959_p1.thy	11
isabelle/test/imo_1960_p2.thy	13
isabelle/test/imo_1962_p2.thy	14
isabelle/test/imo_1963_p5.thy	11
isabelle/test/imo_1964_p2.thy	17
isabelle/test/imo_1965_p2.thy	23
isabelle/test/imo_1968_p5_1.thy	15
isabelle/test/imo_1969_p2.thy	17
isabelle/test/imo_1974_p3.thy	13
isabelle/test/imo_1977_p6.thy	12
isabelle/test/imo_1981_p6.thy	14
isabelle/test/imo_1982_p1.thy	16
isabelle/test/imo_1983_p6.thy	14
isabelle/test/imo_1984_p6.thy	17
isabelle/test/imo_1985_p6.thy	14
isabelle/test/imo_1992_p1.thy	14
isabelle/test/imo_1997_p5.thy	14
isabelle/test/imo_2001_p6.thy	16
isabelle/test/imo_2007_p6.thy	13
isabelle/test/imo_2019_p1.thy	12
isabelle/test/induction_11div10tonmn1ton.thy	11
isabelle/test/induction_12dvd4expnp1p20.thy	11
isabelle/test/induction_1pxpownlt1pnx.thy	13
isabelle/test/induction_nfactltnexpnm1ngt3.thy	13
isabelle/test/induction_pord1p1on2powklt5on2.thy	12
isabelle/test/induction_pprime_pdvdapowpma.thy	14
isabelle/test/induction_prod1p1onk3le3m1onn.thy	12
isabelle/test/induction_sumkexp3eqsumksq.thy	12
isabelle/test/mathd_algebra_107.thy	12
isabelle/test/mathd_algebra_113.thy	12
isabelle/test/mathd_algebra_114.thy	13
isabelle/test/mathd_algebra_125.thy	14
isabelle/test/mathd_algebra_129.thy	14
isabelle/test/mathd_algebra_137.thy	13
isabelle/test/mathd_algebra_139.thy	13
isabelle/test/mathd_algebra_141.thy	12
isabelle/test/mathd_algebra_142.thy	14
isabelle/test/mathd_algebra_143.thy	14
isabelle/test/mathd_algebra_148.thy	14
isabelle/test/mathd_algebra_153.thy	14
isabelle/test/mathd_algebra_156.thy	18
isabelle/test/mathd_algebra_158.thy	15
isabelle/test/mathd_algebra_160.thy	14
isabelle/test/mathd_algebra_17.thy	14
isabelle/test/mathd_algebra_170.thy	10
isabelle/test/mathd_algebra_171.thy	13
isabelle/test/mathd_algebra_176.thy	12
isabelle/test/mathd_algebra_184.thy	13
isabelle/test/mathd_algebra_188.thy	14
isabelle/test/mathd_algebra_196.thy	11
isabelle/test/mathd_algebra_208.thy	11
isabelle/test/mathd_algebra_209.thy	14
isabelle/test/mathd_algebra_215.thy	9
isabelle/test/mathd_algebra_24.thy	13
isabelle/test/mathd_algebra_246.thy	15
isabelle/test/mathd_algebra_263.thy	13
isabelle/test/mathd_algebra_270.thy	13
isabelle/test/mathd_algebra_275.thy	12
isabelle/test/mathd_algebra_276.thy	12
isabelle/test/mathd_algebra_288.thy	17
isabelle/test/mathd_algebra_289.thy	16
isabelle/test/mathd_algebra_293.thy	13
isabelle/test/mathd_algebra_296.thy	9
isabelle/test/mathd_algebra_302.thy	10
isabelle/test/mathd_algebra_304.thy	10
isabelle/test/mathd_algebra_313.thy	16
isabelle/test/mathd_algebra_314.thy	13
isabelle/test/mathd_algebra_320.thy	16
isabelle/test/mathd_algebra_329.thy	14
isabelle/test/mathd_algebra_33.thy	13
isabelle/test/mathd_algebra_332.thy	14
isabelle/test/mathd_algebra_338.thy	15
isabelle/test/mathd_algebra_342.thy	14
isabelle/test/mathd_algebra_346.thy	14
isabelle/test/mathd_algebra_354.thy	14
isabelle/test/mathd_algebra_359.thy	13
isabelle/test/mathd_algebra_362.thy	14
isabelle/test/mathd_algebra_388.thy	13
isabelle/test/mathd_algebra_392.thy	13
isabelle/test/mathd_algebra_398.thy	15
isabelle/test/mathd_algebra_400.thy	13
isabelle/test/mathd_algebra_412.thy	13
isabelle/test/mathd_algebra_419.thy	12
isabelle/test/mathd_algebra_427.thy	14
isabelle/test/mathd_algebra_432.thy	11
isabelle/test/mathd_algebra_44.thy	12
isabelle/test/mathd_algebra_440.thy	13
isabelle/test/mathd_algebra_441.thy	13
isabelle/test/mathd_algebra_452.thy	13
isabelle/test/mathd_algebra_459.thy	16
isabelle/test/mathd_algebra_478.thy	14
isabelle/test/mathd_algebra_484.thy	11
isabelle/test/mathd_algebra_487.thy	16
isabelle/test/mathd_algebra_513.thy	14
isabelle/test/mathd_algebra_598.thy	15
isabelle/test/mathd_algebra_756.thy	13
isabelle/test/mathd_algebra_76.thy	13
isabelle/test/mathd_algebra_80.thy	12
isabelle/test/mathd_numbertheory_100.thy	14
isabelle/test/mathd_numbertheory_1124.thy	12
isabelle/test/mathd_numbertheory_12.thy	11
isabelle/test/mathd_numbertheory_127.thy	10
isabelle/test/mathd_numbertheory_135.thy	16
isabelle/test/mathd_numbertheory_150.thy	13
isabelle/test/mathd_numbertheory_175.thy	11
isabelle/test/mathd_numbertheory_185.thy	13
isabelle/test/mathd_numbertheory_207.thy	9
isabelle/test/mathd_numbertheory_212.thy	11
isabelle/test/mathd_numbertheory_222.thy	14
isabelle/test/mathd_numbertheory_227.thy	14
isabelle/test/mathd_numbertheory_229.thy	11
isabelle/test/mathd_numbertheory_233.thy	13
isabelle/test/mathd_numbertheory_234.thy	14
isabelle/test/mathd_numbertheory_235.thy	10
isabelle/test/mathd_numbertheory_237.thy	9
isabelle/test/mathd_numbertheory_239.thy	11
isabelle/test/mathd_numbertheory_247.thy	12
isabelle/test/mathd_numbertheory_254.thy	10
isabelle/test/mathd_numbertheory_277.thy	14
isabelle/test/mathd_numbertheory_293.thy	12
isabelle/test/mathd_numbertheory_296.thy	15
isabelle/test/mathd_numbertheory_299.thy	8
isabelle/test/mathd_numbertheory_3.thy	9
isabelle/test/mathd_numbertheory_314.thy	15
isabelle/test/mathd_numbertheory_320.thy	14
isabelle/test/mathd_numbertheory_321.thy	13
isabelle/test/mathd_numbertheory_328.thy	11
isabelle/test/mathd_numbertheory_34.thy	13
isabelle/test/mathd_numbertheory_341.thy	14
isabelle/test/mathd_numbertheory_342.thy	9
isabelle/test/mathd_numbertheory_343.thy	10
isabelle/test/mathd_numbertheory_345.thy	11
isabelle/test/mathd_numbertheory_353.thy	13
isabelle/test/mathd_numbertheory_427.thy	13
isabelle/test/mathd_numbertheory_430.thy	21
isabelle/test/mathd_numbertheory_435.thy	15
isabelle/test/mathd_numbertheory_447.thy	11
isabelle/test/mathd_numbertheory_451.thy	13
isabelle/test/mathd_numbertheory_457.thy	13
isabelle/test/mathd_numbertheory_483.thy	14
isabelle/test/mathd_numbertheory_495.thy	14
isabelle/test/mathd_numbertheory_5.thy	13
isabelle/test/mathd_numbertheory_517.thy	10
isabelle/test/mathd_numbertheory_521.thy	16
isabelle/test/mathd_numbertheory_541.thy	15
isabelle/test/mathd_numbertheory_551.thy	11
isabelle/test/mathd_numbertheory_552.thy	13
isabelle/test/mathd_numbertheory_559.thy	15
isabelle/test/mathd_numbertheory_582.thy	14
isabelle/test/mathd_numbertheory_618.thy	14
isabelle/test/mathd_numbertheory_66.thy	10
isabelle/test/mathd_numbertheory_711.thy	15
isabelle/test/mathd_numbertheory_728.thy	11
isabelle/test/mathd_numbertheory_764.thy	16
isabelle/test/mathd_numbertheory_765.thy	14
isabelle/test/mathd_numbertheory_769.thy	9
isabelle/test/mathd_numbertheory_85.thy	10
isabelle/test/mathd_numbertheory_99.thy	12
isabelle/test/numbertheory_2pownm1prime_nprime.thy	13
isabelle/test/numbertheory_3pow2pownm1mod2pownp3eq2pownp2.thy	50
isabelle/test/numbertheory_4x3m7y3neq2003.thy	10
isabelle/test/numbertheory_aoddbdiv4asqpbsqmod8eq1.thy	14
isabelle/test/numbertheory_exk2powkeqapb2mulbpa2_aeq1.thy	14
isabelle/test/numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown.thy	16
isabelle/test/numbertheory_notequiv2i2jasqbsqdiv8.thy	12
isabelle/test/numbertheory_x5neqy2p4.thy	12
lean/src/test.lean	2283
metamath/test/aime-1983-p1.mm	17
metamath/test/aime-1983-p2.mm	12
metamath/test/aime-1983-p3.mm	6
metamath/test/aime-1984-p1.mm	10
metamath/test/aime-1984-p7.mm	10
metamath/test/aime-1987-p5.mm	10
metamath/test/aime-1988-p8.mm	13
metamath/test/aime-1989-p8.mm	17
metamath/test/aime-1990-p15.mm	15
metamath/test/aime-1990-p4.mm	12
metamath/test/aime-1991-p9.mm	11
metamath/test/aime-1994-p3.mm	11
metamath/test/aime-1995-p7.mm	14
metamath/test/aime-1997-p9.mm	11
metamath/test/aime-1999-p11.mm	10
metamath/test/algebra-2varlineareq-fp3zeq11-3tfm1m5zeqn68-feqn10-zeq7.mm	11
metamath/test/algebra-9onxpypzleqsum2onxpy.mm	10
metamath/test/algebra-abpbcpcageq3-sumaonsqrtapbgeq3onsqrt2.mm	11
metamath/test/algebra-absapbon1pabsapbleqsumabsaon1pabsa.mm	9
metamath/test/algebra-absxm1pabsxpabsxp1eqxp2-0leqxleq1.mm	9
metamath/test/algebra-amgm-sum1toneqn-prod1tonleq1.mm	10
metamath/test/algebra-amgm-sumasqdivbgeqsuma.mm	11
metamath/test/algebra-apbmpcneq0-aeq0anbeq0anceq0.mm	15
metamath/test/algebra-apbon2pownleqapownpbpowon2.mm	10
metamath/test/algebra-apbpceq2-abpbcpcaeq1-aleq1on3anbleq1ancleq4on3.mm	14
metamath/test/algebra-bleqa-apbon2msqrtableqambsqon8b.mm	10
metamath/test/algebra-cubrtrp1oncubrtreq3-rcubp1onrcubeq5778.mm	9
metamath/test/algebra-ineq-nto1onlt2m1on.mm	8
metamath/test/algebra-others-exirrpowirrrat.mm	7
metamath/test/algebra-sqineq-at2malt1.mm	8
metamath/test/algebra-sqineq-unitcircatbpabsamblt1.mm	10
metamath/test/algebra-sqineq-unitcircatbpamblt1.mm	10
metamath/test/algebra-sum1onsqrt2to1onsqrt10000lt198.mm	7
metamath/test/amc12-2000-p1.mm	11
metamath/test/amc12-2000-p12.mm	11
metamath/test/amc12-2000-p20.mm	13
metamath/test/amc12-2000-p6.mm	11
metamath/test/amc12-2001-p21.mm	15
metamath/test/amc12-2001-p5.mm	8
metamath/test/amc12a-2002-p13.mm	12
metamath/test/amc12a-2002-p6.mm	8
metamath/test/amc12a-2003-p23.mm	7
metamath/test/amc12a-2003-p5.mm	11
metamath/test/amc12a-2008-p25.mm	13
metamath/test/amc12a-2009-p6.mm	13
metamath/test/amc12a-2009-p7.mm	15
metamath/test/amc12a-2013-p4.mm	7
metamath/test/amc12a-2019-p12.mm	13
metamath/test/amc12a-2020-p10.mm	9
metamath/test/amc12a-2020-p15.mm	11
metamath/test/amc12a-2020-p25.mm	10
metamath/test/amc12a-2020-p4.mm	12
metamath/test/amc12a-2020-p7.mm	15
metamath/test/amc12a-2020-p9.mm	8
metamath/test/amc12a-2021-p12.mm	13
metamath/test/amc12a-2021-p14.mm	7
metamath/test/amc12a-2021-p18.mm	10
metamath/test/amc12a-2021-p19.mm	8
metamath/test/amc12a-2021-p22.mm	7
metamath/test/amc12a-2021-p25.mm	10
metamath/test/amc12a-2021-p3.mm	12
metamath/test/amc12a-2021-p8.mm	12
metamath/test/amc12a-2021-p9.mm	7
metamath/test/amc12b-2002-p19.mm	13
metamath/test/amc12b-2002-p2.mm	8
metamath/test/amc12b-2002-p4.mm	9
metamath/test/amc12b-2002-p7.mm	13
metamath/test/amc12b-2020-p13.mm	7
metamath/test/amc12b-2020-p2.mm	7
metamath/test/amc12b-2020-p21.mm	7
metamath/test/amc12b-2020-p22.mm	8
metamath/test/amc12b-2020-p6.mm	8
metamath/test/amc12b-2021-p1.mm	7
metamath/test/amc12b-2021-p13.mm	7
metamath/test/amc12b-2021-p18.mm	9
metamath/test/amc12b-2021-p3.mm	9
metamath/test/amc12b-2021-p4.mm	10
metamath/test/amc12b-2021-p9.mm	7
metamath/test/imo-1959-p1.mm	8
metamath/test/imo-1960-p2.mm	11
metamath/test/imo-1962-p2.mm	11
metamath/test/imo-1963-p5.mm	7
metamath/test/imo-1964-p2.mm	13
metamath/test/imo-1965-p2.mm	26
metamath/test/imo-1968-p5-1.mm	11
metamath/test/imo-1969-p2.mm	15
metamath/test/imo-1974-p3.mm	8
metamath/test/imo-1977-p6.mm	10
metamath/test/imo-1981-p6.mm	13
metamath/test/imo-1982-p1.mm	14
metamath/test/imo-1983-p6.mm	13
metamath/test/imo-1984-p6.mm	23
metamath/test/imo-1985-p6.mm	12
metamath/test/imo-1992-p1.mm	14
metamath/test/imo-1997-p5.mm	10
metamath/test/imo-2001-p6.mm	15
metamath/test/imo-2007-p6.mm	9
metamath/test/imo-2019-p1.mm	8
metamath/test/induction-11div10tonmn1ton.mm	8
metamath/test/induction-12dvd4expnp1p20.mm	8
metamath/test/induction-1pxpownlt1pnx.mm	10
metamath/test/induction-nfactltnexpnm1ngt3.mm	8
metamath/test/induction-pord1p1on2powklt5on2.mm	8
metamath/test/induction-pprime-pdvdapowpma.mm	9
metamath/test/induction-prod1p1onk3le3m1onn.mm	8
metamath/test/induction-sumkexp3eqsumksqsq.mm	8
metamath/test/mathd-algebra-107.mm	10
metamath/test/mathd-algebra-113.mm	8
metamath/test/mathd-algebra-114.mm	8
metamath/test/mathd-algebra-125.mm	11
metamath/test/mathd-algebra-129.mm	10
metamath/test/mathd-algebra-137.mm	9
metamath/test/mathd-algebra-139.mm	8
metamath/test/mathd-algebra-141.mm	11
metamath/test/mathd-algebra-142.mm	11
metamath/test/mathd-algebra-143.mm	11
metamath/test/mathd-algebra-148.mm	10
metamath/test/mathd-algebra-153.mm	8
metamath/test/mathd-algebra-156.mm	14
metamath/test/mathd-algebra-158.mm	9
metamath/test/mathd-algebra-160.mm	11
metamath/test/mathd-algebra-17.mm	9
metamath/test/mathd-algebra-170.mm	7
metamath/test/mathd-algebra-171.mm	8
metamath/test/mathd-algebra-176.mm	8
metamath/test/mathd-algebra-184.mm	11
metamath/test/mathd-algebra-188.mm	4
metamath/test/mathd-algebra-196.mm	8
metamath/test/mathd-algebra-208.mm	7
metamath/test/mathd-algebra-209.mm	5
metamath/test/mathd-algebra-215.mm	8
metamath/test/mathd-algebra-24.mm	9
metamath/test/mathd-algebra-246.mm	11
metamath/test/mathd-algebra-263.mm	10
metamath/test/mathd-algebra-270.mm	8
metamath/test/mathd-algebra-275.mm	9
metamath/test/mathd-algebra-276.mm	11
metamath/test/mathd-algebra-288.mm	15
metamath/test/mathd-algebra-289.mm	14
metamath/test/mathd-algebra-293.mm	8
metamath/test/mathd-algebra-296.mm	7
metamath/test/mathd-algebra-302.mm	7
metamath/test/mathd-algebra-304.mm	7
metamath/test/mathd-algebra-313.mm	13
metamath/test/mathd-algebra-314.mm	9
metamath/test/mathd-algebra-320.mm	13
metamath/test/mathd-algebra-329.mm	11
metamath/test/mathd-algebra-33.mm	12
metamath/test/mathd-algebra-332.mm	11
metamath/test/mathd-algebra-338.mm	13
metamath/test/mathd-algebra-342.mm	11
metamath/test/mathd-algebra-346.mm	11
metamath/test/mathd-algebra-354.mm	11
metamath/test/mathd-algebra-359.mm	9
metamath/test/mathd-algebra-362.mm	11
metamath/test/mathd-algebra-388.mm	12
metamath/test/mathd-algebra-392.mm	9
metamath/test/mathd-algebra-398.mm	12
metamath/test/mathd-algebra-400.mm	9
metamath/test/mathd-algebra-412.mm	11
metamath/test/mathd-algebra-419.mm	11
metamath/test/mathd-algebra-427.mm	13
metamath/test/mathd-algebra-432.mm	8
metamath/test/mathd-algebra-44.mm	11
metamath/test/mathd-algebra-440.mm	9
metamath/test/mathd-algebra-441.mm	9
metamath/test/mathd-algebra-452.mm	12
metamath/test/mathd-algebra-459.mm	15
metamath/test/mathd-algebra-478.mm	13
metamath/test/mathd-algebra-484.mm	7
metamath/test/mathd-algebra-487.mm	15
metamath/test/mathd-algebra-513.mm	11
metamath/test/mathd-algebra-598.mm	15
metamath/test/mathd-algebra-756.mm	11
metamath/test/mathd-algebra-76.mm	10
metamath/test/mathd-algebra-80.mm	10
metamath/test/mathd-numbertheory-100.mm	10
metamath/test/mathd-numbertheory-1124.mm	9
metamath/test/mathd-numbertheory-12.mm	7
metamath/test/mathd-numbertheory-127.mm	7
metamath/test/mathd-numbertheory-135.mm	15
metamath/test/mathd-numbertheory-150.mm	9
metamath/test/mathd-numbertheory-175.mm	7
metamath/test/mathd-numbertheory-185.mm	9
metamath/test/mathd-numbertheory-207.mm	7
metamath/test/mathd-numbertheory-212.mm	7
metamath/test/mathd-numbertheory-222.mm	10
metamath/test/mathd-numbertheory-227.mm	11
metamath/test/mathd-numbertheory-229.mm	7
metamath/test/mathd-numbertheory-233.mm	10
metamath/test/mathd-numbertheory-234.mm	10
metamath/test/mathd-numbertheory-235.mm	7
metamath/test/mathd-numbertheory-237.mm	7
metamath/test/mathd-numbertheory-239.mm	7
metamath/test/mathd-numbertheory-247.mm	9
metamath/test/mathd-numbertheory-254.mm	7
metamath/test/mathd-numbertheory-277.mm	11
metamath/test/mathd-numbertheory-293.mm	9
metamath/test/mathd-numbertheory-296.mm	11
metamath/test/mathd-numbertheory-299.mm	7
metamath/test/mathd-numbertheory-3.mm	7
metamath/test/mathd-numbertheory-314.mm	11
metamath/test/mathd-numbertheory-320.mm	10
metamath/test/mathd-numbertheory-321.mm	10
metamath/test/mathd-numbertheory-328.mm	7
metamath/test/mathd-numbertheory-34.mm	10
metamath/test/mathd-numbertheory-341.mm	11
metamath/test/mathd-numbertheory-342.mm	7
metamath/test/mathd-numbertheory-343.mm	7
metamath/test/mathd-numbertheory-345.mm	7
metamath/test/mathd-numbertheory-353.mm	8
metamath/test/mathd-numbertheory-427.mm	9
metamath/test/mathd-numbertheory-430.mm	16
metamath/test/mathd-numbertheory-435.mm	11
metamath/test/mathd-numbertheory-447.mm	7
metamath/test/mathd-numbertheory-451.mm	7
metamath/test/mathd-numbertheory-457.mm	9
metamath/test/mathd-numbertheory-483.mm	11
metamath/test/mathd-numbertheory-495.mm	12
metamath/test/mathd-numbertheory-5.mm	11
metamath/test/mathd-numbertheory-517.mm	7
metamath/test/mathd-numbertheory-521.mm	11
metamath/test/mathd-numbertheory-541.mm	12
metamath/test/mathd-numbertheory-551.mm	7
metamath/test/mathd-numbertheory-552.mm	7
metamath/test/mathd-numbertheory-559.mm	12
metamath/test/mathd-numbertheory-582.mm	9
metamath/test/mathd-numbertheory-618.mm	10
metamath/test/mathd-numbertheory-66.mm	7
metamath/test/mathd-numbertheory-711.mm	11
metamath/test/mathd-numbertheory-728.mm	7
metamath/test/mathd-numbertheory-764.mm	11
metamath/test/mathd-numbertheory-765.mm	10
metamath/test/mathd-numbertheory-769.mm	7
metamath/test/mathd-numbertheory-85.mm	7
metamath/test/mathd-numbertheory-99.mm	9
metamath/test/numbertheory-2pownm1prime-nprime.mm	9
metamath/test/numbertheory-3pow2pownm1mod2pownp3eq2pownp2.mm	8
metamath/test/numbertheory-4x3m7y3neq2003.mm	9
metamath/test/numbertheory-aoddbdiv4asqpbsqmod8eq1.mm	10
metamath/test/numbertheory-exk2powkeqapb2mulbpa2-aeq1.mm	10
metamath/test/numbertheory-fxeq4powxp6powxp9powx-f2powmdvdf2pown.mm	11
metamath/test/numbertheory-notequiv2i2jasqbsqdiv8.mm	7
metamath/test/numbertheory-x5neqy2p4.mm	9