Training in progress, step 500

model.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:19b70ab5a45d6f4fb861c78c43d1cd27ba586b861dbc3ed9e93c5fdf27e0aefc
+oid sha256:30355f480594f0030a13b7f3ef78b382fafc4fce645a64c345162b8f85378e43
 size 328693404

runs/Jan10_01-10-02_e28f27bc0ed8/events.out.tfevents.1704849002.e28f27bc0ed8.222.0

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:2c11db177a4c7663725e3bdd9e6c06bdf08ba29118799bbb6f4ba5869ca79d05
+size 4575

tokenizer.json

@@ -67,478 +67,321 @@
       "<unk>": 3,
       "<mask>": 4,
       ".": 5,
-      "0": 6,
-      "1": 7,
-      "2": 8,
-      "3": 9,
-      "5": 10,
-      "6": 11,
-      "_": 12,
-      "a": 13,
-      "b": 14,
-      "c": 15,
-      "d": 16,
-      "e": 17,
-      "f": 18,
-      "g": 19,
-      "h": 20,
-      "i": 21,
-      "j": 22,
-      "l": 23,
-      "m": 24,
-      "n": 25,
-      "o": 26,
-      "p": 27,
-      "q": 28,
-      "r": 29,
-      "s": 30,
-      "t": 31,
-      "u": 32,
-      "v": 33,
-      "w": 34,
-      "x": 35,
-      "y": 36,
-      "##x": 37,
-      "##t": 38,
-      "##r": 39,
-      "##e": 40,
-      "##a": 41,
-      "##l": 42,
-      "##_": 43,
-      "##d": 44,
-      "##f": 45,
-      "##v": 46,
-      "##n": 47,
-      "##s": 48,
-      "##m": 49,
-      "##w": 50,
-      "##i": 51,
-      "##c": 52,
-      "##o": 53,
-      "##b": 54,
-      "##p": 55,
-      "##u": 56,
-      "##g": 57,
-      "##2": 58,
-      "##h": 59,
-      "##y": 60,
-      "##.": 61,
-      "##5": 62,
-      "##j": 63,
-      "##1": 64,
-      "##0": 65,
-      "##3": 66,
-      "##6": 67,
-      "##q": 68,
-      "##_t": 69,
-      "##ac": 70,
-      "##_tac": 71,
-      "##ef": 72,
-      "##_d": 73,
-      "##_def": 74,
-      "##re": 75,
-      "##in": 76,
-      "##al": 77,
-      "##al_": 78,
-      "##xt": 79,
-      "##real_": 80,
-      "ext": 81,
-      "extreal_": 82,
-      "lt": 83,
-      "##w_tac": 84,
-      "##_in": 85,
-      "##ft": 86,
-      "##fty": 87,
-      "##le": 88,
-      "##_infty": 89,
-      "##et": 90,
-      "rw_tac": 91,
-      "##is": 92,
-      "##an": 93,
-      "##_s": 94,
-      "met": 95,
-      "##is_tac": 96,
-      "metis_tac": 97,
-      "##ran": 98,
-      "##_tran": 99,
-      "##_trans": 100,
-      "extreal_m": 101,
-      "##lt": 102,
-      "##ax": 103,
-      "##en": 104,
-      "##lt_def": 105,
-      "##_le": 106,
-      "##te": 107,
-      "##le_def": 108,
-      "##ore": 109,
-      "d_": 110,
-      "lt_le": 111,
-      "lt_infty": 112,
-      "extreal_lt_def": 113,
-      "extreal_le_def": 114,
-      "##on": 115,
-      "##im": 116,
-      "##ot": 117,
-      "##ite": 118,
-      "##ion": 119,
-      "##ch": 120,
-      "##in_def": 121,
-      "##isch": 122,
-      "extreal_min_def": 123,
-      "##isch_tac": 124,
-      "min": 125,
-      "max": 126,
-      "##e_trans": 127,
-      "lte_trans": 128,
-      "max_infty": 129,
-      "let": 130,
-      "##_tot": 131,
-      "lt_tot": 132,
-      "min_infty": 133,
-      "let_trans": 134,
-      "lt_total": 135,
-      "disch_tac": 136,
-      "##_sim": 137,
-      "##rite": 138,
-      "##write": 139,
-      "##p_tac": 140,
-      "##write_tac": 141,
-      "sr": 142,
-      "##bef": 143,
-      "srw_tac": 144,
-      "##before": 145,
-      "gs": 146,
-      "extreal_max": 147,
-      "extreal_max_def": 148,
-      "##tion": 149,
-      "##e_": 150,
-      "##ec": 151,
-      "##pec": 152,
-      "##ation": 153,
-      "##fi": 154,
-      "##ifi": 155,
-      "##cation": 156,
-      "gspec": 157,
-      "##ification": 158,
-      "gspecification": 159,
-      "##before_def": 160,
-      "th": 161,
-      "then": 162,
-      "##ul": 163,
-      "then1": 164,
-      "##ts": 165,
-      "##ven": 166,
-      "##d_s": 167,
-      "st": 168,
-      "##pac": 169,
-      "##d_ss": 170,
-      "std_ss": 171,
-      "##or": 172,
-      "##and": 173,
-      "##pace": 174,
-      "ful": 175,
-      "##l_sim": 176,
-      "full_sim": 177,
-      "full_simp_tac": 178,
-      "##ab": 179,
-      "##_re": 180,
-      "##_rewrite_tac": 181,
-      "##as": 182,
-      "##_space": 183,
-      "##_e": 184,
-      "##ep": 185,
-      "##s_def": 186,
-      "##ets_def": 187,
-      "##orel": 188,
-      "d_and": 189,
-      "d_and_def": 190,
-      "##able": 191,
-      "##vents": 192,
-      "##_space_def": 193,
-      "events": 194,
-      "d_before_def": 195,
-      "d_or": 196,
-      "d_or_def": 197,
-      "re": 198,
-      "##ar": 199,
-      "##_n": 200,
-      "##cl": 201,
-      "in": 202,
-      "##rable": 203,
-      "##eas": 204,
-      "##us": 205,
-      "##urable": 206,
-      "##clus": 207,
-      "##easurable": 208,
-      "##_inclus": 209,
-      "d_sim": 210,
-      "d_inclus": 211,
-      "##_v": 212,
-      "##ve_": 213,
-      "##ive_": 214,
-      "##ult_def": 215,
-      "rewrite_tac": 216,
-      "d_simult_def": 217,
-      "d_inclusive_": 218,
-      "##_var": 219,
-      "d_inclusive_before_def": 220,
-      "##m_rewrite_tac": 221,
-      "as": 222,
-      "mp_tac": 223,
-      "##sion": 224,
-      "exten": 225,
-      "extension": 226,
-      "lb": 227,
-      "measurable": 228,
-      "##f_n": 229,
-      "##m_def": 230,
-      "##of_n": 231,
-      "##um_def": 232,
-      "extreal_of_n": 233,
-      "##_sets_def": 234,
-      "lborel": 235,
-      "measurable_sets_def": 236,
-      "extreal_of_num_def": 237,
-      "le": 238,
-      "le_": 239,
-      "p_space_def": 240,
-      "q.": 241,
-      "##inite": 242,
-      "le_infty": 243,
-      "le_lt": 244,
-      "##dep": 245,
-      "indep": 246,
-      "indep_var": 247,
-      "##xis": 248,
-      "##exis": 249,
-      "##ts_tac": 250,
-      "asm_rewrite_tac": 251,
-      "q.exis": 252,
-      "q.exists_tac": 253,
-      "dft": 254,
-      "dep": 255,
-      "extreal_real_": 256,
-      "##vent": 257,
-      "##_event": 258,
-      "dep_rewrite_tac": 259,
-      "##ub": 260,
-      "##ter": 261,
-      "borel": 262,
-      "sub": 263,
-      "##sets_def": 264,
-      "##ma": 265,
-      "##_inter": 266,
-      "dft_event": 267,
-      "extreal_real_le": 268,
-      "subsets_def": 269,
-      "finite": 270,
-      "m_space_def": 271,
-      "nor": 272,
-      "##mal_": 273,
-      "##ing": 274,
-      "events_def": 275,
-      "normal_": 276,
-      "##ct": 277,
-      "##om": 278,
-      "##real": 279,
-      "##_sing": 280,
-      "gen": 281,
-      "pr": 282,
-      "##lim": 283,
-      "##hm": 284,
-      "##_thm": 285,
-      "##_elim": 286,
-      "normal_real": 287,
-      "gen_tac": 288,
-      "pro": 289,
-      "##ig": 290,
-      "events_inter": 291,
-      "indep_vars": 292,
-      "et": 293,
-      "se": 294,
-      "sig": 295,
-      "##ag": 296,
-      "##a_thm": 297,
-      "##_c": 298,
-      "##nd": 299,
-      "##lect": 300,
-      "##et_tac": 301,
-      "##imag": 302,
-      "##ot_infty": 303,
-      "##ma_def": 304,
-      "dft_event_def": 305,
-      "finite_sing": 306,
-      "##_elim_tac": 307,
-      "eta_thm": 308,
-      "select": 309,
-      "sigma_def": 310,
-      "select_elim_tac": 311,
-      "eq": 312,
-      "##_m": 313,
-      "##ve": 314,
-      "##un": 315,
-      "prob": 316,
-      "eq_tac": 317,
-      "on": 318,
-      "rand": 319,
-      "space": 320,
-      "und": 321,
-      "##table": 322,
-      "##_before": 323,
-      "##finite": 324,
-      "##iab": 325,
-      "##ce_": 326,
-      "##oun": 327,
-      "##gt": 328,
-      "##reimag": 329,
-      "##ist": 330,
-      "##asm_rewrite_tac": 331,
-      "events_space": 332,
-      "in_m": 333,
-      "##_variab": 334,
-      "lborel_le": 335,
-      "##om_variab": 336,
-      "prob_": 337,
-      "once_": 338,
-      "random_variab": 339,
-      "space_def": 340,
-      "undisch_tac": 341,
-      "##ountable": 342,
-      "in_measurable": 343,
-      "once_asm_rewrite_tac": 344,
-      "random_variable_def": 345,
-      "##_p": 346,
-      "##_as": 347,
-      "##dd": 348,
-      "##so": 349,
-      "##m_s": 350,
-      "extreal_le": 351,
-      "##_eq": 352,
-      "asm_s": 353,
-      "##gt0": 354,
-      "##_asso": 355,
-      "extreal_le_eq": 356,
-      "asm_set_tac": 357,
-      "##_assoc": 358,
-      "cd": 359,
-      "mul": 360,
-      "ne": 361,
-      "pi": 362,
-      "preimag": 363,
-      "##r_def": 364,
-      "##ext": 365,
-      "##e_le": 366,
-      "##_gt0": 367,
-      "##f_def": 368,
-      "##not_infty": 369,
-      "##ym": 370,
-      "extreal_mul": 371,
-      "gsym": 372,
-      "##_not_infty": 373,
-      "##omm": 374,
-      "##_countable": 375,
-      "##_comm": 376,
-      "##ver_def": 377,
-      "prob_finite": 378,
-      "cdf_def": 379,
-      "never_def": 380,
-      "pie_le": 381,
-      "extreal_mul_def": 382,
-      "pie_lem": 383,
-      "al": 384,
-      "add": 385,
-      "con": 386,
-      "car": 387,
-      "ps": 388,
-      "##l_d": 389,
-      "##_and": 390,
-      "##se": 391,
-      "##inct": 392,
-      "extreal_not_infty": 393,
-      "##e_ext": 394,
-      "dft_event_and": 395,
-      "prove": 396,
-      "##istinct": 397,
-      "preimage_ext": 398,
-      "pie_lemma": 399,
-      "all_d": 400,
-      "conj": 401,
-      "pset_tac": 402,
-      "dft_event_and_before": 403,
-      "preimage_extreal_": 404,
-      "all_distinct": 405,
-      "and": 406,
-      "countable": 407,
-      "dist": 408,
-      "ima": 409,
-      "me": 410,
-      "not": 411,
-      "po": 412,
-      "rv": 413,
-      "##ty": 414,
-      "##rv": 415,
-      "##ri": 416,
-      "##r_thm": 417,
-      "##ai": 418,
-      "##add": 419,
-      "##_l": 420,
-      "##_imag": 421,
-      "##ss": 422,
-      "##mp": 423,
-      "##mul": 424,
-      "##ose": 425,
-      "##bu": 426,
-      "##ge_": 427,
-      "##2rv": 428,
-      "##infty": 429,
-      "##al_ss": 430,
-      "##real_mul": 431,
-      "##real_2rv": 432,
-      "##ispec": 433,
-      "min_comm": 434,
-      "##tion_def": 435,
-      "##_emp": 436,
-      "events_countable": 437,
-      "real": 438,
-      "real_ss": 439,
-      "##_ninfty": 440,
-      "in_elim": 441,
-      "q.ispec": 442,
-      "dft_before": 443,
-      "extreal_real_lt": 444,
-      "##_event_gt0": 445,
-      "finite_def": 446,
-      "finite_countable": 447,
-      "normal_real_mul": 448,
-      "##_sing_emp": 449,
-      "##_preimag": 450,
-      "##_pai": 451,
-      "mul_not_infty": 452,
-      "##_gt0_ninfty": 453,
-      "add_assoc": 454,
-      "card": 455,
-      "conj_assoc": 456,
-      "dft_event_and_before_preimag": 457,
-      "preimage_extreal_real_2rv": 458,
-      "and_inter": 459,
-      "countable_imag": 460,
-      "distri": 461,
-      "image_": 462,
-      "mem": 463,
-      "not_sing_emp": 464,
-      "rv_gt0_ninfty": 465,
-      "##osed": 466,
-      "##bution_def": 467,
-      "events_countable_inter": 468,
-      "in_elim_pai": 469,
-      "q.ispecl": 470,
-      "dft_before_event_gt0": 471,
-      "countable_image": 472,
-      "distribution_def": 473,
-      "image_finite": 474,
-      "not_sing_empty": 475,
-      "rv_gt0_ninfty_def": 476,
-      "in_elim_pair_thm": 477
+      "1": 6,
+      "2": 7,
+      "A": 8,
+      "B": 9,
+      "C": 10,
+      "D": 11,
+      "E": 12,
+      "F": 13,
+      "G": 14,
+      "H": 15,
+      "I": 16,
+      "J": 17,
+      "K": 18,
+      "L": 19,
+      "M": 20,
+      "N": 21,
+      "O": 22,
+      "P": 23,
+      "Q": 24,
+      "R": 25,
+      "S": 26,
+      "T": 27,
+      "U": 28,
+      "V": 29,
+      "W": 30,
+      "X": 31,
+      "Y": 32,
+      "_": 33,
+      "##I": 34,
+      "##M": 35,
+      "##P": 36,
+      "##_": 37,
+      "##T": 38,
+      "##A": 39,
+      "##C": 40,
+      "##E": 41,
+      "##S": 42,
+      "##U": 43,
+      "##F": 44,
+      "##J": 45,
+      "##2": 46,
+      "##O": 47,
+      "##N": 48,
+      "##D": 49,
+      "##R": 50,
+      "##W": 51,
+      "##H": 52,
+      "##G": 53,
+      "##L": 54,
+      "##B": 55,
+      "##1": 56,
+      "##V": 57,
+      "##Y": 58,
+      "##Q": 59,
+      "##.": 60,
+      "##X": 61,
+      "##_T": 62,
+      "##AC": 63,
+      "##_TAC": 64,
+      "##P_TAC": 65,
+      "##E_TAC": 66,
+      "##RI": 67,
+      "##MP_TAC": 68,
+      "##EW": 69,
+      "##RIT": 70,
+      "##EWRIT": 71,
+      "##EWRITE_TAC": 72,
+      "##W_TAC": 73,
+      "##IMP_TAC": 74,
+      "AS": 75,
+      "##AS": 76,
+      "##IS": 77,
+      "##CH": 78,
+      "##M_": 79,
+      "ASM_": 80,
+      "REWRITE_TAC": 81,
+      "##SIMP_TAC": 82,
+      "RW_TAC": 83,
+      "##SU": 84,
+      "##S_TAC": 85,
+      "##ON": 86,
+      "##SUM": 87,
+      "ST": 88,
+      "STRI": 89,
+      "##EN": 90,
+      "##REWRITE_TAC": 91,
+      "STRIP_TAC": 92,
+      "##P_": 93,
+      "SR": 94,
+      "SRW_TAC": 95,
+      "MP_TAC": 96,
+      "PR": 97,
+      "##OV": 98,
+      "PROV": 99,
+      "PROVE_TAC": 100,
+      "CAS": 101,
+      "##LL": 102,
+      "##AT": 103,
+      "##ASSUM": 104,
+      "##ATCH": 105,
+      "##ATCH_": 106,
+      "ASM_SIMP_TAC": 107,
+      "Q.": 108,
+      "##ATCH_MP_TAC": 109,
+      "##P_ASSUM": 110,
+      "DIS": 111,
+      "ASM_REWRITE_TAC": 112,
+      "##EN_TAC": 113,
+      "GEN_TAC": 114,
+      "DISCH": 115,
+      "FU": 116,
+      "PO": 117,
+      "SIMP_TAC": 118,
+      "POP_ASSUM": 119,
+      "MATCH_MP_TAC": 120,
+      "##_SIMP_TAC": 121,
+      "##LL_SIMP_TAC": 122,
+      "FULL_SIMP_TAC": 123,
+      "##_ON": 124,
+      "##TS_TAC": 125,
+      "##XIS": 126,
+      "##XISTS_TAC": 127,
+      "CASE": 128,
+      "##S_ON": 129,
+      "CASES_ON": 130,
+      "CON": 131,
+      "##ES_TAC": 132,
+      "##E_": 133,
+      "##EXISTS_TAC": 134,
+      "Q.EXISTS_TAC": 135,
+      "SU": 136,
+      "##ET": 137,
+      "##_TH": 138,
+      "##ST": 139,
+      "##_THEN": 140,
+      "SUB": 141,
+      "##E_REWRITE_TAC": 142,
+      "##EC": 143,
+      "DISCH_TAC": 144,
+      "SUBST": 145,
+      "##CE_REWRITE_TAC": 146,
+      "ASSUM": 147,
+      "ASSUME_TAC": 148,
+      "##1_TAC": 149,
+      "SUBST1_TAC": 150,
+      "ON": 151,
+      "IM": 152,
+      "IMP_": 153,
+      "MET": 154,
+      "##IS_TAC": 155,
+      "ONCE_REWRITE_TAC": 156,
+      "METIS_TAC": 157,
+      "##RES_TAC": 158,
+      "IMP_RES_TAC": 159,
+      "##T_TAC": 160,
+      "##UC": 161,
+      "##V_TAC": 162,
+      "DISCH_THEN": 163,
+      "CONV_TAC": 164,
+      "##ND": 165,
+      "CASE_TAC": 166,
+      "EQ": 167,
+      "IND": 168,
+      "EQ_TAC": 169,
+      "INDUC": 170,
+      "##J_TAC": 171,
+      "CONJ_TAC": 172,
+      "INDUCT_TAC": 173,
+      "##LL_TAC": 174,
+      "DEC": 175,
+      "##ID": 176,
+      "DECID": 177,
+      "DECIDE_TAC": 178,
+      "##PEC": 179,
+      "##SPEC": 180,
+      "Q.SPEC": 181,
+      "Q.SPEC_TAC": 182,
+      "ALL_TAC": 183,
+      "EXISTS_TAC": 184,
+      "RES_TAC": 185,
+      "##AL": 186,
+      "BET": 187,
+      "##A_TAC": 188,
+      "##OAL": 189,
+      "##GOAL": 190,
+      "BETA_TAC": 191,
+      "HO": 192,
+      "##_M": 193,
+      "HO_M": 194,
+      "##GOAL_THEN": 195,
+      "PU": 196,
+      "##CAS": 197,
+      "PUR": 198,
+      "##BGOAL_THEN": 199,
+      "##SUBGOAL_THEN": 200,
+      "Q.SUBGOAL_THEN": 201,
+      "##CASES_TAC": 202,
+      "HO_MATCH_MP_TAC": 203,
+      "##PT_TAC": 204,
+      "##CE": 205,
+      "##CEPT_TAC": 206,
+      "FR": 207,
+      "##PO": 208,
+      "##_PO": 209,
+      "##UL": 210,
+      "##AC_PO": 211,
+      "FRAC_PO": 212,
+      "FRAC_POS_TAC": 213,
+      "##_ASSUM": 214,
+      "RUL": 215,
+      "##E_ON": 216,
+      "STRIP_ASSUM": 217,
+      "##ASSUM_TAC": 218,
+      "##E_ASSUM_TAC": 219,
+      "PURE_ON": 220,
+      "RULE_ASSUM_TAC": 221,
+      "STRIP_ASSUME_TAC": 222,
+      "PURE_ONCE_REWRITE_TAC": 223,
+      "FI": 224,
+      "##_CASES_TAC": 225,
+      "##RST": 226,
+      "FIRST": 227,
+      "MATCH_": 228,
+      "##ATCH_TAC": 229,
+      "HO_MATCH_TAC": 230,
+      "PURE_REWRITE_TAC": 231,
+      "AC": 232,
+      "##T_ON": 233,
+      "##T_CASES_TAC": 234,
+      "##ER": 235,
+      "##RUC": 236,
+      "##ACCEPT_TAC": 237,
+      "ASM_CASES_TAC": 238,
+      "STRUC": 239,
+      "INDUCT_ON": 240,
+      "FIRST_ASSUM": 241,
+      "MATCH_ACCEPT_TAC": 242,
+      "ACCEPT_TAC": 243,
+      "STRUCT_CASES_TAC": 244,
+      "AP": 245,
+      "NT": 246,
+      "##M_TAC": 247,
+      "##_A": 248,
+      "##FF": 249,
+      "CASES_TAC": 250,
+      "SUFF": 251,
+      "SUBST_A": 252,
+      "NTAC": 253,
+      "SUFF_TAC": 254,
+      "SUBST_ALL_TAC": 255,
+      "Q_TAC": 256,
+      "##CON": 257,
+      "##_TER": 258,
+      "SUBGOAL_THEN": 259,
+      "AP_TER": 260,
+      "AP_TERM_TAC": 261,
+      "KN": 262,
+      "UND": 263,
+      "##CE_": 264,
+      "##OW_TAC": 265,
+      "##REWRIT": 266,
+      "##ISCH": 267,
+      "COND": 268,
+      "##E_CON": 269,
+      "ONCE_": 270,
+      "KNOW_TAC": 271,
+      "UNDISCH": 272,
+      "##REWRITE_CON": 273,
+      "ONCE_REWRITE_CON": 274,
+      "UNDISCH_TAC": 275,
+      "ONCE_REWRITE_CONV": 276,
+      "AB": 277,
+      "MA": 278,
+      "RE": 279,
+      "X_": 280,
+      "##PAT": 281,
+      "##_E": 282,
+      "##_X": 283,
+      "##TIS": 284,
+      "##AN": 285,
+      "##EV": 286,
+      "##EV_TAC": 287,
+      "##FL": 288,
+      "##N_E": 289,
+      "##RUL": 290,
+      "##REV_TAC": 291,
+      "##GEN_TAC": 292,
+      "##BREV_TAC": 293,
+      "##YM_": 294,
+      "##Q_TH": 295,
+      "##P_EV": 296,
+      "Q.PAT": 297,
+      "DISJ_TAC": 298,
+      "FUN_E": 299,
+      "SUBGOAL": 300,
+      "SUBST_TAC": 301,
+      "IMP_AN": 302,
+      "FIRST_X": 303,
+      "##ERY": 304,
+      "COND_CASES_TAC": 305,
+      "ABBREV_TAC": 306,
+      "MAP_EV": 307,
+      "REFL": 308,
+      "X_GEN_TAC": 309,
+      "##TISYM_": 310,
+      "##RULE": 311,
+      "##Q_THM": 312,
+      "Q.PAT_ASSUM": 313,
+      "FUN_EQ_THM": 314,
+      "SUBGOAL_TAC": 315,
+      "IMP_ANTISYM_": 316,
+      "FIRST_X_ASSUM": 317,
+      "MAP_EVERY": 318,
+      "REFL_TAC": 319,
+      "IMP_ANTISYM_RULE": 320
     }
   }
 }

