Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute
import
import_segment "hol4"
def_maps
"VB" > "VB_def"
"NBWORD" > "NBWORD_def"
"BV" > "BV_def"
"BNVAL" > "BNVAL_def"
const_maps
"VB" > "HOL4Vec.bword_num.VB"
"NBWORD" > "HOL4Vec.bword_num.NBWORD"
"BV" > "HOL4Vec.bword_num.BV"
thm_maps
"ZERO_WORD_VAL" > "HOL4Vec.bword_num.ZERO_WORD_VAL"
"WSPLIT_NBWORD_0" > "HOL4Vec.bword_num.WSPLIT_NBWORD_0"
"WSEG_NBWORD_SUC" > "HOL4Vec.bword_num.WSEG_NBWORD_SUC"
"WSEG_NBWORD" > "HOL4Vec.bword_num.WSEG_NBWORD"
"WORDLEN_NBWORD" > "HOL4Vec.bword_num.WORDLEN_NBWORD"
"WCAT_NBWORD_0" > "HOL4Vec.bword_num.WCAT_NBWORD_0"
"VB_def" > "HOL4Vec.bword_num.VB_def"
"VB_DEF" > "HOL4Vec.bword_num.VB_DEF"
"VB_BV" > "HOL4Vec.bword_num.VB_BV"
"PWORDLEN_NBWORD" > "HOL4Vec.bword_num.PWORDLEN_NBWORD"
"NBWORD_def" > "HOL4Vec.bword_num.NBWORD_def"
"NBWORD_SUC_WSEG" > "HOL4Vec.bword_num.NBWORD_SUC_WSEG"
"NBWORD_SUC_FST" > "HOL4Vec.bword_num.NBWORD_SUC_FST"
"NBWORD_SUC" > "HOL4Vec.bword_num.NBWORD_SUC"
"NBWORD_SPLIT" > "HOL4Vec.bword_num.NBWORD_SPLIT"
"NBWORD_MOD" > "HOL4Vec.bword_num.NBWORD_MOD"
"NBWORD_DEF" > "HOL4Vec.bword_num.NBWORD_DEF"
"NBWORD_BNVAL" > "HOL4Vec.bword_num.NBWORD_BNVAL"
"NBWORD0" > "HOL4Vec.bword_num.NBWORD0"
"MSB_NBWORD" > "HOL4Vec.bword_num.MSB_NBWORD"
"EQ_NBWORD0_SPLIT" > "HOL4Vec.bword_num.EQ_NBWORD0_SPLIT"
"DOUBL_EQ_SHL" > "HOL4Vec.bword_num.DOUBL_EQ_SHL"
"BV_def" > "HOL4Vec.bword_num.BV_def"
"BV_VB" > "HOL4Vec.bword_num.BV_VB"
"BV_LESS_2" > "HOL4Vec.bword_num.BV_LESS_2"
"BV_DEF" > "HOL4Vec.bword_num.BV_DEF"
"BNVAL_WCAT2" > "HOL4Vec.bword_num.BNVAL_WCAT2"
"BNVAL_WCAT1" > "HOL4Vec.bword_num.BNVAL_WCAT1"
"BNVAL_WCAT" > "HOL4Vec.bword_num.BNVAL_WCAT"
"BNVAL_ONTO" > "HOL4Vec.bword_num.BNVAL_ONTO"
"BNVAL_NVAL" > "HOL4Vec.bword_num.BNVAL_NVAL"
"BNVAL_NBWORD" > "HOL4Vec.bword_num.BNVAL_NBWORD"
"BNVAL_MAX" > "HOL4Vec.bword_num.BNVAL_MAX"
"BNVAL_DEF" > "HOL4Vec.bword_num.BNVAL_DEF"
"BNVAL_11" > "HOL4Vec.bword_num.BNVAL_11"
"BNVAL0" > "HOL4Vec.bword_num.BNVAL0"
"BIT_NBWORD0" > "HOL4Vec.bword_num.BIT_NBWORD0"
"ADD_BNVAL_SPLIT" > "HOL4Vec.bword_num.ADD_BNVAL_SPLIT"
"ADD_BNVAL_RIGHT" > "HOL4Vec.bword_num.ADD_BNVAL_RIGHT"
"ADD_BNVAL_LEFT" > "HOL4Vec.bword_num.ADD_BNVAL_LEFT"
end