Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
BinaryContext
MemSorts
MemState
SimState
executeBinary()
executeCBranch()
executeLoad()
executePopcount()
executeSignExtend()
executeStore()
executeSubpiece()
executeUnary()
executeZeroExtend()
pc_of_addr()
pretty_insn()
pretty_op()
test_pcode()