Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute
import
import_segment "hol4"
def_maps
"STL" > "STL_primdef"
"STAKE" > "STAKE_primdef"
"SHD" > "SHD_primdef"
"SDROP" > "SDROP_primdef"
"SDEST" > "SDEST_primdef"
"SCONST" > "SCONST_primdef"
"SCONS" > "SCONS_primdef"
const_maps
"STL" > "HOL4Prob.boolean_sequence.STL"
"SHD" > "HOL4Prob.boolean_sequence.SHD"
"SDEST" > "HOL4Prob.boolean_sequence.SDEST"
"SCONST" > "HOL4Prob.boolean_sequence.SCONST"
thm_maps
"STL_primdef" > "HOL4Prob.boolean_sequence.STL_primdef"
"STL_def" > "HOL4Prob.boolean_sequence.STL_def"
"STL_SCONST" > "HOL4Prob.boolean_sequence.STL_SCONST"
"STL_SCONS" > "HOL4Prob.boolean_sequence.STL_SCONS"
"STAKE_def" > "HOL4Prob.boolean_sequence.STAKE_def"
"SHD_primdef" > "HOL4Prob.boolean_sequence.SHD_primdef"
"SHD_def" > "HOL4Prob.boolean_sequence.SHD_def"
"SHD_STL_ISO" > "HOL4Prob.boolean_sequence.SHD_STL_ISO"
"SHD_SCONST" > "HOL4Prob.boolean_sequence.SHD_SCONST"
"SHD_SCONS" > "HOL4Prob.boolean_sequence.SHD_SCONS"
"SDROP_def" > "HOL4Prob.boolean_sequence.SDROP_def"
"SDEST_primdef" > "HOL4Prob.boolean_sequence.SDEST_primdef"
"SDEST_def" > "HOL4Prob.boolean_sequence.SDEST_def"
"SCONS_def" > "HOL4Prob.boolean_sequence.SCONS_def"
"SCONS_SURJ" > "HOL4Prob.boolean_sequence.SCONS_SURJ"
"SCONST_primdef" > "HOL4Prob.boolean_sequence.SCONST_primdef"
"SCONST_def" > "HOL4Prob.boolean_sequence.SCONST_def"
end