|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"ICARRY" > "ICARRY_def"
|
|
|
7 |
"ACARRY" > "ACARRY_def"
|
|
|
8 |
|
|
|
9 |
thm_maps
|
|
|
10 |
"WSEG_NBWORD_ADD" > "HOL4Vec.bword_arith.WSEG_NBWORD_ADD"
|
|
|
11 |
"ICARRY_WSEG" > "HOL4Vec.bword_arith.ICARRY_WSEG"
|
|
|
12 |
"ICARRY_DEF" > "HOL4Vec.bword_arith.ICARRY_DEF"
|
|
|
13 |
"BNVAL_LESS_EQ" > "HOL4Vec.bword_arith.BNVAL_LESS_EQ"
|
|
|
14 |
"ADD_WORD_SPLIT" > "HOL4Vec.bword_arith.ADD_WORD_SPLIT"
|
|
|
15 |
"ADD_NBWORD_EQ0_SPLIT" > "HOL4Vec.bword_arith.ADD_NBWORD_EQ0_SPLIT"
|
|
|
16 |
"ADD_BV_BNVAL_LESS_EQ1" > "HOL4Vec.bword_arith.ADD_BV_BNVAL_LESS_EQ1"
|
|
|
17 |
"ADD_BV_BNVAL_LESS_EQ" > "HOL4Vec.bword_arith.ADD_BV_BNVAL_LESS_EQ"
|
|
|
18 |
"ADD_BV_BNVAL_DIV_LESS_EQ1" > "HOL4Vec.bword_arith.ADD_BV_BNVAL_DIV_LESS_EQ1"
|
|
|
19 |
"ADD_BNVAL_LESS_EQ1" > "HOL4Vec.bword_arith.ADD_BNVAL_LESS_EQ1"
|
|
|
20 |
"ACARRY_WSEG" > "HOL4Vec.bword_arith.ACARRY_WSEG"
|
|
|
21 |
"ACARRY_MSB" > "HOL4Vec.bword_arith.ACARRY_MSB"
|
|
|
22 |
"ACARRY_EQ_ICARRY" > "HOL4Vec.bword_arith.ACARRY_EQ_ICARRY"
|
|
|
23 |
"ACARRY_EQ_ADD_DIV" > "HOL4Vec.bword_arith.ACARRY_EQ_ADD_DIV"
|
|
|
24 |
"ACARRY_DEF" > "HOL4Vec.bword_arith.ACARRY_DEF"
|
|
|
25 |
"ACARRY_ACARRY_WSEG" > "HOL4Vec.bword_arith.ACARRY_ACARRY_WSEG"
|
|
|
26 |
|
|
|
27 |
end
|