|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"VB" > "VB_def"
|
|
|
7 |
"NBWORD" > "NBWORD_def"
|
|
|
8 |
"BV" > "BV_def"
|
|
|
9 |
"BNVAL" > "BNVAL_def"
|
|
|
10 |
|
|
|
11 |
const_maps
|
|
|
12 |
"VB" > "HOL4Vec.bword_num.VB"
|
|
|
13 |
"NBWORD" > "HOL4Vec.bword_num.NBWORD"
|
|
|
14 |
"BV" > "HOL4Vec.bword_num.BV"
|
|
|
15 |
|
|
|
16 |
thm_maps
|
|
|
17 |
"ZERO_WORD_VAL" > "HOL4Vec.bword_num.ZERO_WORD_VAL"
|
|
|
18 |
"WSPLIT_NBWORD_0" > "HOL4Vec.bword_num.WSPLIT_NBWORD_0"
|
|
|
19 |
"WSEG_NBWORD_SUC" > "HOL4Vec.bword_num.WSEG_NBWORD_SUC"
|
|
|
20 |
"WSEG_NBWORD" > "HOL4Vec.bword_num.WSEG_NBWORD"
|
|
|
21 |
"WORDLEN_NBWORD" > "HOL4Vec.bword_num.WORDLEN_NBWORD"
|
|
|
22 |
"WCAT_NBWORD_0" > "HOL4Vec.bword_num.WCAT_NBWORD_0"
|
|
|
23 |
"VB_def" > "HOL4Vec.bword_num.VB_def"
|
|
|
24 |
"VB_DEF" > "HOL4Vec.bword_num.VB_DEF"
|
|
|
25 |
"VB_BV" > "HOL4Vec.bword_num.VB_BV"
|
|
|
26 |
"PWORDLEN_NBWORD" > "HOL4Vec.bword_num.PWORDLEN_NBWORD"
|
|
|
27 |
"NBWORD_def" > "HOL4Vec.bword_num.NBWORD_def"
|
|
|
28 |
"NBWORD_SUC_WSEG" > "HOL4Vec.bword_num.NBWORD_SUC_WSEG"
|
|
|
29 |
"NBWORD_SUC_FST" > "HOL4Vec.bword_num.NBWORD_SUC_FST"
|
|
|
30 |
"NBWORD_SUC" > "HOL4Vec.bword_num.NBWORD_SUC"
|
|
|
31 |
"NBWORD_SPLIT" > "HOL4Vec.bword_num.NBWORD_SPLIT"
|
|
|
32 |
"NBWORD_MOD" > "HOL4Vec.bword_num.NBWORD_MOD"
|
|
|
33 |
"NBWORD_DEF" > "HOL4Vec.bword_num.NBWORD_DEF"
|
|
|
34 |
"NBWORD_BNVAL" > "HOL4Vec.bword_num.NBWORD_BNVAL"
|
|
|
35 |
"NBWORD0" > "HOL4Vec.bword_num.NBWORD0"
|
|
|
36 |
"MSB_NBWORD" > "HOL4Vec.bword_num.MSB_NBWORD"
|
|
|
37 |
"EQ_NBWORD0_SPLIT" > "HOL4Vec.bword_num.EQ_NBWORD0_SPLIT"
|
|
|
38 |
"DOUBL_EQ_SHL" > "HOL4Vec.bword_num.DOUBL_EQ_SHL"
|
|
|
39 |
"BV_def" > "HOL4Vec.bword_num.BV_def"
|
|
|
40 |
"BV_VB" > "HOL4Vec.bword_num.BV_VB"
|
|
|
41 |
"BV_LESS_2" > "HOL4Vec.bword_num.BV_LESS_2"
|
|
|
42 |
"BV_DEF" > "HOL4Vec.bword_num.BV_DEF"
|
|
|
43 |
"BNVAL_WCAT2" > "HOL4Vec.bword_num.BNVAL_WCAT2"
|
|
|
44 |
"BNVAL_WCAT1" > "HOL4Vec.bword_num.BNVAL_WCAT1"
|
|
|
45 |
"BNVAL_WCAT" > "HOL4Vec.bword_num.BNVAL_WCAT"
|
|
|
46 |
"BNVAL_ONTO" > "HOL4Vec.bword_num.BNVAL_ONTO"
|
|
|
47 |
"BNVAL_NVAL" > "HOL4Vec.bword_num.BNVAL_NVAL"
|
|
|
48 |
"BNVAL_NBWORD" > "HOL4Vec.bword_num.BNVAL_NBWORD"
|
|
|
49 |
"BNVAL_MAX" > "HOL4Vec.bword_num.BNVAL_MAX"
|
|
|
50 |
"BNVAL_DEF" > "HOL4Vec.bword_num.BNVAL_DEF"
|
|
|
51 |
"BNVAL_11" > "HOL4Vec.bword_num.BNVAL_11"
|
|
|
52 |
"BNVAL0" > "HOL4Vec.bword_num.BNVAL0"
|
|
|
53 |
"BIT_NBWORD0" > "HOL4Vec.bword_num.BIT_NBWORD0"
|
|
|
54 |
"ADD_BNVAL_SPLIT" > "HOL4Vec.bword_num.ADD_BNVAL_SPLIT"
|
|
|
55 |
"ADD_BNVAL_RIGHT" > "HOL4Vec.bword_num.ADD_BNVAL_RIGHT"
|
|
|
56 |
"ADD_BNVAL_LEFT" > "HOL4Vec.bword_num.ADD_BNVAL_LEFT"
|
|
|
57 |
|
|
|
58 |
end
|