training_args.bin

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:578b7db646b1c5db5a6a20397df1572770ad68c1673c3da073a9e3c3c541807e
+oid sha256:79d858d9b645ac6ae3ff446b6a472bb946b43857ab3052e1edcce9029b3c21b7
 size 4283

vocab.txt

@@ -4,475 +4,318 @@
 <unk>
 <mask>
 .
-0
 1
 2
-3
-5
-6
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
 _
-a
-b
-c
-d
-e
-f
-g
-h
-i
-j
-l
-m
-n
-o
-p
-q
-r
-s
-t
-u
-v
-w
-x
-y
-##x
-##t
-##r
-##e
-##a
-##l
+##I
+##M
+##P
 ##_
-##d
-##f
-##v
-##n
-##s
-##m
-##w
-##i
-##c
-##o
-##b
-##p
-##u
-##g
+##T
+##A
+##C
+##E
+##S
+##U
+##F
+##J
 ##2
-##h
-##y
-##.
-##5
-##j
+##O
+##N
+##D
+##R
+##W
+##H
+##G
+##L
+##B
 ##1
-##0
-##3
-##6
-##q
-##_t
-##ac
-##_tac
-##ef
-##_d
-##_def
-##re
-##in
-##al
-##al_
-##xt
-##real_
-ext
-extreal_
-lt
-##w_tac
-##_in
-##ft
-##fty
-##le
-##_infty
-##et
-rw_tac
-##is
-##an
-##_s
-met
-##is_tac
-metis_tac
-##ran
-##_tran
-##_trans
-extreal_m
-##lt
-##ax
-##en
-##lt_def
-##_le
-##te
-##le_def
-##ore
-d_
-lt_le
-lt_infty
-extreal_lt_def
-extreal_le_def
-##on
-##im
-##ot
-##ite
-##ion
-##ch
-##in_def
-##isch
-extreal_min_def
-##isch_tac
-min
-max
-##e_trans
-lte_trans
-max_infty
-let
-##_tot
-lt_tot
-min_infty
-let_trans
-lt_total
-disch_tac
-##_sim
-##rite
-##write
-##p_tac
-##write_tac
-sr
-##bef
-srw_tac
-##before
-gs
-extreal_max
-extreal_max_def
-##tion
-##e_
-##ec
-##pec
-##ation
-##fi
-##ifi
-##cation
-gspec
-##ification
-gspecification
-##before_def
-th
-then
-##ul
-then1
-##ts
-##ven
-##d_s
-st
-##pac
-##d_ss
-std_ss
-##or
-##and
-##pace
-ful
-##l_sim
-full_sim
-full_simp_tac
-##ab
-##_re
-##_rewrite_tac
-##as
-##_space
-##_e
-##ep
-##s_def
-##ets_def
-##orel
-d_and
-d_and_def
-##able
-##vents
-##_space_def
-events
-d_before_def
-d_or
-d_or_def
-re
-##ar
-##_n
-##cl
-in
-##rable
-##eas
-##us
-##urable
-##clus
-##easurable
-##_inclus
-d_sim
-d_inclus
-##_v
-##ve_
-##ive_
-##ult_def
-rewrite_tac
-d_simult_def
-d_inclusive_
-##_var
-d_inclusive_before_def
-##m_rewrite_tac
-as
-mp_tac
-##sion
-exten
-extension
-lb
-measurable
-##f_n
-##m_def
-##of_n
-##um_def
-extreal_of_n
-##_sets_def
-lborel
-measurable_sets_def
-extreal_of_num_def
-le
-le_
-p_space_def
-q.
-##inite
-le_infty
-le_lt
-##dep
-indep
-indep_var
-##xis
-##exis
-##ts_tac
-asm_rewrite_tac
-q.exis
-q.exists_tac
-dft
-dep
-extreal_real_
-##vent
-##_event
-dep_rewrite_tac
-##ub
-##ter
-borel
-sub
-##sets_def
-##ma
-##_inter
-dft_event
-extreal_real_le
-subsets_def
-finite
-m_space_def
-nor
-##mal_
-##ing
-events_def
-normal_
-##ct
-##om
-##real
-##_sing
-gen
-pr
-##lim
-##hm
-##_thm
-##_elim
-normal_real
-gen_tac
-pro
-##ig
-events_inter
-indep_vars
-et
-se
-sig
-##ag
-##a_thm
-##_c
-##nd
-##lect
-##et_tac
-##imag
-##ot_infty
-##ma_def
-dft_event_def
-finite_sing
-##_elim_tac
-eta_thm
-select
-sigma_def
-select_elim_tac
-eq
-##_m
-##ve
-##un
-prob
-eq_tac
-on
-rand
-space
-und
-##table
-##_before
-##finite
-##iab
-##ce_
-##oun
-##gt
-##reimag
-##ist
-##asm_rewrite_tac
-events_space
-in_m
-##_variab
-lborel_le
-##om_variab
-prob_
-once_
-random_variab
-space_def
-undisch_tac
-##ountable
-in_measurable
-once_asm_rewrite_tac
-random_variable_def
-##_p
-##_as
-##dd
-##so
-##m_s
-extreal_le
-##_eq
-asm_s
-##gt0
-##_asso
-extreal_le_eq
-asm_set_tac
-##_assoc
-cd
-mul
-ne
-pi
-preimag
-##r_def
-##ext
-##e_le
-##_gt0
-##f_def
-##not_infty
-##ym
-extreal_mul
-gsym
-##_not_infty
-##omm
-##_countable
-##_comm
-##ver_def
-prob_finite
-cdf_def
-never_def
-pie_le
-extreal_mul_def
-pie_lem
-al
-add
-con
-car
-ps
-##l_d
-##_and
-##se
-##inct
-extreal_not_infty
-##e_ext
-dft_event_and
-prove
-##istinct
-preimage_ext
-pie_lemma
-all_d
-conj
-pset_tac
-dft_event_and_before
-preimage_extreal_
-all_distinct
-and
-countable
-dist
-ima
-me
-not
-po
-rv
-##ty
-##rv
-##ri
-##r_thm
-##ai
-##add
-##_l
-##_imag
-##ss
-##mp
-##mul
-##ose
-##bu
-##ge_
-##2rv
-##infty
-##al_ss
-##real_mul
-##real_2rv
-##ispec
-min_comm
-##tion_def
-##_emp
-events_countable
-real
-real_ss
-##_ninfty
-in_elim
-q.ispec
-dft_before
-extreal_real_lt
-##_event_gt0
-finite_def
-finite_countable
-normal_real_mul
-##_sing_emp
-##_preimag
-##_pai
-mul_not_infty
-##_gt0_ninfty
-add_assoc
-card
-conj_assoc
-dft_event_and_before_preimag
-preimage_extreal_real_2rv
-and_inter
-countable_imag
-distri
-image_
-mem
-not_sing_emp
-rv_gt0_ninfty
-##osed
-##bution_def
-events_countable_inter
-in_elim_pai
-q.ispecl
-dft_before_event_gt0
-countable_image
-distribution_def
-image_finite
-not_sing_empty
-rv_gt0_ninfty_def
-in_elim_pair_thm
+##V
+##Y
+##Q
+##.
+##X
+##_T
+##AC
+##_TAC
+##P_TAC
+##E_TAC
+##RI
+##MP_TAC
+##EW
+##RIT
+##EWRIT
+##EWRITE_TAC
+##W_TAC
+##IMP_TAC
+AS
+##AS
+##IS
+##CH
+##M_
+ASM_
+REWRITE_TAC
+##SIMP_TAC
+RW_TAC
+##SU
+##S_TAC
+##ON
+##SUM
+ST
+STRI
+##EN
+##REWRITE_TAC
+STRIP_TAC
+##P_
+SR
+SRW_TAC
+MP_TAC
+PR
+##OV
+PROV
+PROVE_TAC
+CAS
+##LL
+##AT
+##ASSUM
+##ATCH
+##ATCH_
+ASM_SIMP_TAC
+Q.
+##ATCH_MP_TAC
+##P_ASSUM
+DIS
+ASM_REWRITE_TAC
+##EN_TAC
+GEN_TAC
+DISCH
+FU
+PO
+SIMP_TAC
+POP_ASSUM
+MATCH_MP_TAC
+##_SIMP_TAC
+##LL_SIMP_TAC
+FULL_SIMP_TAC
+##_ON
+##TS_TAC
+##XIS
+##XISTS_TAC
+CASE
+##S_ON
+CASES_ON
+CON
+##ES_TAC
+##E_
+##EXISTS_TAC
+Q.EXISTS_TAC
+SU
+##ET
+##_TH
+##ST
+##_THEN
+SUB
+##E_REWRITE_TAC
+##EC
+DISCH_TAC
+SUBST
+##CE_REWRITE_TAC
+ASSUM
+ASSUME_TAC
+##1_TAC
+SUBST1_TAC
+ON
+IM
+IMP_
+MET
+##IS_TAC
+ONCE_REWRITE_TAC
+METIS_TAC
+##RES_TAC
+IMP_RES_TAC
+##T_TAC
+##UC
+##V_TAC
+DISCH_THEN
+CONV_TAC
+##ND
+CASE_TAC
+EQ
+IND
+EQ_TAC
+INDUC
+##J_TAC
+CONJ_TAC
+INDUCT_TAC
+##LL_TAC
+DEC
+##ID
+DECID
+DECIDE_TAC
+##PEC
+##SPEC
+Q.SPEC
+Q.SPEC_TAC
+ALL_TAC
+EXISTS_TAC
+RES_TAC
+##AL
+BET
+##A_TAC
+##OAL
+##GOAL
+BETA_TAC
+HO
+##_M
+HO_M
+##GOAL_THEN
+PU
+##CAS
+PUR
+##BGOAL_THEN
+##SUBGOAL_THEN
+Q.SUBGOAL_THEN
+##CASES_TAC
+HO_MATCH_MP_TAC
+##PT_TAC
+##CE
+##CEPT_TAC
+FR
+##PO
+##_PO
+##UL
+##AC_PO
+FRAC_PO
+FRAC_POS_TAC
+##_ASSUM
+RUL
+##E_ON
+STRIP_ASSUM
+##ASSUM_TAC
+##E_ASSUM_TAC
+PURE_ON
+RULE_ASSUM_TAC
+STRIP_ASSUME_TAC
+PURE_ONCE_REWRITE_TAC
+FI
+##_CASES_TAC
+##RST
+FIRST
+MATCH_
+##ATCH_TAC
+HO_MATCH_TAC
+PURE_REWRITE_TAC
+AC
+##T_ON
+##T_CASES_TAC
+##ER
+##RUC
+##ACCEPT_TAC
+ASM_CASES_TAC
+STRUC
+INDUCT_ON
+FIRST_ASSUM
+MATCH_ACCEPT_TAC
+ACCEPT_TAC
+STRUCT_CASES_TAC
+AP
+NT
+##M_TAC
+##_A
+##FF
+CASES_TAC
+SUFF
+SUBST_A
+NTAC
+SUFF_TAC
+SUBST_ALL_TAC
+Q_TAC
+##CON
+##_TER
+SUBGOAL_THEN
+AP_TER
+AP_TERM_TAC
+KN
+UND
+##CE_
+##OW_TAC
+##REWRIT
+##ISCH
+COND
+##E_CON
+ONCE_
+KNOW_TAC
+UNDISCH
+##REWRITE_CON
+ONCE_REWRITE_CON
+UNDISCH_TAC
+ONCE_REWRITE_CONV
+AB
+MA
+RE
+X_
+##PAT
+##_E
+##_X
+##TIS
+##AN
+##EV
+##EV_TAC
+##FL
+##N_E
+##RUL
+##REV_TAC
+##GEN_TAC
+##BREV_TAC
+##YM_
+##Q_TH
+##P_EV
+Q.PAT
+DISJ_TAC
+FUN_E
+SUBGOAL
+SUBST_TAC
+IMP_AN
+FIRST_X
+##ERY
+COND_CASES_TAC
+ABBREV_TAC
+MAP_EV
+REFL
+X_GEN_TAC
+##TISYM_
+##RULE
+##Q_THM
+Q.PAT_ASSUM
+FUN_EQ_THM
+SUBGOAL_TAC
+IMP_ANTISYM_
+FIRST_X_ASSUM
+MAP_EVERY
+REFL_TAC
+IMP_ANTISYM_RULE