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
