Remove cheri and mips specs -- they now have their own repository.

272 files changed, 0 insertions, 1165 deletions

diff --git a/cheri/sail_latexcc/commands.tex b/cheri/sail_latexcc/commands.tex
deleted file mode 100644
index 8b9678a1..00000000
--- a/cheri/sail_latexcc/commands.tex
+++ /dev/null
@@ -1,544 +0,0 @@
-\newcommand{\sailccsailccregderefv}{\label{zregzyderef} \lstinputlisting[language=sail]{sail_latexcc/sailccsailccregderefv.tex}}
-
-\newcommand{\sailccregderef}{\label{zzyregzyderef} \lstinputlisting[language=sail]{sail_latexcc/sailccregderef.tex}}
-
-\newcommand{\sailcceqbittwo}{\label{zeqzybittwo} \lstinputlisting[language=sail]{sail_latexcc/sailcceqbittwo.tex}}
-
-\newcommand{\sailccsailccsailccsailcczeightoperatorzzerozJzJzninevvv}{\label{zzeightoperatorzzerozJzJznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailccsailccsailcczeightoperatorzzerozJzJzninevvv.tex}}
-
-\newcommand{\sailccdiv}{\label{zdiv} \lstinputlisting[language=sail]{sail_latexcc/sailccdiv.tex}}
-
-\newcommand{\sailccsailccsailcczeightoperatorzzerozFzninevv}{\label{zzeightoperatorzzerozFznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailccsailcczeightoperatorzzerozFzninevv.tex}}
-
-\newcommand{\sailccmod}{\label{zmod} \lstinputlisting[language=sail]{sail_latexcc/sailccmod.tex}}
-
-\newcommand{\sailccsailccsailcczeightoperatorzzerozfivezninevv}{\label{zzeightoperatorzzerozfiveznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailccsailcczeightoperatorzzerozfivezninevv.tex}}
-
-\newcommand{\sailccabsatom}{\label{zabszyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccabsatom.tex}}
-
-\newcommand{\sailccnotbool}{\label{znotzybool} \lstinputlisting[language=sail]{sail_latexcc/sailccnotbool.tex}}
-
-\newcommand{\sailccandbool}{\label{zandzybool} \lstinputlisting[language=sail]{sail_latexcc/sailccandbool.tex}}
-
-\newcommand{\sailccorbool}{\label{zorzybool} \lstinputlisting[language=sail]{sail_latexcc/sailccorbool.tex}}
-
-\newcommand{\sailcceqatom}{\label{zeqzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailcceqatom.tex}}
-
-\newcommand{\sailccneqatom}{\label{zneqzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccneqatom.tex}}
-
-\newcommand{\sailccfnneqatom}{\label{zneqzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccfnneqatom.tex}}
-
-\newcommand{\sailcclteqatom}{\label{zlteqzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailcclteqatom.tex}}
-
-\newcommand{\sailccgteqatom}{\label{zgteqzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccgteqatom.tex}}
-
-\newcommand{\sailccltatom}{\label{zltzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccltatom.tex}}
-
-\newcommand{\sailccgtatom}{\label{zgtzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccgtatom.tex}}
-
-\newcommand{\sailccltrangeatom}{\label{zltzyrangezyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccltrangeatom.tex}}
-
-\newcommand{\sailcclteqrangeatom}{\label{zlteqzyrangezyatom} \lstinputlisting[language=sail]{sail_latexcc/sailcclteqrangeatom.tex}}
-
-\newcommand{\sailccgtrangeatom}{\label{zgtzyrangezyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccgtrangeatom.tex}}
-
-\newcommand{\sailccgteqrangeatom}{\label{zgteqzyrangezyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccgteqrangeatom.tex}}
-
-\newcommand{\sailccltatomrange}{\label{zltzyatomzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccltatomrange.tex}}
-
-\newcommand{\sailcclteqatomrange}{\label{zlteqzyatomzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailcclteqatomrange.tex}}
-
-\newcommand{\sailccgtatomrange}{\label{zgtzyatomzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccgtatomrange.tex}}
-
-\newcommand{\sailccgteqatomrange}{\label{zgteqzyatomzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccgteqatomrange.tex}}
-
-\newcommand{\sailcceqrange}{\label{zeqzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailcceqrange.tex}}
-
-\newcommand{\sailcceqint}{\label{zeqzyint} \lstinputlisting[language=sail]{sail_latexcc/sailcceqint.tex}}
-
-\newcommand{\sailcceqbool}{\label{zeqzybool} \lstinputlisting[language=sail]{sail_latexcc/sailcceqbool.tex}}
-
-\newcommand{\sailccneqrange}{\label{zneqzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccneqrange.tex}}
-
-\newcommand{\sailccfnneqrange}{\label{zneqzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccfnneqrange.tex}}
-
-\newcommand{\sailccneqint}{\label{zneqzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccneqint.tex}}
-
-\newcommand{\sailccfnneqint}{\label{zneqzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccfnneqint.tex}}
-
-\newcommand{\sailccneqbool}{\label{zneqzybool} \lstinputlisting[language=sail]{sail_latexcc/sailccneqbool.tex}}
-
-\newcommand{\sailccfnneqbool}{\label{zneqzybool} \lstinputlisting[language=sail]{sail_latexcc/sailccfnneqbool.tex}}
-
-\newcommand{\sailcclteqint}{\label{zlteqzyint} \lstinputlisting[language=sail]{sail_latexcc/sailcclteqint.tex}}
-
-\newcommand{\sailccgteqint}{\label{zgteqzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccgteqint.tex}}
-
-\newcommand{\sailccltint}{\label{zltzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccltint.tex}}
-
-\newcommand{\sailccgtint}{\label{zgtzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccgtint.tex}}
-
-\newcommand{\sailccsailccsailcczeightoperatorzzerozJzJzninevv}{\label{zzeightoperatorzzerozJzJznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailccsailcczeightoperatorzzerozJzJzninevv.tex}}
-
-\newcommand{\sailccsailcczeightoperatorzzerozonezJzninev}{\label{zzeightoperatorzzerozonezJznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozonezJzninev.tex}}
-
-\newcommand{\sailccsailcczeightoperatorzzerozUzninev}{\label{zzeightoperatorzzerozUznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozUzninev.tex}}
-
-\newcommand{\sailccsailcczeightoperatorzzerozsixzninev}{\label{zzeightoperatorzzerozsixznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozsixzninev.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozIzJznine}{\label{zzeightoperatorzzerozIzJznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozIzJznine.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozIznine}{\label{zzeightoperatorzzerozIznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozIznine.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozKzJznine}{\label{zzeightoperatorzzerozKzJznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozKzJznine.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozKznine}{\label{zzeightoperatorzzerozKznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozKznine.tex}}
-
-\newcommand{\sailccaddatom}{\label{zaddzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccaddatom.tex}}
-
-\newcommand{\sailccaddint}{\label{zaddzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccaddint.tex}}
-
-\newcommand{\sailccsailccsailcczeightoperatorzzerozBzninevv}{\label{zzeightoperatorzzerozBznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailccsailcczeightoperatorzzerozBzninevv.tex}}
-
-\newcommand{\sailccsubatom}{\label{zsubzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccsubatom.tex}}
-
-\newcommand{\sailccsubint}{\label{zsubzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccsubint.tex}}
-
-\newcommand{\sailccsailcczeightoperatorzzerozDzninev}{\label{zzeightoperatorzzerozDznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozDzninev.tex}}
-
-\newcommand{\sailccnegateatom}{\label{znegatezyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccnegateatom.tex}}
-
-\newcommand{\sailccnegateint}{\label{znegatezyint} \lstinputlisting[language=sail]{sail_latexcc/sailccnegateint.tex}}
-
-\newcommand{\sailccsailccnegatev}{\label{znegate} \lstinputlisting[language=sail]{sail_latexcc/sailccsailccnegatev.tex}}
-
-\newcommand{\sailccmultatom}{\label{zmultzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccmultatom.tex}}
-
-\newcommand{\sailccmultint}{\label{zmultzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccmultint.tex}}
-
-\newcommand{\sailccsailcczeightoperatorzzerozAzninev}{\label{zzeightoperatorzzerozAznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozAzninev.tex}}
-
-\newcommand{\sailccprintint}{\label{zprintzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccprintint.tex}}
-
-\newcommand{\sailccprerrint}{\label{zprerrzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccprerrint.tex}}
-
-\newcommand{\sailccshlint}{\label{zshlzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccshlint.tex}}
-
-\newcommand{\sailccshrint}{\label{zshrzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccshrint.tex}}
-
-\newcommand{\sailccdivint}{\label{zdivzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccdivint.tex}}
-
-\newcommand{\sailccsailcczeightoperatorzzerozFzninev}{\label{zzeightoperatorzzerozFznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozFzninev.tex}}
-
-\newcommand{\sailccmodint}{\label{zmodzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccmodint.tex}}
-
-\newcommand{\sailccsailcczeightoperatorzzerozfivezninev}{\label{zzeightoperatorzzerozfiveznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozfivezninev.tex}}
-
-\newcommand{\sailccabsint}{\label{zabszyint} \lstinputlisting[language=sail]{sail_latexcc/sailccabsint.tex}}
-
-\newcommand{\sailccisnone}{\label{ziszynone} \lstinputlisting[language=sail]{sail_latexcc/sailccisnone.tex}}
-
-\newcommand{\sailccfnisnone}{\label{ziszynone} \lstinputlisting[language=sail]{sail_latexcc/sailccfnisnone.tex}}
-
-\newcommand{\sailccissome}{\label{ziszysome} \lstinputlisting[language=sail]{sail_latexcc/sailccissome.tex}}
-
-\newcommand{\sailccfnissome}{\label{ziszysome} \lstinputlisting[language=sail]{sail_latexcc/sailccfnissome.tex}}
-
-\newcommand{\sailccbits}{\label{zbits} \lstinputlisting[language=sail]{sail_latexcc/sailccbits.tex}}
-
-\newcommand{\sailcceqbit}{\label{zeqzybit} \lstinputlisting[language=sail]{sail_latexcc/sailcceqbit.tex}}
-
-\newcommand{\sailcceqbits}{\label{zeqzybits} \lstinputlisting[language=sail]{sail_latexcc/sailcceqbits.tex}}
-
-\newcommand{\sailccsailcczeightoperatorzzerozJzJzninev}{\label{zzeightoperatorzzerozJzJznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozJzJzninev.tex}}
-
-\newcommand{\sailccbitvectorlength}{\label{zbitvectorzylength} \lstinputlisting[language=sail]{sail_latexcc/sailccbitvectorlength.tex}}
-
-\newcommand{\sailccvectorlength}{\label{zvectorzylength} \lstinputlisting[language=sail]{sail_latexcc/sailccvectorlength.tex}}
-
-\newcommand{\sailcclength}{\label{zlength} \lstinputlisting[language=sail]{sail_latexcc/sailcclength.tex}}
-
-\newcommand{\sailccsailzzeros}{\label{zsailzyzzeros} \lstinputlisting[language=sail]{sail_latexcc/sailccsailzzeros.tex}}
-
-\newcommand{\sailccprintbits}{\label{zprintzybits} \lstinputlisting[language=sail]{sail_latexcc/sailccprintbits.tex}}
-
-\newcommand{\sailccprerrbits}{\label{zprerrzybits} \lstinputlisting[language=sail]{sail_latexcc/sailccprerrbits.tex}}
-
-\newcommand{\sailccsailsignextend}{\label{zsailzysignzyextend} \lstinputlisting[language=sail]{sail_latexcc/sailccsailsignextend.tex}}
-
-\newcommand{\sailccsailzzeroextend}{\label{zsailzyzzerozyextend} \lstinputlisting[language=sail]{sail_latexcc/sailccsailzzeroextend.tex}}
-
-\newcommand{\sailcctruncate}{\label{ztruncate} \lstinputlisting[language=sail]{sail_latexcc/sailcctruncate.tex}}
-
-\newcommand{\sailccsailmask}{\label{zsailzymask} \lstinputlisting[language=sail]{sail_latexcc/sailccsailmask.tex}}
-
-\newcommand{\sailccfnsailmask}{\label{zsailzymask} \lstinputlisting[language=sail]{sail_latexcc/sailccfnsailmask.tex}}
-
-\newcommand{\sailccsailcczeightoperatorzzerozQzninev}{\label{zzeightoperatorzzerozQznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozQzninev.tex}}
-
-\newcommand{\sailccbitvectorconcat}{\label{zbitvectorzyconcat} \lstinputlisting[language=sail]{sail_latexcc/sailccbitvectorconcat.tex}}
-
-\newcommand{\sailccappend}{\label{zappend} \lstinputlisting[language=sail]{sail_latexcc/sailccappend.tex}}
-
-\newcommand{\sailccappendsixfour}{\label{zappendzysixfour} \lstinputlisting[language=sail]{sail_latexcc/sailccappendsixfour.tex}}
-
-\newcommand{\sailccbitvectoraccess}{\label{zbitvectorzyaccess} \lstinputlisting[language=sail]{sail_latexcc/sailccbitvectoraccess.tex}}
-
-\newcommand{\sailccplainvectoraccess}{\label{zplainzyvectorzyaccess} \lstinputlisting[language=sail]{sail_latexcc/sailccplainvectoraccess.tex}}
-
-\newcommand{\sailccvectoraccess}{\label{zvectorzyaccess} \lstinputlisting[language=sail]{sail_latexcc/sailccvectoraccess.tex}}
-
-\newcommand{\sailccbitvectorupdate}{\label{zbitvectorzyupdate} \lstinputlisting[language=sail]{sail_latexcc/sailccbitvectorupdate.tex}}
-
-\newcommand{\sailccplainvectorupdate}{\label{zplainzyvectorzyupdate} \lstinputlisting[language=sail]{sail_latexcc/sailccplainvectorupdate.tex}}
-
-\newcommand{\sailccvectorupdate}{\label{zvectorzyupdate} \lstinputlisting[language=sail]{sail_latexcc/sailccvectorupdate.tex}}
-
-\newcommand{\sailccaddbits}{\label{zaddzybits} \lstinputlisting[language=sail]{sail_latexcc/sailccaddbits.tex}}
-
-\newcommand{\sailccaddbitsint}{\label{zaddzybitszyint} \lstinputlisting[language=sail]{sail_latexcc/sailccaddbitsint.tex}}
-
-\newcommand{\sailccsailcczeightoperatorzzerozBzninev}{\label{zzeightoperatorzzerozBznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozBzninev.tex}}
-
-\newcommand{\sailccvectorsubrange}{\label{zvectorzysubrange} \lstinputlisting[language=sail]{sail_latexcc/sailccvectorsubrange.tex}}
-
-\newcommand{\sailccvectorupdatesubrange}{\label{zvectorzyupdatezysubrange} \lstinputlisting[language=sail]{sail_latexcc/sailccvectorupdatesubrange.tex}}
-
-\newcommand{\sailccgetsliceint}{\label{zgetzyslicezyint} \lstinputlisting[language=sail]{sail_latexcc/sailccgetsliceint.tex}}
-
-\newcommand{\sailccsetsliceint}{\label{zsetzyslicezyint} \lstinputlisting[language=sail]{sail_latexcc/sailccsetsliceint.tex}}
-
-\newcommand{\sailccsetslicebits}{\label{zsetzyslicezybits} \lstinputlisting[language=sail]{sail_latexcc/sailccsetslicebits.tex}}
-
-\newcommand{\sailccslice}{\label{zslice} \lstinputlisting[language=sail]{sail_latexcc/sailccslice.tex}}
-
-\newcommand{\sailccreplicatebits}{\label{zreplicatezybits} \lstinputlisting[language=sail]{sail_latexcc/sailccreplicatebits.tex}}
-
-\newcommand{\sailccunsigned}{\label{zunsigned} \lstinputlisting[language=sail]{sail_latexcc/sailccunsigned.tex}}
-
-\newcommand{\sailccsigned}{\label{zsigned} \lstinputlisting[language=sail]{sail_latexcc/sailccsigned.tex}}
-
-\newcommand{\sailcceqanything}{\label{zeqzyanything} \lstinputlisting[language=sail]{sail_latexcc/sailcceqanything.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozJzJznine}{\label{zzeightoperatorzzerozJzJznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozJzJznine.tex}}
-
-\newcommand{\sailccnotvec}{\label{znotzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailccnotvec.tex}}
-
-\newcommand{\sailcczW}{\label{zzW} \lstinputlisting[language=sail]{sail_latexcc/sailcczW.tex}}
-
-\newcommand{\sailccnot}{\label{znot} \lstinputlisting[language=sail]{sail_latexcc/sailccnot.tex}}
-
-\newcommand{\sailccneqvec}{\label{zneqzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailccneqvec.tex}}
-
-\newcommand{\sailccfnneqvec}{\label{zneqzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailccfnneqvec.tex}}
-
-\newcommand{\sailccneqanything}{\label{zneqzyanything} \lstinputlisting[language=sail]{sail_latexcc/sailccneqanything.tex}}
-
-\newcommand{\sailccfnneqanything}{\label{zneqzyanything} \lstinputlisting[language=sail]{sail_latexcc/sailccfnneqanything.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozonezJznine}{\label{zzeightoperatorzzerozonezJznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozonezJznine.tex}}
-
-\newcommand{\sailccandbits}{\label{zandzybits} \lstinputlisting[language=sail]{sail_latexcc/sailccandbits.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozsixznine}{\label{zzeightoperatorzzerozsixznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozsixznine.tex}}
-
-\newcommand{\sailccorbits}{\label{zorzybits} \lstinputlisting[language=sail]{sail_latexcc/sailccorbits.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozUznine}{\label{zzeightoperatorzzerozUznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozUznine.tex}}
-
-\newcommand{\sailcccastunitvec}{\label{zcastzyunitzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailcccastunitvec.tex}}
-
-\newcommand{\sailccfncastunitvec}{\label{zcastzyunitzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailccfncastunitvec.tex}}
-
-\newcommand{\sailccprint}{\label{zprint} \lstinputlisting[language=sail]{sail_latexcc/sailccprint.tex}}
-
-\newcommand{\sailccprerrendline}{\label{zprerrzyendline} \lstinputlisting[language=sail]{sail_latexcc/sailccprerrendline.tex}}
-
-\newcommand{\sailccprerrstring}{\label{zprerrzystring} \lstinputlisting[language=sail]{sail_latexcc/sailccprerrstring.tex}}
-
-\newcommand{\sailccputchar}{\label{zputchar} \lstinputlisting[language=sail]{sail_latexcc/sailccputchar.tex}}
-
-\newcommand{\sailccconcatstr}{\label{zconcatzystr} \lstinputlisting[language=sail]{sail_latexcc/sailccconcatstr.tex}}
-
-\newcommand{\sailccstringofint}{\label{zstringzyofzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccstringofint.tex}}
-
-\newcommand{\sailccBitStr}{\label{zBitStr} \lstinputlisting[language=sail]{sail_latexcc/sailccBitStr.tex}}
-
-\newcommand{\sailccxorvec}{\label{zxorzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailccxorvec.tex}}
-
-\newcommand{\sailccintpower}{\label{zintzypower} \lstinputlisting[language=sail]{sail_latexcc/sailccintpower.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozQznine}{\label{zzeightoperatorzzerozQznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozQznine.tex}}
-
-\newcommand{\sailccaddrange}{\label{zaddzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccaddrange.tex}}
-
-\newcommand{\sailccaddvec}{\label{zaddzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailccaddvec.tex}}
-
-\newcommand{\sailccaddvecint}{\label{zaddzyveczyint} \lstinputlisting[language=sail]{sail_latexcc/sailccaddvecint.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozBznine}{\label{zzeightoperatorzzerozBznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozBznine.tex}}
-
-\newcommand{\sailccsubrange}{\label{zsubzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccsubrange.tex}}
-
-\newcommand{\sailccsubvec}{\label{zsubzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailccsubvec.tex}}
-
-\newcommand{\sailccsubvecint}{\label{zsubzyveczyint} \lstinputlisting[language=sail]{sail_latexcc/sailccsubvecint.tex}}
-
-\newcommand{\sailccnegaterange}{\label{znegatezyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccnegaterange.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozDznine}{\label{zzeightoperatorzzerozDznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozDznine.tex}}
-
-\newcommand{\sailccnegate}{\label{znegate} \lstinputlisting[language=sail]{sail_latexcc/sailccnegate.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozAznine}{\label{zzeightoperatorzzerozAznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozAznine.tex}}
-
-\newcommand{\sailccquotientnat}{\label{zquotientzynat} \lstinputlisting[language=sail]{sail_latexcc/sailccquotientnat.tex}}
-
-\newcommand{\sailccquotient}{\label{zquotient} \lstinputlisting[language=sail]{sail_latexcc/sailccquotient.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozFznine}{\label{zzeightoperatorzzerozFznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozFznine.tex}}
-
-\newcommand{\sailccquotroundzzero}{\label{zquotzyroundzyzzero} \lstinputlisting[language=sail]{sail_latexcc/sailccquotroundzzero.tex}}
-
-\newcommand{\sailccremroundzzero}{\label{zremzyroundzyzzero} \lstinputlisting[language=sail]{sail_latexcc/sailccremroundzzero.tex}}
-
-\newcommand{\sailccmodulus}{\label{zmodulus} \lstinputlisting[language=sail]{sail_latexcc/sailccmodulus.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozfiveznine}{\label{zzeightoperatorzzerozfiveznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozfiveznine.tex}}
-
-\newcommand{\sailccminnat}{\label{zminzynat} \lstinputlisting[language=sail]{sail_latexcc/sailccminnat.tex}}
-
-\newcommand{\sailccminint}{\label{zminzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccminint.tex}}
-
-\newcommand{\sailccmaxnat}{\label{zmaxzynat} \lstinputlisting[language=sail]{sail_latexcc/sailccmaxnat.tex}}
-
-\newcommand{\sailccmaxint}{\label{zmaxzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccmaxint.tex}}
-
-\newcommand{\sailccminatom}{\label{zminzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccminatom.tex}}
-
-\newcommand{\sailccmaxatom}{\label{zmaxzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccmaxatom.tex}}
-
-\newcommand{\sailccmin}{\label{zmin} \lstinputlisting[language=sail]{sail_latexcc/sailccmin.tex}}
-
-\newcommand{\sailccmax}{\label{zmax} \lstinputlisting[language=sail]{sail_latexcc/sailccmax.tex}}
-
-\newcommand{\sailccWriteRAM}{\label{zzyzyWriteRAM} \lstinputlisting[language=sail]{sail_latexcc/sailccWriteRAM.tex}}
-
-\newcommand{\sailccMIPSwrite}{\label{zzyzyMIPSzywrite} \lstinputlisting[language=sail]{sail_latexcc/sailccMIPSwrite.tex}}
-
-\newcommand{\sailccfnMIPSwrite}{\label{zzyzyMIPSzywrite} \lstinputlisting[language=sail]{sail_latexcc/sailccfnMIPSwrite.tex}}
-
-\newcommand{\sailccReadRAM}{\label{zzyzyReadRAM} \lstinputlisting[language=sail]{sail_latexcc/sailccReadRAM.tex}}
-
-\newcommand{\sailccMIPSread}{\label{zzyzyMIPSzyread} \lstinputlisting[language=sail]{sail_latexcc/sailccMIPSread.tex}}
-
-\newcommand{\sailccfnMIPSread}{\label{zzyzyMIPSzyread} \lstinputlisting[language=sail]{sail_latexcc/sailccfnMIPSread.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozQzQznine}{\label{zzeightoperatorzzerozQzQznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozQzQznine.tex}}
-
-\newcommand{\sailccfnzeightoperatorzzerozQzQznine}{\label{zzeightoperatorzzerozQzQznine} \lstinputlisting[language=sail]{sail_latexcc/sailccfnzeightoperatorzzerozQzQznine.tex}}
-
-\newcommand{\sailccpowtwo}{\label{zpowtwo} \lstinputlisting[language=sail]{sail_latexcc/sailccpowtwo.tex}}
-
-\newcommand{\sailccmipssignextend}{\label{zmipszysignzyextend} \lstinputlisting[language=sail]{sail_latexcc/sailccmipssignextend.tex}}
-
-\newcommand{\sailccmipszzeroextend}{\label{zmipszyzzerozyextend} \lstinputlisting[language=sail]{sail_latexcc/sailccmipszzeroextend.tex}}
-
-\newcommand{\sailccfnmipssignextend}{\label{zmipszysignzyextend} \lstinputlisting[language=sail]{sail_latexcc/sailccfnmipssignextend.tex}}
-
-\newcommand{\sailccfnmipszzeroextend}{\label{zmipszyzzerozyextend} \lstinputlisting[language=sail]{sail_latexcc/sailccfnmipszzeroextend.tex}}
-
-\newcommand{\sailccsignextend}{\label{zsignzyextend} \lstinputlisting[language=sail]{sail_latexcc/sailccsignextend.tex}}
-
-\newcommand{\sailcczzeroextend}{\label{zzzerozyextend} \lstinputlisting[language=sail]{sail_latexcc/sailcczzeroextend.tex}}
-
-\newcommand{\sailcczzeros}{\label{zzzeros} \lstinputlisting[language=sail]{sail_latexcc/sailcczzeros.tex}}
-
-\newcommand{\sailccfnzzeros}{\label{zzzeros} \lstinputlisting[language=sail]{sail_latexcc/sailccfnzzeros.tex}}
-
-\newcommand{\sailccones}{\label{zones} \lstinputlisting[language=sail]{sail_latexcc/sailccones.tex}}
-
-\newcommand{\sailccfnones}{\label{zones} \lstinputlisting[language=sail]{sail_latexcc/sailccfnones.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozIsznine}{\label{zzeightoperatorzzerozIzysznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozIsznine.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozKzJsznine}{\label{zzeightoperatorzzerozKzJzysznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozKzJsznine.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozIuznine}{\label{zzeightoperatorzzerozIzyuznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozIuznine.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozKzJuznine}{\label{zzeightoperatorzzerozKzJzyuznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozKzJuznine.tex}}
-
-\newcommand{\sailccfnzeightoperatorzzerozIsznine}{\label{zzeightoperatorzzerozIzysznine} \lstinputlisting[language=sail]{sail_latexcc/sailccfnzeightoperatorzzerozIsznine.tex}}
-
-\newcommand{\sailccfnzeightoperatorzzerozKzJsznine}{\label{zzeightoperatorzzerozKzJzysznine} \lstinputlisting[language=sail]{sail_latexcc/sailccfnzeightoperatorzzerozKzJsznine.tex}}
-
-\newcommand{\sailccfnzeightoperatorzzerozIuznine}{\label{zzeightoperatorzzerozIzyuznine} \lstinputlisting[language=sail]{sail_latexcc/sailccfnzeightoperatorzzerozIuznine.tex}}
-
-\newcommand{\sailccfnzeightoperatorzzerozKzJuznine}{\label{zzeightoperatorzzerozKzJzyuznine} \lstinputlisting[language=sail]{sail_latexcc/sailccfnzeightoperatorzzerozKzJuznine.tex}}
-
-\newcommand{\sailccbooltobits}{\label{zboolzytozybits} \lstinputlisting[language=sail]{sail_latexcc/sailccbooltobits.tex}}
-
-\newcommand{\sailccfnbooltobits}{\label{zboolzytozybits} \lstinputlisting[language=sail]{sail_latexcc/sailccfnbooltobits.tex}}
-
-\newcommand{\sailccbittobool}{\label{zbitzytozybool} \lstinputlisting[language=sail]{sail_latexcc/sailccbittobool.tex}}
-
-\newcommand{\sailccfnbittobool}{\label{zbitzytozybool} \lstinputlisting[language=sail]{sail_latexcc/sailccfnbittobool.tex}}
-
-\newcommand{\sailccbitstobool}{\label{zbitszytozybool} \lstinputlisting[language=sail]{sail_latexcc/sailccbitstobool.tex}}
-
-\newcommand{\sailccfnbitstobool}{\label{zbitszytozybool} \lstinputlisting[language=sail]{sail_latexcc/sailccfnbitstobool.tex}}
-
-\newcommand{\sailccshiftbitsright}{\label{zshiftzybitszyright} \lstinputlisting[language=sail]{sail_latexcc/sailccshiftbitsright.tex}}
-
-\newcommand{\sailccshiftbitsleft}{\label{zshiftzybitszyleft} \lstinputlisting[language=sail]{sail_latexcc/sailccshiftbitsleft.tex}}
-
-\newcommand{\sailccshiftl}{\label{zshiftl} \lstinputlisting[language=sail]{sail_latexcc/sailccshiftl.tex}}
-
-\newcommand{\sailccshiftr}{\label{zshiftr} \lstinputlisting[language=sail]{sail_latexcc/sailccshiftr.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozKzKznine}{\label{zzeightoperatorzzerozKzKznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozKzKznine.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozIzIznine}{\label{zzeightoperatorzzerozIzIznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozIzIznine.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozKzKsznine}{\label{zzeightoperatorzzerozKzKzysznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozKzKsznine.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozAsznine}{\label{zzeightoperatorzzerozAzysznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozAsznine.tex}}
-
-\newcommand{\sailcczeightoperatorzzerozAuznine}{\label{zzeightoperatorzzerozAzyuznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozAuznine.tex}}
-
-\newcommand{\sailcctobits}{\label{ztozybits} 
-\function{to\_bits} converts an integer to a bit vector of given length. If the integer is negative a twos-complement representation is used. If the integer is too large (or too negative) to fit in the requested length then it is truncated to the least significant bits.
-\lstinputlisting[language=sail]{sail_latexcc/sailcctobits.tex}}
-
-\newcommand{\sailccfntobits}{\label{ztozybits} \lstinputlisting[language=sail]{sail_latexcc/sailccfntobits.tex}}
-
-\newcommand{\sailccmask}{\label{zmask} \lstinputlisting[language=sail]{sail_latexcc/sailccmask.tex}}
-
-\newcommand{\sailccfnmask}{\label{zmask} \lstinputlisting[language=sail]{sail_latexcc/sailccfnmask.tex}}
-
-\newcommand{\sailccgettimens}{\label{zgetzytimezyns} \lstinputlisting[language=sail]{sail_latexcc/sailccgettimens.tex}}
-
-\newcommand{\sailccCapLen}{\label{zCapLen} \lstinputlisting[language=sail]{sail_latexcc/sailccCapLen.tex}}
-
-\newcommand{\sailccuintsixfour}{\label{zuintsixfour} \lstinputlisting[language=sail]{sail_latexcc/sailccuintsixfour.tex}}
-
-\newcommand{\sailccCPtrCmpOp}{\label{zCPtrCmpOp} \lstinputlisting[language=sail]{sail_latexcc/sailccCPtrCmpOp.tex}}
-
-\newcommand{\sailccCPtrCmpOpofnum}{\label{zCPtrCmpOpzyofzynum} \lstinputlisting[language=sail]{sail_latexcc/sailccCPtrCmpOpofnum.tex}}
-
-\newcommand{\sailccfnCPtrCmpOpofnum}{\label{zCPtrCmpOpzyofzynum} \lstinputlisting[language=sail]{sail_latexcc/sailccfnCPtrCmpOpofnum.tex}}
-
-\newcommand{\sailccnumofCPtrCmpOp}{\label{znumzyofzyCPtrCmpOp} \lstinputlisting[language=sail]{sail_latexcc/sailccnumofCPtrCmpOp.tex}}
-
-\newcommand{\sailccfnnumofCPtrCmpOp}{\label{znumzyofzyCPtrCmpOp} \lstinputlisting[language=sail]{sail_latexcc/sailccfnnumofCPtrCmpOp.tex}}
-
-\newcommand{\sailccClearRegSet}{\label{zClearRegSet} \lstinputlisting[language=sail]{sail_latexcc/sailccClearRegSet.tex}}
-
-\newcommand{\sailccClearRegSetofnum}{\label{zClearRegSetzyofzynum} \lstinputlisting[language=sail]{sail_latexcc/sailccClearRegSetofnum.tex}}
-
-\newcommand{\sailccfnClearRegSetofnum}{\label{zClearRegSetzyofzynum} \lstinputlisting[language=sail]{sail_latexcc/sailccfnClearRegSetofnum.tex}}
-
-\newcommand{\sailccnumofClearRegSet}{\label{znumzyofzyClearRegSet} \lstinputlisting[language=sail]{sail_latexcc/sailccnumofClearRegSet.tex}}
-
-\newcommand{\sailccfnnumofClearRegSet}{\label{znumzyofzyClearRegSet} \lstinputlisting[language=sail]{sail_latexcc/sailccfnnumofClearRegSet.tex}}
-
-\newcommand{\sailccCapReg}{\label{zCapReg} \lstinputlisting[language=sail]{sail_latexcc/sailccCapReg.tex}}
-
-\newcommand{\sailccCapStruct}{\label{zCapStruct} \lstinputlisting[language=sail]{sail_latexcc/sailccCapStruct.tex}}
-
-\newcommand{\sailcccapRegToCapStruct}{\label{zcapRegToCapStruct} \lstinputlisting[language=sail]{sail_latexcc/sailcccapRegToCapStruct.tex}}
-
-\newcommand{\sailccfncapRegToCapStruct}{\label{zcapRegToCapStruct} \lstinputlisting[language=sail]{sail_latexcc/sailccfncapRegToCapStruct.tex}}
-
-\newcommand{\sailccgetCapHardPerms}{\label{zgetCapHardPerms} \lstinputlisting[language=sail]{sail_latexcc/sailccgetCapHardPerms.tex}}
-
-\newcommand{\sailccfngetCapHardPerms}{\label{zgetCapHardPerms} \lstinputlisting[language=sail]{sail_latexcc/sailccfngetCapHardPerms.tex}}
-
-\newcommand{\sailcccapStructToMemBitsonetwoeight}{\label{zcapStructToMemBitsonetwoeight} \lstinputlisting[language=sail]{sail_latexcc/sailcccapStructToMemBitsonetwoeight.tex}}
-
-\newcommand{\sailccfncapStructToMemBitsonetwoeight}{\label{zcapStructToMemBitsonetwoeight} \lstinputlisting[language=sail]{sail_latexcc/sailccfncapStructToMemBitsonetwoeight.tex}}
-
-\newcommand{\sailcccapStructToCapReg}{\label{zcapStructToCapReg} \lstinputlisting[language=sail]{sail_latexcc/sailcccapStructToCapReg.tex}}
-
-\newcommand{\sailccfncapStructToCapReg}{\label{zcapStructToCapReg} \lstinputlisting[language=sail]{sail_latexcc/sailccfncapStructToCapReg.tex}}
-
-\newcommand{\sailccmemBitsToCapBitsonetwoeight}{\label{zmemBitsToCapBitsonetwoeight} \lstinputlisting[language=sail]{sail_latexcc/sailccmemBitsToCapBitsonetwoeight.tex}}
-
-\newcommand{\sailccfnmemBitsToCapBitsonetwoeight}{\label{zmemBitsToCapBitsonetwoeight} \lstinputlisting[language=sail]{sail_latexcc/sailccfnmemBitsToCapBitsonetwoeight.tex}}
-
-\newcommand{\sailcccapStructToMemBits}{\label{zcapStructToMemBits} \lstinputlisting[language=sail]{sail_latexcc/sailcccapStructToMemBits.tex}}
-
-\newcommand{\sailccfncapStructToMemBits}{\label{zcapStructToMemBits} \lstinputlisting[language=sail]{sail_latexcc/sailccfncapStructToMemBits.tex}}
-
-\newcommand{\sailccmemBitsToCapBits}{\label{zmemBitsToCapBits} \lstinputlisting[language=sail]{sail_latexcc/sailccmemBitsToCapBits.tex}}
-
-\newcommand{\sailccfnmemBitsToCapBits}{\label{zmemBitsToCapBits} \lstinputlisting[language=sail]{sail_latexcc/sailccfnmemBitsToCapBits.tex}}
-
-\newcommand{\sailccgetCapPerms}{\label{zgetCapPerms} \lstinputlisting[language=sail]{sail_latexcc/sailccgetCapPerms.tex}}
-
-\newcommand{\sailccfngetCapPerms}{\label{zgetCapPerms} \lstinputlisting[language=sail]{sail_latexcc/sailccfngetCapPerms.tex}}
-
-\newcommand{\sailccsetCapPerms}{\label{zsetCapPerms} \lstinputlisting[language=sail]{sail_latexcc/sailccsetCapPerms.tex}}
-
-\newcommand{\sailccfnsetCapPerms}{\label{zsetCapPerms} \lstinputlisting[language=sail]{sail_latexcc/sailccfnsetCapPerms.tex}}
-
-\newcommand{\sailccsealCap}{\label{zsealCap} \lstinputlisting[language=sail]{sail_latexcc/sailccsealCap.tex}}
-
-\newcommand{\sailccfnsealCap}{\label{zsealCap} \lstinputlisting[language=sail]{sail_latexcc/sailccfnsealCap.tex}}
-
-\newcommand{\sailccatopcorrection}{\label{zazytopzycorrection} \lstinputlisting[language=sail]{sail_latexcc/sailccatopcorrection.tex}}
-
-\newcommand{\sailccfnatopcorrection}{\label{zazytopzycorrection} \lstinputlisting[language=sail]{sail_latexcc/sailccfnatopcorrection.tex}}
-
-\newcommand{\sailccgetCapBase}{\label{zgetCapBase} \lstinputlisting[language=sail]{sail_latexcc/sailccgetCapBase.tex}}
-
-\newcommand{\sailccfngetCapBase}{\label{zgetCapBase} \lstinputlisting[language=sail]{sail_latexcc/sailccfngetCapBase.tex}}
-
-\newcommand{\sailccgetCapTop}{\label{zgetCapTop} \lstinputlisting[language=sail]{sail_latexcc/sailccgetCapTop.tex}}
-
-\newcommand{\sailccfngetCapTop}{\label{zgetCapTop} \lstinputlisting[language=sail]{sail_latexcc/sailccfngetCapTop.tex}}
-
-\newcommand{\sailccgetCapOffset}{\label{zgetCapOffset} \lstinputlisting[language=sail]{sail_latexcc/sailccgetCapOffset.tex}}
-
-\newcommand{\sailccfngetCapOffset}{\label{zgetCapOffset} \lstinputlisting[language=sail]{sail_latexcc/sailccfngetCapOffset.tex}}
-
-\newcommand{\sailccgetCapLength}{\label{zgetCapLength} \lstinputlisting[language=sail]{sail_latexcc/sailccgetCapLength.tex}}
-
-\newcommand{\sailccfngetCapLength}{\label{zgetCapLength} \lstinputlisting[language=sail]{sail_latexcc/sailccfngetCapLength.tex}}
-
-\newcommand{\sailccgetCapCursor}{\label{zgetCapCursor} \lstinputlisting[language=sail]{sail_latexcc/sailccgetCapCursor.tex}}
-
-\newcommand{\sailccfngetCapCursor}{\label{zgetCapCursor} \lstinputlisting[language=sail]{sail_latexcc/sailccfngetCapCursor.tex}}
-
-\newcommand{\sailccfastRepCheck}{\label{zfastRepCheck} \lstinputlisting[language=sail]{sail_latexcc/sailccfastRepCheck.tex}}
-
-\newcommand{\sailccfnfastRepCheck}{\label{zfastRepCheck} \lstinputlisting[language=sail]{sail_latexcc/sailccfnfastRepCheck.tex}}
-
-\newcommand{\sailccsetCapOffset}{\label{zsetCapOffset} \lstinputlisting[language=sail]{sail_latexcc/sailccsetCapOffset.tex}}
-
-\newcommand{\sailccfnsetCapOffset}{\label{zsetCapOffset} \lstinputlisting[language=sail]{sail_latexcc/sailccfnsetCapOffset.tex}}
-
-\newcommand{\sailccincCapOffset}{\label{zincCapOffset} \lstinputlisting[language=sail]{sail_latexcc/sailccincCapOffset.tex}}
-
-\newcommand{\sailccfnincCapOffset}{\label{zincCapOffset} \lstinputlisting[language=sail]{sail_latexcc/sailccfnincCapOffset.tex}}
-
-\newcommand{\sailccHighestSetBit}{\label{zHighestSetBit} \lstinputlisting[language=sail]{sail_latexcc/sailccHighestSetBit.tex}}
-
-\newcommand{\sailccfnHighestSetBit}{\label{zHighestSetBit} \lstinputlisting[language=sail]{sail_latexcc/sailccfnHighestSetBit.tex}}
-
-\newcommand{\sailccroundUp}{\label{zroundUp} \lstinputlisting[language=sail]{sail_latexcc/sailccroundUp.tex}}
-
-\newcommand{\sailccfnroundUp}{\label{zroundUp} \lstinputlisting[language=sail]{sail_latexcc/sailccfnroundUp.tex}}
-
-\newcommand{\sailcccomputeE}{\label{zcomputeE} \lstinputlisting[language=sail]{sail_latexcc/sailcccomputeE.tex}}
-
-\newcommand{\sailccfncomputeE}{\label{zcomputeE} \lstinputlisting[language=sail]{sail_latexcc/sailccfncomputeE.tex}}
-
-\newcommand{\sailccsetCapBounds}{\label{zsetCapBounds} \lstinputlisting[language=sail]{sail_latexcc/sailccsetCapBounds.tex}}
-
-\newcommand{\sailccfnsetCapBounds}{\label{zsetCapBounds} \lstinputlisting[language=sail]{sail_latexcc/sailccfnsetCapBounds.tex}}
-
-\newcommand{\sailccinttocap}{\label{zintzytozycap} \lstinputlisting[language=sail]{sail_latexcc/sailccinttocap.tex}}
-
-\newcommand{\sailccfninttocap}{\label{zintzytozycap} \lstinputlisting[language=sail]{sail_latexcc/sailccfninttocap.tex}}
-
diff --git a/cheri/sail_latexcc/sailccBitStr.tex b/cheri/sail_latexcc/sailccBitStr.tex
deleted file mode 100644
index a0d408ab..00000000
--- a/cheri/sail_latexcc/sailccBitStr.tex
+++ /dev/null
@@ -1 +0,0 @@
-val BitStr = "string_of_bits" : forall 'n. #\hyperref[zbits]{bits}#('n) -> string
diff --git a/cheri/sail_latexcc/sailccCPtrCmpOp.tex b/cheri/sail_latexcc/sailccCPtrCmpOp.tex
deleted file mode 100644
index cb0a73ae..00000000
--- a/cheri/sail_latexcc/sailccCPtrCmpOp.tex
+++ /dev/null
@@ -1,10 +0,0 @@
-enum CPtrCmpOp = {
-  CEQ,
-  CNE,
-  CLT,
-  CLE,
-  CLTU,
-  CLEU,
-  CEXEQ,
-  CNEXEQ
-}
diff --git a/cheri/sail_latexcc/sailccCPtrCmpOpofnum.tex b/cheri/sail_latexcc/sailccCPtrCmpOpofnum.tex
deleted file mode 100644
index bd6ca31c..00000000
--- a/cheri/sail_latexcc/sailccCPtrCmpOpofnum.tex
+++ /dev/null
@@ -1 +0,0 @@
-val CPtrCmpOp_of_num : forall ('e : Int), 0 <= 'e & 'e <= 7. atom('e) -> CPtrCmpOp
diff --git a/cheri/sail_latexcc/sailccCapLen.tex b/cheri/sail_latexcc/sailccCapLen.tex
deleted file mode 100644
index 812f45ff..00000000
--- a/cheri/sail_latexcc/sailccCapLen.tex
+++ /dev/null
@@ -1 +0,0 @@
-type CapLen = range(0, 2 ^ 65)
diff --git a/cheri/sail_latexcc/sailccCapReg.tex b/cheri/sail_latexcc/sailccCapReg.tex
deleted file mode 100644
index 702141d9..00000000
--- a/cheri/sail_latexcc/sailccCapReg.tex
+++ /dev/null
@@ -1 +0,0 @@
-type CapReg = #\hyperref[zbits]{bits}#(129)
diff --git a/cheri/sail_latexcc/sailccCapStruct.tex b/cheri/sail_latexcc/sailccCapStruct.tex
deleted file mode 100644
index b1df7ec5..00000000
--- a/cheri/sail_latexcc/sailccCapStruct.tex
+++ /dev/null
@@ -1,22 +0,0 @@
-struct CapStruct = {
-  tag                    : bool    ,
-  uperms                 : #\hyperref[zbits]{bits}#(4) ,
-  access_system_regs     : bool    ,
-  permit_unseal          : bool    ,
-  permit_ccall           : bool    ,
-  permit_seal            : bool    ,
-  permit_store_local_cap : bool    ,
-  permit_store_cap       : bool    ,
-  permit_load_cap        : bool    ,
-  permit_store           : bool    ,
-  permit_load            : bool    ,
-  permit_execute         : bool    ,
-  global                 : bool    ,
-  reserved               : #\hyperref[zbits]{bits}#(2) ,
-  E                      : #\hyperref[zbits]{bits}#(6) ,
-  sealed                 : bool    ,
-  B                      : #\hyperref[zbits]{bits}#(20),
-  T                      : #\hyperref[zbits]{bits}#(20),
-  otype                  : #\hyperref[zbits]{bits}#(24),
-  address                : #\hyperref[zbits]{bits}#(64)
-}
diff --git a/cheri/sail_latexcc/sailccClearRegSet.tex b/cheri/sail_latexcc/sailccClearRegSet.tex
deleted file mode 100644
index c04ea7d4..00000000
--- a/cheri/sail_latexcc/sailccClearRegSet.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-enum ClearRegSet = {
-GPLo,
-GPHi,
-CLo,
-CHi
-}
diff --git a/cheri/sail_latexcc/sailccClearRegSetofnum.tex b/cheri/sail_latexcc/sailccClearRegSetofnum.tex
deleted file mode 100644
index c73d36d9..00000000
--- a/cheri/sail_latexcc/sailccClearRegSetofnum.tex
+++ /dev/null
@@ -1 +0,0 @@
-val ClearRegSet_of_num : forall ('e : Int), 0 <= 'e & 'e <= 3. atom('e) -> ClearRegSet
diff --git a/cheri/sail_latexcc/sailccHighestSetBit.tex b/cheri/sail_latexcc/sailccHighestSetBit.tex
deleted file mode 100644
index eb8a5e36..00000000
--- a/cheri/sail_latexcc/sailccHighestSetBit.tex
+++ /dev/null
@@ -1 +0,0 @@
-val HighestSetBit : forall 'N , 'N >= 2. #\hyperref[zbits]{bits}#('N) -> {'n, 0 <= 'n < 'N . (bool, atom('n))}
diff --git a/cheri/sail_latexcc/sailccMIPSread.tex b/cheri/sail_latexcc/sailccMIPSread.tex
deleted file mode 100644
index 92ca59cc..00000000
--- a/cheri/sail_latexcc/sailccMIPSread.tex
+++ /dev/null
@@ -1 +0,0 @@
-val __MIPS_read : forall 'n, 'n >= 0. (#\hyperref[zbits]{bits}#(64), atom('n)) -> #\hyperref[zbits]{bits}#(8 * 'n) effect {rmem}
diff --git a/cheri/sail_latexcc/sailccMIPSwrite.tex b/cheri/sail_latexcc/sailccMIPSwrite.tex
deleted file mode 100644
index cc67fa20..00000000
--- a/cheri/sail_latexcc/sailccMIPSwrite.tex
+++ /dev/null
@@ -1 +0,0 @@
-val __MIPS_write : forall 'n. (#\hyperref[zbits]{bits}#(64), atom('n), #\hyperref[zbits]{bits}#(8 * 'n)) -> unit effect {wmv}
diff --git a/cheri/sail_latexcc/sailccReadRAM.tex b/cheri/sail_latexcc/sailccReadRAM.tex
deleted file mode 100644
index 68d629a6..00000000
--- a/cheri/sail_latexcc/sailccReadRAM.tex
+++ /dev/null
@@ -1,2 +0,0 @@
-val __ReadRAM = "read_ram" : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), #\hyperref[zbits]{bits}#('m), #\hyperref[zbits]{bits}#('m)) -> #\hyperref[zbits]{bits}#(8 * 'n) effect {rmem}
diff --git a/cheri/sail_latexcc/sailccWriteRAM.tex b/cheri/sail_latexcc/sailccWriteRAM.tex
deleted file mode 100644
index 2ed4aca2..00000000
--- a/cheri/sail_latexcc/sailccWriteRAM.tex
+++ /dev/null
@@ -1,2 +0,0 @@
-val __WriteRAM = "write_ram" : forall 'n 'm.
-  (atom('m), atom('n), #\hyperref[zbits]{bits}#('m), #\hyperref[zbits]{bits}#('m), #\hyperref[zbits]{bits}#(8 * 'n)) -> bool effect {wmv}
diff --git a/cheri/sail_latexcc/sailccabsatom.tex b/cheri/sail_latexcc/sailccabsatom.tex
deleted file mode 100644
index 5164ef32..00000000
--- a/cheri/sail_latexcc/sailccabsatom.tex
+++ /dev/null
@@ -1,7 +0,0 @@
-val abs_atom = {
-  smt : "abs",
-  ocaml: "abs_int",
-  lem: "abs_int",
-  c: "abs_int",
-  coq: "abs_with_eq"
-} : forall 'n. atom('n) -> {'o, 'o = #\hyperref[zabszyatom]{abs\_atom}#('n). atom('o)}
diff --git a/cheri/sail_latexcc/sailccabsint.tex b/cheri/sail_latexcc/sailccabsint.tex
deleted file mode 100644
index d3b67cfb..00000000
--- a/cheri/sail_latexcc/sailccabsint.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-val abs_int = {
-  smt : "abs",
-  ocaml: "abs_int",
-  lem: "abs_int",
-  coq: "Z.abs"
-} : (int, int) -> int
diff --git a/cheri/sail_latexcc/sailccaddatom.tex b/cheri/sail_latexcc/sailccaddatom.tex
deleted file mode 100644
index 8b6ac810..00000000
--- a/cheri/sail_latexcc/sailccaddatom.tex
+++ /dev/null
@@ -1,2 +0,0 @@
-val add_atom = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm.
-  (atom('n), atom('m)) -> atom('n + 'm)
diff --git a/cheri/sail_latexcc/sailccaddbits.tex b/cheri/sail_latexcc/sailccaddbits.tex
deleted file mode 100644
index 95f653d1..00000000
--- a/cheri/sail_latexcc/sailccaddbits.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-val add_bits = {
-  ocaml: "add_vec",
-  lem: "add_vec",
-  c: "add_bits",
-  coq: "add_vec"
-} : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailccaddbitsint.tex b/cheri/sail_latexcc/sailccaddbitsint.tex
deleted file mode 100644
index ee9a8aa2..00000000
--- a/cheri/sail_latexcc/sailccaddbitsint.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-val add_bits_int = {
-  ocaml: "add_vec_int",
-  lem: "add_vec_int",
-  c: "add_bits_int",
-  coq: "add_vec_int"
-} : forall 'n. (#\hyperref[zbits]{bits}#('n), int) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailccaddint.tex b/cheri/sail_latexcc/sailccaddint.tex
deleted file mode 100644
index 9fe5b078..00000000
--- a/cheri/sail_latexcc/sailccaddint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : (int, int) -> int
diff --git a/cheri/sail_latexcc/sailccaddrange.tex b/cheri/sail_latexcc/sailccaddrange.tex
deleted file mode 100644
index fbf498b1..00000000
--- a/cheri/sail_latexcc/sailccaddrange.tex
+++ /dev/null
@@ -1,2 +0,0 @@
-val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range", c: "add_int"} : forall 'n 'm 'o 'p.
-  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
diff --git a/cheri/sail_latexcc/sailccaddvec.tex b/cheri/sail_latexcc/sailccaddvec.tex
deleted file mode 100644
index bb625afe..00000000
--- a/cheri/sail_latexcc/sailccaddvec.tex
+++ /dev/null
@@ -1 +0,0 @@
-val add_vec = "add_vec" : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailccaddvecint.tex b/cheri/sail_latexcc/sailccaddvecint.tex
deleted file mode 100644
index 189ad4aa..00000000
--- a/cheri/sail_latexcc/sailccaddvecint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val add_vec_int = "add_vec_int" : forall 'n. (#\hyperref[zbits]{bits}#('n), int) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailccandbits.tex b/cheri/sail_latexcc/sailccandbits.tex
deleted file mode 100644
index 8e35bd5b..00000000
--- a/cheri/sail_latexcc/sailccandbits.tex
+++ /dev/null
@@ -1 +0,0 @@
-val and_bits = {c:"and_bits", _: "and_vec"} : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailccandbool.tex b/cheri/sail_latexcc/sailccandbool.tex
deleted file mode 100644
index 926dce9f..00000000
--- a/cheri/sail_latexcc/sailccandbool.tex
+++ /dev/null
@@ -1 +0,0 @@
-val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
diff --git a/cheri/sail_latexcc/sailccappend.tex b/cheri/sail_latexcc/sailccappend.tex
deleted file mode 100644
index 56c12116..00000000
--- a/cheri/sail_latexcc/sailccappend.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload append = {bitvector_concat}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccappendsixfour.tex b/cheri/sail_latexcc/sailccappendsixfour.tex
deleted file mode 100644
index 633593b3..00000000
--- a/cheri/sail_latexcc/sailccappendsixfour.tex
+++ /dev/null
@@ -1 +0,0 @@
-val "append_64" : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#(64)) -> #\hyperref[zbits]{bits}#('n + 64)
diff --git a/cheri/sail_latexcc/sailccatopcorrection.tex b/cheri/sail_latexcc/sailccatopcorrection.tex
deleted file mode 100644
index 13bbaf7b..00000000
--- a/cheri/sail_latexcc/sailccatopcorrection.tex
+++ /dev/null
@@ -1 +0,0 @@
-val a_top_correction : (bits(20), bits(20), bits(20)) -> bits(65)
diff --git a/cheri/sail_latexcc/sailccbits.tex b/cheri/sail_latexcc/sailccbits.tex
deleted file mode 100644
index 88255b5a..00000000
--- a/cheri/sail_latexcc/sailccbits.tex
+++ /dev/null
@@ -1 +0,0 @@
-type #\hyperref[zbits]{bits}# ('n : Int) = vector('n, dec, bit)
diff --git a/cheri/sail_latexcc/sailccbitstobool.tex b/cheri/sail_latexcc/sailccbitstobool.tex
deleted file mode 100644
index 17cb3483..00000000
--- a/cheri/sail_latexcc/sailccbitstobool.tex
+++ /dev/null
@@ -1 +0,0 @@
-val cast bits_to_bool : #\hyperref[zbits]{bits}#(1) -> bool
diff --git a/cheri/sail_latexcc/sailccbittobool.tex b/cheri/sail_latexcc/sailccbittobool.tex
deleted file mode 100644
index 13a2dfb8..00000000
--- a/cheri/sail_latexcc/sailccbittobool.tex
+++ /dev/null
@@ -1 +0,0 @@
-val cast bit_to_bool : bit -> bool
diff --git a/cheri/sail_latexcc/sailccbitvectoraccess.tex b/cheri/sail_latexcc/sailccbitvectoraccess.tex
deleted file mode 100644
index 4bb98eb8..00000000
--- a/cheri/sail_latexcc/sailccbitvectoraccess.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-val bitvector_access = {
-  ocaml: "access",
-  lem: "access_vec_dec",
-  coq: "access_vec_dec",
-  c: "vector_access"
-} : forall ('n : Int), 'n >= 0. (#\hyperref[zbits]{bits}#('n), int) -> bit
diff --git a/cheri/sail_latexcc/sailccbitvectorconcat.tex b/cheri/sail_latexcc/sailccbitvectorconcat.tex
deleted file mode 100644
index afc03901..00000000
--- a/cheri/sail_latexcc/sailccbitvectorconcat.tex
+++ /dev/null
@@ -1,2 +0,0 @@
-val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
-  (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('m)) -> #\hyperref[zbits]{bits}#('n + 'm)
diff --git a/cheri/sail_latexcc/sailccbitvectorlength.tex b/cheri/sail_latexcc/sailccbitvectorlength.tex
deleted file mode 100644
index ac601acd..00000000
--- a/cheri/sail_latexcc/sailccbitvectorlength.tex
+++ /dev/null
@@ -1 +0,0 @@
-val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. #\hyperref[zbits]{bits}#('n) -> atom('n)
diff --git a/cheri/sail_latexcc/sailccbitvectorupdate.tex b/cheri/sail_latexcc/sailccbitvectorupdate.tex
deleted file mode 100644
index 6524146e..00000000
--- a/cheri/sail_latexcc/sailccbitvectorupdate.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-val bitvector_update = {
-  ocaml: "update",
-  lem: "update_vec_dec",
-  coq: "update_vec_dec",
-  c: "vector_update"
-} : forall 'n, 'n >= 0. (#\hyperref[zbits]{bits}#('n), int, bit) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailccbooltobits.tex b/cheri/sail_latexcc/sailccbooltobits.tex
deleted file mode 100644
index 711ab763..00000000
--- a/cheri/sail_latexcc/sailccbooltobits.tex
+++ /dev/null
@@ -1 +0,0 @@
-val cast bool_to_bits : bool -> #\hyperref[zbits]{bits}#(1)
diff --git a/cheri/sail_latexcc/sailcccapRegToCapStruct.tex b/cheri/sail_latexcc/sailcccapRegToCapStruct.tex
deleted file mode 100644
index bd64d554..00000000
--- a/cheri/sail_latexcc/sailcccapRegToCapStruct.tex
+++ /dev/null
@@ -1 +0,0 @@
-val capRegToCapStruct : CapReg -> CapStruct
diff --git a/cheri/sail_latexcc/sailcccapStructToCapReg.tex b/cheri/sail_latexcc/sailcccapStructToCapReg.tex
deleted file mode 100644
index b5409845..00000000
--- a/cheri/sail_latexcc/sailcccapStructToCapReg.tex
+++ /dev/null
@@ -1 +0,0 @@
-val capStructToCapReg : CapStruct -> CapReg
diff --git a/cheri/sail_latexcc/sailcccapStructToMemBits.tex b/cheri/sail_latexcc/sailcccapStructToMemBits.tex
deleted file mode 100644
index 4a49e9c0..00000000
--- a/cheri/sail_latexcc/sailcccapStructToMemBits.tex
+++ /dev/null
@@ -1 +0,0 @@
-val capStructToMemBits : CapStruct -> bits(128)
diff --git a/cheri/sail_latexcc/sailcccapStructToMemBitsonetwoeight.tex b/cheri/sail_latexcc/sailcccapStructToMemBitsonetwoeight.tex
deleted file mode 100644
index 8f3a8d0f..00000000
--- a/cheri/sail_latexcc/sailcccapStructToMemBitsonetwoeight.tex
+++ /dev/null
@@ -1 +0,0 @@
-val capStructToMemBits128 : CapStruct -> bits(128)
diff --git a/cheri/sail_latexcc/sailcccastunitvec.tex b/cheri/sail_latexcc/sailcccastunitvec.tex
deleted file mode 100644
index e0391ded..00000000
--- a/cheri/sail_latexcc/sailcccastunitvec.tex
+++ /dev/null
@@ -1 +0,0 @@
-val cast cast_unit_vec : bit -> #\hyperref[zbits]{bits}#(1)
diff --git a/cheri/sail_latexcc/sailcccomputeE.tex b/cheri/sail_latexcc/sailcccomputeE.tex
deleted file mode 100644
index 893cea49..00000000
--- a/cheri/sail_latexcc/sailcccomputeE.tex
+++ /dev/null
@@ -1 +0,0 @@
-val computeE : bits(65) -> range(0, 48) effect {escape}
diff --git a/cheri/sail_latexcc/sailccconcatstr.tex b/cheri/sail_latexcc/sailccconcatstr.tex
deleted file mode 100644
index 07556728..00000000
--- a/cheri/sail_latexcc/sailccconcatstr.tex
+++ /dev/null
@@ -1 +0,0 @@
-val concat_str = {lem: "stringAppend", coq: "String.append", _: "concat_str"} : (string, string) -> string
diff --git a/cheri/sail_latexcc/sailccdiv.tex b/cheri/sail_latexcc/sailccdiv.tex
deleted file mode 100644
index 58318fe9..00000000
--- a/cheri/sail_latexcc/sailccdiv.tex
+++ /dev/null
@@ -1,7 +0,0 @@
-val div = {
-  smt: "div",
-  ocaml: "quotient",
-  lem: "integerDiv",
-  c: "tdiv_int",
-  coq: "div_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = #\hyperref[zdiv]{div}#('n, 'm). atom('o)}
diff --git a/cheri/sail_latexcc/sailccdivint.tex b/cheri/sail_latexcc/sailccdivint.tex
deleted file mode 100644
index 34ae6121..00000000
--- a/cheri/sail_latexcc/sailccdivint.tex
+++ /dev/null
@@ -1,7 +0,0 @@
-val div_int = {
-  smt: "div",
-  ocaml: "quotient",
-  lem: "integerDiv",
-  c: "tdiv_int",
-  coq: "Z.quot"
-} : (int, int) -> int
diff --git a/cheri/sail_latexcc/sailcceqanything.tex b/cheri/sail_latexcc/sailcceqanything.tex
deleted file mode 100644
index 9b5d3c92..00000000
--- a/cheri/sail_latexcc/sailcceqanything.tex
+++ /dev/null
@@ -1 +0,0 @@
-val eq_anything = {ocaml: "(#\hyperref[zfun]{fun}# (x, y) -> x = y)", lem: "eq", coq: "generic_eq", _:"eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
diff --git a/cheri/sail_latexcc/sailcceqatom.tex b/cheri/sail_latexcc/sailcceqatom.tex
deleted file mode 100644
index 0325ab15..00000000
--- a/cheri/sail_latexcc/sailcceqatom.tex
+++ /dev/null
@@ -1 +0,0 @@
-val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool
diff --git a/cheri/sail_latexcc/sailcceqbit.tex b/cheri/sail_latexcc/sailcceqbit.tex
deleted file mode 100644
index 205d3436..00000000
--- a/cheri/sail_latexcc/sailcceqbit.tex
+++ /dev/null
@@ -1 +0,0 @@
-val eq_bit = { lem : "eq", _ : "eq_bit" } : (bit, bit) -> bool
diff --git a/cheri/sail_latexcc/sailcceqbits.tex b/cheri/sail_latexcc/sailcceqbits.tex
deleted file mode 100644
index e78ed19a..00000000
--- a/cheri/sail_latexcc/sailcceqbits.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-val eq_bits = {
-  ocaml: "eq_list",
-  lem: "eq_vec",
-  c: "eq_bits",
-  coq: "eq_vec"
-} : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool
diff --git a/cheri/sail_latexcc/sailcceqbittwo.tex b/cheri/sail_latexcc/sailcceqbittwo.tex
deleted file mode 100644
index 59353940..00000000
--- a/cheri/sail_latexcc/sailcceqbittwo.tex
+++ /dev/null
@@ -1 +0,0 @@
-val eq_bit2 = "eq_bit" : (bit, bit) -> bool
diff --git a/cheri/sail_latexcc/sailcceqbool.tex b/cheri/sail_latexcc/sailcceqbool.tex
deleted file mode 100644
index 4d2c346b..00000000
--- a/cheri/sail_latexcc/sailcceqbool.tex
+++ /dev/null
@@ -1 +0,0 @@
-val eq_bool = {ocaml: "eq_bool", lem: "eq", c: "eq_bool", coq: "Bool.eqb"} : (bool, bool) -> bool
diff --git a/cheri/sail_latexcc/sailcceqint.tex b/cheri/sail_latexcc/sailcceqint.tex
deleted file mode 100644
index 4c0462c1..00000000
--- a/cheri/sail_latexcc/sailcceqint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : (int, int) -> bool
diff --git a/cheri/sail_latexcc/sailcceqrange.tex b/cheri/sail_latexcc/sailcceqrange.tex
deleted file mode 100644
index 7f1cd5f2..00000000
--- a/cheri/sail_latexcc/sailcceqrange.tex
+++ /dev/null
@@ -1 +0,0 @@
-val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "eq_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
diff --git a/cheri/sail_latexcc/sailccfastRepCheck.tex b/cheri/sail_latexcc/sailccfastRepCheck.tex
deleted file mode 100644
index 2dd665fb..00000000
--- a/cheri/sail_latexcc/sailccfastRepCheck.tex
+++ /dev/null
@@ -1 +0,0 @@
-val fastRepCheck : (CapStruct, bits(64)) -> bool
diff --git a/cheri/sail_latexcc/sailccfnCPtrCmpOpofnum.tex b/cheri/sail_latexcc/sailccfnCPtrCmpOpofnum.tex
deleted file mode 100644
index 6ab563f3..00000000
--- a/cheri/sail_latexcc/sailccfnCPtrCmpOpofnum.tex
+++ /dev/null
@@ -1,10 +0,0 @@
-function CPtrCmpOp_of_num arg# = match arg# {
-  0 => CEQ,
-  1 => CNE,
-  2 => CLT,
-  3 => CLE,
-  4 => CLTU,
-  5 => CLEU,
-  6 => CEXEQ,
-  _ => CNEXEQ
-}
diff --git a/cheri/sail_latexcc/sailccfnClearRegSetofnum.tex b/cheri/sail_latexcc/sailccfnClearRegSetofnum.tex
deleted file mode 100644
index edfe64e3..00000000
--- a/cheri/sail_latexcc/sailccfnClearRegSetofnum.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-function ClearRegSet_of_num arg# = match arg# {
-  0 => GPLo,
-  1 => GPHi,
-  2 => CLo,
-  _ => CHi
-}
diff --git a/cheri/sail_latexcc/sailccfnHighestSetBit.tex b/cheri/sail_latexcc/sailccfnHighestSetBit.tex
deleted file mode 100644
index dbbc5b49..00000000
--- a/cheri/sail_latexcc/sailccfnHighestSetBit.tex
+++ /dev/null
@@ -1,5 +0,0 @@
-function HighestSetBit x = {
-  foreach (i #\hyperref[zfrom]{from}# ('N - 1) to 0 by 1 in dec)
-    if [x[i]] == 0b1 then return (true, i);
-  return (false, 0)
-}
diff --git a/cheri/sail_latexcc/sailccfnMIPSread.tex b/cheri/sail_latexcc/sailccfnMIPSread.tex
deleted file mode 100644
index ee937856..00000000
--- a/cheri/sail_latexcc/sailccfnMIPSread.tex
+++ /dev/null
@@ -1 +0,0 @@
-function #\hyperref[zzyzyMIPSzyread]{\_\_MIPS\_read}# (addr, width) = #\hyperref[zzyzyReadRAM]{\_\_ReadRAM}#(64, width, 0x0000_0000_0000_0000, addr)
diff --git a/cheri/sail_latexcc/sailccfnMIPSwrite.tex b/cheri/sail_latexcc/sailccfnMIPSwrite.tex
deleted file mode 100644
index 5e81f335..00000000
--- a/cheri/sail_latexcc/sailccfnMIPSwrite.tex
+++ /dev/null
@@ -1 +0,0 @@
-function #\hyperref[zzyzyMIPSzywrite]{\_\_MIPS\_write}# (addr, width, data) = let _ = #\hyperref[zzyzyWriteRAM]{\_\_WriteRAM}#(64, width, 0x0000_0000_0000_0000, addr, data) in ()
diff --git a/cheri/sail_latexcc/sailccfnatopcorrection.tex b/cheri/sail_latexcc/sailccfnatopcorrection.tex
deleted file mode 100644
index 3a6be173..00000000
--- a/cheri/sail_latexcc/sailccfnatopcorrection.tex
+++ /dev/null
@@ -1,7 +0,0 @@
-function #\hyperref[zazytopzycorrection]{a\_top\_correction}#(a_mid, R, bound) : (#\hyperref[zbits]{bits}#(20), #\hyperref[zbits]{bits}#(20), #\hyperref[zbits]{bits}#(20)) -> #\hyperref[zbits]{bits}#(65) =
-    match (a_mid <_u R, bound <_u R) {
-      (false, false)  => #\hyperref[zzzeros]{zeros}#(),
-      (false, true)   => #\hyperref[zzzerozyextend]{zero\_extend}#(0b1),
-      (true, false)   => #\hyperref[zones]{ones}#(),
-      (true, true)    => #\hyperref[zzzeros]{zeros}#()
-    }
diff --git a/cheri/sail_latexcc/sailccfnbitstobool.tex b/cheri/sail_latexcc/sailccfnbitstobool.tex
deleted file mode 100644
index 1cb33076..00000000
--- a/cheri/sail_latexcc/sailccfnbitstobool.tex
+++ /dev/null
@@ -1 +0,0 @@
-function bits_to_bool x = #\hyperref[zbitzytozybool]{bit\_to\_bool}#(x[0])
diff --git a/cheri/sail_latexcc/sailccfnbittobool.tex b/cheri/sail_latexcc/sailccfnbittobool.tex
deleted file mode 100644
index a5eea578..00000000
--- a/cheri/sail_latexcc/sailccfnbittobool.tex
+++ /dev/null
@@ -1,4 +0,0 @@
-function bit_to_bool b = match b {
-  bitone => true,
-  _ => false
-}
diff --git a/cheri/sail_latexcc/sailccfnbooltobits.tex b/cheri/sail_latexcc/sailccfnbooltobits.tex
deleted file mode 100644
index 99075369..00000000
--- a/cheri/sail_latexcc/sailccfnbooltobits.tex
+++ /dev/null
@@ -1 +0,0 @@
-function bool_to_bits x = if x then 0b1 else 0b0
diff --git a/cheri/sail_latexcc/sailccfncapRegToCapStruct.tex b/cheri/sail_latexcc/sailccfncapRegToCapStruct.tex
deleted file mode 100644
index 4af338b9..00000000
--- a/cheri/sail_latexcc/sailccfncapRegToCapStruct.tex
+++ /dev/null
@@ -1,27 +0,0 @@
-function #\hyperref[zcapRegToCapStruct]{capRegToCapStruct}#(c) : CapReg -> CapStruct =
-  let s : bool  = c[104] in
-  let Bc : #\hyperref[zbits]{bits}#(20) = if s then c[103..96] @ 0x000 else c[103..84] in
-  let Tc : #\hyperref[zbits]{bits}#(20) = if s then c[83..76] @ 0x000 else c[83..64] in
-  let otype : #\hyperref[zbits]{bits}#(24) = if s then c[95..84] @ c[75..64] else #\hyperref[zzzeros]{zeros}#() in
-  struct {
-    tag                    = c[128],
-    uperms                 = c[127..124],
-    access_system_regs     = c[123],
-    permit_unseal          = c[122],
-    permit_ccall           = c[121],
-    permit_seal            = c[120],
-    permit_store_local_cap = c[119],
-    permit_store_cap       = c[118],
-    permit_load_cap        = c[117],
-    permit_store           = c[116],
-    permit_load            = c[115],
-    permit_execute         = c[114],
-    global                 = c[113],
-    reserved               = c[112..111],
-    E                      = c[110..105],
-    sealed                 = s,
-    B                      = Bc,
-    T                      = Tc,
-    otype                  = otype,
-    address                = c[63..0]
-  }
diff --git a/cheri/sail_latexcc/sailccfncapStructToCapReg.tex b/cheri/sail_latexcc/sailccfncapStructToCapReg.tex
deleted file mode 100644
index f6b02365..00000000
--- a/cheri/sail_latexcc/sailccfncapStructToCapReg.tex
+++ /dev/null
@@ -1,2 +0,0 @@
-function #\hyperref[zcapStructToCapReg]{capStructToCapReg}#(cap) : CapStruct -> CapReg =
-    (cap.tag @ #\hyperref[zcapStructToMemBitsonetwoeight]{capStructToMemBits128}#(cap))
diff --git a/cheri/sail_latexcc/sailccfncapStructToMemBits.tex b/cheri/sail_latexcc/sailccfncapStructToMemBits.tex
deleted file mode 100644
index ea19467f..00000000
--- a/cheri/sail_latexcc/sailccfncapStructToMemBits.tex
+++ /dev/null
@@ -1,2 +0,0 @@
-function #\hyperref[zcapStructToMemBits]{capStructToMemBits}#(cap) : CapStruct -> #\hyperref[zbits]{bits}#(128) =
-  #\hyperref[zcapStructToMemBitsonetwoeight]{capStructToMemBits128}#(cap) ^ null_cap_bits
diff --git a/cheri/sail_latexcc/sailccfncapStructToMemBitsonetwoeight.tex b/cheri/sail_latexcc/sailccfncapStructToMemBitsonetwoeight.tex
deleted file mode 100644
index 08da637f..00000000
--- a/cheri/sail_latexcc/sailccfncapStructToMemBitsonetwoeight.tex
+++ /dev/null
@@ -1,12 +0,0 @@
-function #\hyperref[zcapStructToMemBitsonetwoeight]{capStructToMemBits128}#(cap) : CapStruct -> #\hyperref[zbits]{bits}#(128) =
-    let b : #\hyperref[zbits]{bits}#(20) = if cap.sealed then (cap.B)[19..12] @ (cap.otype)[23..12] else cap.B in
-    let t : #\hyperref[zbits]{bits}#(20) = if cap.sealed then (cap.T)[19..12] @ (cap.otype)[11..0]  else cap.T in
-    ( cap.uperms
-    @ #\hyperref[zgetCapHardPerms]{getCapHardPerms}#(cap)
-    @ cap.reserved
-    @ cap.E
-    @ cap.sealed
-    @ b
-    @ t
-    @ cap.address
-    )
diff --git a/cheri/sail_latexcc/sailccfncastunitvec.tex b/cheri/sail_latexcc/sailccfncastunitvec.tex
deleted file mode 100644
index 1bb7a9e0..00000000
--- a/cheri/sail_latexcc/sailccfncastunitvec.tex
+++ /dev/null
@@ -1,4 +0,0 @@
-function cast_unit_vec b = match b {
-  bitzero => 0b0,
-  _ => 0b1
-}
diff --git a/cheri/sail_latexcc/sailccfncomputeE.tex b/cheri/sail_latexcc/sailccfncomputeE.tex
deleted file mode 100644
index ef4cb71b..00000000
--- a/cheri/sail_latexcc/sailccfncomputeE.tex
+++ /dev/null
@@ -1,7 +0,0 @@
-function #\hyperref[zcomputeE]{computeE}# (rlength) : #\hyperref[zbits]{bits}#(65) -> range(0, 48) =
-    let (nonzero, 'msb) = #\hyperref[zHighestSetBit]{HighestSetBit}#((rlength + (rlength >> 6)) >> 19) in
-    if nonzero then 
-      /* above will always return <= 45 because 19 bits of zero are shifted in from right */
-      {assert(0 <= msb & msb <= 45); #\hyperref[zroundUp]{roundUp}# (#\hyperref[zmin]{min}#(msb,45)) }
-    else 
-      0
diff --git a/cheri/sail_latexcc/sailccfnfastRepCheck.tex b/cheri/sail_latexcc/sailccfnfastRepCheck.tex
deleted file mode 100644
index 3e4d2111..00000000
--- a/cheri/sail_latexcc/sailccfnfastRepCheck.tex
+++ /dev/null
@@ -1,23 +0,0 @@
-function #\hyperref[zfastRepCheck]{fastRepCheck}#(c, i) : (CapStruct, #\hyperref[zbits]{bits}#(64)) -> bool=
-    let 'E = #\hyperref[zunsigned]{unsigned}#(c.E) in
-    if (E >= 44) then
-        true /* in this case representable region is whole address space */
-    else
-        let E'       = #\hyperref[zmin]{min}#(E, 43) in
-        let i_top    = #\hyperref[zsigned]{signed}#(i[63..E+20]) in
-        let i_mid : #\hyperref[zbits]{bits}#(20) = i[E+19..E] in
-        let a_mid : #\hyperref[zbits]{bits}#(20) = (c.address)[E+19..E] in
-        let R : #\hyperref[zbits]{bits}#(20)     = (c.B) - 0x01000 in
-        let diff : #\hyperref[zbits]{bits}#(20)  = R - a_mid in
-        let diff1 : #\hyperref[zbits]{bits}#(20) = diff - 1 in
-        /* i_top determines 1. whether the increment is inRange
-           i.e. less than the size of the representable region
-           (2**(E+20)) and 2. whether it is positive or negative. To
-           satisfy 1. all top bits must be the same so we are
-           interested in the cases i_top is 0 or -1 */
-        if (i_top == 0) then
-          i_mid <_u diff1
-        else if (i_top == -1) then
-          (i_mid >=_u diff) & (R != a_mid)
-        else
-          false
diff --git a/cheri/sail_latexcc/sailccfngetCapBase.tex b/cheri/sail_latexcc/sailccfngetCapBase.tex
deleted file mode 100644
index 51677965..00000000
--- a/cheri/sail_latexcc/sailccfngetCapBase.tex
+++ /dev/null
@@ -1,10 +0,0 @@
-function #\hyperref[zgetCapBase]{getCapBase}#(c) : CapStruct -> uint64 =
-    let E = #\hyperref[zmin]{min}#(#\hyperref[zunsigned]{unsigned}#(c.E), 48) in
-    let Bc : #\hyperref[zbits]{bits}#(20) = c.B in
-    let a : #\hyperref[zbits]{bits}#(65) = #\hyperref[zzzerozyextend]{zero\_extend}#(c.address) in
-    let R : #\hyperref[zbits]{bits}#(20) = Bc - 0x01000 in /* wraps */
-    let a_mid : #\hyperref[zbits]{bits}#(20) = #\hyperref[zmask]{mask}#(a >> E) in
-    let correction = #\hyperref[zazytopzycorrection]{a\_top\_correction}#(a_mid, R, Bc) in
-    let a_top = a >> E+20 in
-    let base : #\hyperref[zbits]{bits}#(64) = #\hyperref[zmask]{mask}#(((a_top + correction) @ Bc) << E) in
-    #\hyperref[zunsigned]{unsigned}#(base)
diff --git a/cheri/sail_latexcc/sailccfngetCapCursor.tex b/cheri/sail_latexcc/sailccfngetCapCursor.tex
deleted file mode 100644
index 9f5d5757..00000000
--- a/cheri/sail_latexcc/sailccfngetCapCursor.tex
+++ /dev/null
@@ -1 +0,0 @@
-function #\hyperref[zgetCapCursor]{getCapCursor}#(cap) : CapStruct -> uint64 = #\hyperref[zunsigned]{unsigned}#(cap.address)
diff --git a/cheri/sail_latexcc/sailccfngetCapHardPerms.tex b/cheri/sail_latexcc/sailccfngetCapHardPerms.tex
deleted file mode 100644
index 0b86b980..00000000
--- a/cheri/sail_latexcc/sailccfngetCapHardPerms.tex
+++ /dev/null
@@ -1,12 +0,0 @@
-function #\hyperref[zgetCapHardPerms]{getCapHardPerms}#(cap) : CapStruct -> #\hyperref[zbits]{bits}#(11) =
-   (cap.access_system_regs
-  @ cap.permit_unseal
-  @ cap.permit_ccall
-  @ cap.permit_seal
-  @ cap.permit_store_local_cap
-  @ cap.permit_store_cap
-  @ cap.permit_load_cap
-  @ cap.permit_store
-  @ cap.permit_load
-  @ cap.permit_execute
-  @ cap.global)
diff --git a/cheri/sail_latexcc/sailccfngetCapLength.tex b/cheri/sail_latexcc/sailccfngetCapLength.tex
deleted file mode 100644
index e9ce6566..00000000
--- a/cheri/sail_latexcc/sailccfngetCapLength.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-function #\hyperref[zgetCapLength]{getCapLength}#(c) : CapStruct -> CapLen =
-         let 'top = #\hyperref[zgetCapTop]{getCapTop}#(c) in
-         let 'base = #\hyperref[zgetCapBase]{getCapBase}#(c) in {
-             assert (top >= base);
-             top - base
-         }
diff --git a/cheri/sail_latexcc/sailccfngetCapOffset.tex b/cheri/sail_latexcc/sailccfngetCapOffset.tex
deleted file mode 100644
index 8bf83916..00000000
--- a/cheri/sail_latexcc/sailccfngetCapOffset.tex
+++ /dev/null
@@ -1,3 +0,0 @@
-function #\hyperref[zgetCapOffset]{getCapOffset}#(c) : CapStruct -> uint64 = 
-    let base = #\hyperref[zgetCapBase]{getCapBase}#(c) in
-    (#\hyperref[zunsigned]{unsigned}#(c.address) - base) % #\hyperref[zpowtwo]{pow2}#(64)
diff --git a/cheri/sail_latexcc/sailccfngetCapPerms.tex b/cheri/sail_latexcc/sailccfngetCapPerms.tex
deleted file mode 100644
index 9701e163..00000000
--- a/cheri/sail_latexcc/sailccfngetCapPerms.tex
+++ /dev/null
@@ -1,5 +0,0 @@
-function #\hyperref[zgetCapPerms]{getCapPerms}#(cap) : CapStruct -> #\hyperref[zbits]{bits}#(31) = 
-    let perms : #\hyperref[zbits]{bits}#(15) = #\hyperref[zzzerozyextend]{zero\_extend}#(#\hyperref[zgetCapHardPerms]{getCapHardPerms}#(cap)) in
-    (0x000 /* uperms 30-19 */
-  @ cap.uperms
-  @ perms)
diff --git a/cheri/sail_latexcc/sailccfngetCapTop.tex b/cheri/sail_latexcc/sailccfngetCapTop.tex
deleted file mode 100644
index 1be5af24..00000000
--- a/cheri/sail_latexcc/sailccfngetCapTop.tex
+++ /dev/null
@@ -1,11 +0,0 @@
-function #\hyperref[zgetCapTop]{getCapTop}# (c) : CapStruct -> CapLen = 
-    let E = #\hyperref[zmin]{min}#(#\hyperref[zunsigned]{unsigned}#(c.E), 48) in
-    let Bc : #\hyperref[zbits]{bits}#(20) = c.B in
-    let T : #\hyperref[zbits]{bits}#(20) = c.T in
-    let a : #\hyperref[zbits]{bits}#(65) = #\hyperref[zzzerozyextend]{zero\_extend}#(c.address)  in
-    let R : #\hyperref[zbits]{bits}#(20) = Bc - 0x01000 in /* wraps */
-    let a_mid : #\hyperref[zbits]{bits}#(20) = #\hyperref[zmask]{mask}#(a >> E) in
-    let correction = #\hyperref[zazytopzycorrection]{a\_top\_correction}#(a_mid, R, T) in
-    let a_top = a >> E+20 in
-    let top1 : #\hyperref[zbits]{bits}#(65) = #\hyperref[zmask]{mask}#((a_top + correction) @ T) in
-    #\hyperref[zunsigned]{unsigned}#(top1 << E)
diff --git a/cheri/sail_latexcc/sailccfnincCapOffset.tex b/cheri/sail_latexcc/sailccfnincCapOffset.tex
deleted file mode 100644
index 59d3237e..00000000
--- a/cheri/sail_latexcc/sailccfnincCapOffset.tex
+++ /dev/null
@@ -1,5 +0,0 @@
-function #\hyperref[zincCapOffset]{incCapOffset}#(c, delta) : (CapStruct, #\hyperref[zbits]{bits}#(64)) -> (bool, CapStruct) =
-    let newAddress : #\hyperref[zbits]{bits}#(64) = c.address + delta in
-    let newCap     = { c with address = newAddress } in
-    let representable = #\hyperref[zfastRepCheck]{fastRepCheck}#(c, delta) in
-    (representable, newCap)
diff --git a/cheri/sail_latexcc/sailccfninttocap.tex b/cheri/sail_latexcc/sailccfninttocap.tex
deleted file mode 100644
index 31bb2bec..00000000
--- a/cheri/sail_latexcc/sailccfninttocap.tex
+++ /dev/null
@@ -1,2 +0,0 @@
-function #\hyperref[zintzytozycap]{int\_to\_cap}# (offset) : #\hyperref[zbits]{bits}#(64) -> CapStruct = 
-    {null_cap with address = offset}
diff --git a/cheri/sail_latexcc/sailccfnisnone.tex b/cheri/sail_latexcc/sailccfnisnone.tex
deleted file mode 100644
index 877cc2a0..00000000
--- a/cheri/sail_latexcc/sailccfnisnone.tex
+++ /dev/null
@@ -1,4 +0,0 @@
-function is_none opt = match opt {
-  #\hyperref[zSome]{Some}#(_) => false,
-  #\hyperref[zNone]{None}#()  => true
-}
diff --git a/cheri/sail_latexcc/sailccfnissome.tex b/cheri/sail_latexcc/sailccfnissome.tex
deleted file mode 100644
index f1f5f655..00000000
--- a/cheri/sail_latexcc/sailccfnissome.tex
+++ /dev/null
@@ -1,4 +0,0 @@
-function is_some opt = match opt {
-  #\hyperref[zSome]{Some}#(_) => true,
-  #\hyperref[zNone]{None}#()  => false
-}
diff --git a/cheri/sail_latexcc/sailccfnmask.tex b/cheri/sail_latexcc/sailccfnmask.tex
deleted file mode 100644
index e62ea529..00000000
--- a/cheri/sail_latexcc/sailccfnmask.tex
+++ /dev/null
@@ -1 +0,0 @@
-function mask bs = bs['n - 1 .. 0]
diff --git a/cheri/sail_latexcc/sailccfnmemBitsToCapBits.tex b/cheri/sail_latexcc/sailccfnmemBitsToCapBits.tex
deleted file mode 100644
index 198cf984..00000000
--- a/cheri/sail_latexcc/sailccfnmemBitsToCapBits.tex
+++ /dev/null
@@ -1,2 +0,0 @@
-function #\hyperref[zmemBitsToCapBits]{memBitsToCapBits}#(tag, b) : (bool, #\hyperref[zbits]{bits}#(128)) -> #\hyperref[zbits]{bits}#(129) =
-  #\hyperref[zmemBitsToCapBitsonetwoeight]{memBitsToCapBits128}#(tag, b ^ null_cap_bits)
diff --git a/cheri/sail_latexcc/sailccfnmemBitsToCapBitsonetwoeight.tex b/cheri/sail_latexcc/sailccfnmemBitsToCapBitsonetwoeight.tex
deleted file mode 100644
index 723571e9..00000000
--- a/cheri/sail_latexcc/sailccfnmemBitsToCapBitsonetwoeight.tex
+++ /dev/null
@@ -1,2 +0,0 @@
-function #\hyperref[zmemBitsToCapBitsonetwoeight]{memBitsToCapBits128}#(tag, b) : (bool, #\hyperref[zbits]{bits}#(128)) -> CapReg=
-  (tag @ b)
diff --git a/cheri/sail_latexcc/sailccfnmipssignextend.tex b/cheri/sail_latexcc/sailccfnmipssignextend.tex
deleted file mode 100644
index 80945b61..00000000
--- a/cheri/sail_latexcc/sailccfnmipssignextend.tex
+++ /dev/null
@@ -1 +0,0 @@
-function mips_sign_extend v = #\hyperref[zsailzysignzyextend]{sail\_sign\_extend}#(v, sizeof('m))
diff --git a/cheri/sail_latexcc/sailccfnmipszzeroextend.tex b/cheri/sail_latexcc/sailccfnmipszzeroextend.tex
deleted file mode 100644
index 6c9914d9..00000000
--- a/cheri/sail_latexcc/sailccfnmipszzeroextend.tex
+++ /dev/null
@@ -1 +0,0 @@
-function mips_zero_extend v = #\hyperref[zsailzyzzerozyextend]{sail\_zero\_extend}#(v, sizeof('m))
diff --git a/cheri/sail_latexcc/sailccfnneqanything.tex b/cheri/sail_latexcc/sailccfnneqanything.tex
deleted file mode 100644
index 1605ed05..00000000
--- a/cheri/sail_latexcc/sailccfnneqanything.tex
+++ /dev/null
@@ -1 +0,0 @@
-function #\hyperref[zneqzyanything]{neq\_anything}# (x, y) = #\hyperref[znotzybool]{not\_bool}#(x == y)
diff --git a/cheri/sail_latexcc/sailccfnneqatom.tex b/cheri/sail_latexcc/sailccfnneqatom.tex
deleted file mode 100644
index e9a9f93f..00000000
--- a/cheri/sail_latexcc/sailccfnneqatom.tex
+++ /dev/null
@@ -1 +0,0 @@
-function #\hyperref[zneqzyatom]{neq\_atom}# (x, y) = #\hyperref[znotzybool]{not\_bool}#(#\hyperref[zeqzyatom]{eq\_atom}#(x, y))
diff --git a/cheri/sail_latexcc/sailccfnneqbool.tex b/cheri/sail_latexcc/sailccfnneqbool.tex
deleted file mode 100644
index 65007b8e..00000000
--- a/cheri/sail_latexcc/sailccfnneqbool.tex
+++ /dev/null
@@ -1 +0,0 @@
-function #\hyperref[zneqzybool]{neq\_bool}# (x, y) = #\hyperref[znotzybool]{not\_bool}#(#\hyperref[zeqzybool]{eq\_bool}#(x, y))
diff --git a/cheri/sail_latexcc/sailccfnneqint.tex b/cheri/sail_latexcc/sailccfnneqint.tex
deleted file mode 100644
index 952a7735..00000000
--- a/cheri/sail_latexcc/sailccfnneqint.tex
+++ /dev/null
@@ -1 +0,0 @@
-function #\hyperref[zneqzyint]{neq\_int}# (x, y) = #\hyperref[znotzybool]{not\_bool}#(#\hyperref[zeqzyint]{eq\_int}#(x, y))
diff --git a/cheri/sail_latexcc/sailccfnneqrange.tex b/cheri/sail_latexcc/sailccfnneqrange.tex
deleted file mode 100644
index 43f49e9e..00000000
--- a/cheri/sail_latexcc/sailccfnneqrange.tex
+++ /dev/null
@@ -1 +0,0 @@
-function #\hyperref[zneqzyrange]{neq\_range}# (x, y) = #\hyperref[znotzybool]{not\_bool}#(#\hyperref[zeqzyrange]{eq\_range}#(x, y))
diff --git a/cheri/sail_latexcc/sailccfnneqvec.tex b/cheri/sail_latexcc/sailccfnneqvec.tex
deleted file mode 100644
index c446df08..00000000
--- a/cheri/sail_latexcc/sailccfnneqvec.tex
+++ /dev/null
@@ -1 +0,0 @@
-function #\hyperref[zneqzyvec]{neq\_vec}# (x, y) = #\hyperref[znotzybool]{not\_bool}#(#\hyperref[zeqzybits]{eq\_bits}#(x, y))
diff --git a/cheri/sail_latexcc/sailccfnnumofCPtrCmpOp.tex b/cheri/sail_latexcc/sailccfnnumofCPtrCmpOp.tex
deleted file mode 100644
index 4d20546b..00000000
--- a/cheri/sail_latexcc/sailccfnnumofCPtrCmpOp.tex
+++ /dev/null
@@ -1,10 +0,0 @@
-function num_of_CPtrCmpOp arg# = match arg# {
-  CEQ => 0,
-  CNE => 1,
-  CLT => 2,
-  CLE => 3,
-  CLTU => 4,
-  CLEU => 5,
-  CEXEQ => 6,
-  CNEXEQ => 7
-}
diff --git a/cheri/sail_latexcc/sailccfnnumofClearRegSet.tex b/cheri/sail_latexcc/sailccfnnumofClearRegSet.tex
deleted file mode 100644
index 3dd58b89..00000000
--- a/cheri/sail_latexcc/sailccfnnumofClearRegSet.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-function num_of_ClearRegSet arg# = match arg# {
-  GPLo => 0,
-  GPHi => 1,
-  CLo => 2,
-  CHi => 3
-}
diff --git a/cheri/sail_latexcc/sailccfnones.tex b/cheri/sail_latexcc/sailccfnones.tex
deleted file mode 100644
index e58040d7..00000000
--- a/cheri/sail_latexcc/sailccfnones.tex
+++ /dev/null
@@ -1 +0,0 @@
-function #\hyperref[zones]{ones}#() = #\hyperref[zreplicatezybits]{replicate\_bits}# (0b1,'n)
diff --git a/cheri/sail_latexcc/sailccfnroundUp.tex b/cheri/sail_latexcc/sailccfnroundUp.tex
deleted file mode 100644
index 1ed68a59..00000000
--- a/cheri/sail_latexcc/sailccfnroundUp.tex
+++ /dev/null
@@ -1,5 +0,0 @@
-function #\hyperref[zroundUp]{roundUp}#(e) : range(0, 45) -> range(0, 48) =
-    let 'r = e % 4 in
-    if (r == 0)
-    then e
-    else (e - r + 4)
diff --git a/cheri/sail_latexcc/sailccfnsailmask.tex b/cheri/sail_latexcc/sailccfnsailmask.tex
deleted file mode 100644
index 37ede658..00000000
--- a/cheri/sail_latexcc/sailccfnsailmask.tex
+++ /dev/null
@@ -1 +0,0 @@
-function #\hyperref[zsailzymask]{sail\_mask}#(len, v) = if len <= #\hyperref[zlength]{length}#(v) then #\hyperref[ztruncate]{truncate}#(v, len) else #\hyperref[zsailzyzzerozyextend]{sail\_zero\_extend}#(v, len)
diff --git a/cheri/sail_latexcc/sailccfnsealCap.tex b/cheri/sail_latexcc/sailccfnsealCap.tex
deleted file mode 100644
index 55c55014..00000000
--- a/cheri/sail_latexcc/sailccfnsealCap.tex
+++ /dev/null
@@ -1,5 +0,0 @@
-function #\hyperref[zsealCap]{sealCap}#(cap, otype) : (CapStruct, #\hyperref[zbits]{bits}#(24)) -> (bool, CapStruct) =
-    if (((cap.T)[11..0] == #\hyperref[zzzeros]{zeros}#()) & ((cap.B)[11..0] == #\hyperref[zzzeros]{zeros}#())) then
-        (true, {cap with sealed=true, otype=otype})
-    else
-        (false, cap /* XXX should be undefined? */ )
diff --git a/cheri/sail_latexcc/sailccfnsetCapBounds.tex b/cheri/sail_latexcc/sailccfnsetCapBounds.tex
deleted file mode 100644
index 44808068..00000000
--- a/cheri/sail_latexcc/sailccfnsetCapBounds.tex
+++ /dev/null
@@ -1,13 +0,0 @@
-function #\hyperref[zsetCapBounds]{setCapBounds}#(cap, base, top) : (CapStruct, #\hyperref[zbits]{bits}#(64), #\hyperref[zbits]{bits}#(65)) -> (bool, CapStruct) =
-    /* {cap with base=base; length=(#\hyperref[zbits]{bits}#(64)) length; offset=0} */
-    let 'e = #\hyperref[zcomputeE]{computeE}#(top - (0b0 @ base)) in
-    let Bc : #\hyperref[zbits]{bits}#(20) = #\hyperref[zmask]{mask}#(base >> e) in
-    let T : #\hyperref[zbits]{bits}#(20) = #\hyperref[zmask]{mask}#(top >> e) in
-    let e_mask : #\hyperref[zbits]{bits}#(65) = #\hyperref[zzzerozyextend]{zero\_extend}#(#\hyperref[zreplicatezybits]{replicate\_bits}#(0b1, e)) in
-    let e_bits = top & e_mask in
-    let T2 : #\hyperref[zbits]{bits}#(20) = T + (if #\hyperref[zunsigned]{unsigned}#(e_bits) == 0 then 0x00000 else 0x00001) in
-    let newCap  = {cap with address=base, E=#\hyperref[ztozybits]{to\_bits}#(6, e), B=Bc, T=T2} in
-    let newBase = #\hyperref[zgetCapBase]{getCapBase}#(newCap) in
-    let newTop  = #\hyperref[zgetCapTop]{getCapTop}#(newCap) in
-    let exact   = (#\hyperref[zunsigned]{unsigned}#(base) == newBase) & (#\hyperref[zunsigned]{unsigned}#(top) == newTop) in
-    (exact, newCap)
diff --git a/cheri/sail_latexcc/sailccfnsetCapOffset.tex b/cheri/sail_latexcc/sailccfnsetCapOffset.tex
deleted file mode 100644
index f272f7d3..00000000
--- a/cheri/sail_latexcc/sailccfnsetCapOffset.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-function #\hyperref[zsetCapOffset]{setCapOffset}#(c, offset) : (CapStruct, #\hyperref[zbits]{bits}#(64)) -> (bool, CapStruct) =
-    let base : #\hyperref[zbits]{bits}#(64)       = #\hyperref[ztozybits]{to\_bits}#(64, #\hyperref[zgetCapBase]{getCapBase}#(c)) in
-    let newAddress : #\hyperref[zbits]{bits}#(64) = base + offset in
-    let newCap     = { c with address = newAddress } in
-    let representable = #\hyperref[zfastRepCheck]{fastRepCheck}#(c, (newAddress - c.address)) in
-    (representable, newCap)
diff --git a/cheri/sail_latexcc/sailccfnsetCapPerms.tex b/cheri/sail_latexcc/sailccfnsetCapPerms.tex
deleted file mode 100644
index 5af9e7f6..00000000
--- a/cheri/sail_latexcc/sailccfnsetCapPerms.tex
+++ /dev/null
@@ -1,16 +0,0 @@
-function #\hyperref[zsetCapPerms]{setCapPerms}#(cap, perms) : (CapStruct, #\hyperref[zbits]{bits}#(31)) -> CapStruct =
-    { cap with
-      uperms                 = perms[18..15],
-      /* 14..11 reserved -- ignore */
-      access_system_regs     = perms[10],
-      permit_unseal          = perms[9],
-      permit_ccall           = perms[8],
-      permit_seal            = perms[7],
-      permit_store_local_cap = perms[6],
-      permit_store_cap       = perms[5],
-      permit_load_cap        = perms[4],
-      permit_store           = perms[3],
-      permit_load            = perms[2],
-      permit_execute         = perms[1],
-      global                 = perms[0]
-      }
diff --git a/cheri/sail_latexcc/sailccfntobits.tex b/cheri/sail_latexcc/sailccfntobits.tex
deleted file mode 100644
index d1df5e83..00000000
--- a/cheri/sail_latexcc/sailccfntobits.tex
+++ /dev/null
@@ -1 +0,0 @@
-function #\hyperref[ztozybits]{to\_bits}# (l, n) = #\hyperref[zgetzyslicezyint]{get\_slice\_int}#(l, n, 0)
diff --git a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozIsznine.tex b/cheri/sail_latexcc/sailccfnzeightoperatorzzerozIsznine.tex
deleted file mode 100644
index 62e5a2e4..00000000
--- a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozIsznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-function operator <#\hyperref[zzys]{\_s}#  (x, y) = #\hyperref[zsigned]{signed}#(x) < #\hyperref[zsigned]{signed}#(y)
diff --git a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozIuznine.tex b/cheri/sail_latexcc/sailccfnzeightoperatorzzerozIuznine.tex
deleted file mode 100644
index 3f946820..00000000
--- a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozIuznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-function operator <#\hyperref[zzyu]{\_u}#  (x, y) = #\hyperref[zunsigned]{unsigned}#(x) < #\hyperref[zunsigned]{unsigned}#(y)
diff --git a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozKzJsznine.tex b/cheri/sail_latexcc/sailccfnzeightoperatorzzerozKzJsznine.tex
deleted file mode 100644
index 57ecf181..00000000
--- a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozKzJsznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-function operator >=#\hyperref[zzys]{\_s}# (x, y) = #\hyperref[zsigned]{signed}#(x) >= #\hyperref[zsigned]{signed}#(y)
diff --git a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozKzJuznine.tex b/cheri/sail_latexcc/sailccfnzeightoperatorzzerozKzJuznine.tex
deleted file mode 100644
index 6df36c6f..00000000
--- a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozKzJuznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-function operator >=#\hyperref[zzyu]{\_u}# (x, y) = #\hyperref[zunsigned]{unsigned}#(x) >= #\hyperref[zunsigned]{unsigned}#(y)
diff --git a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozQzQznine.tex b/cheri/sail_latexcc/sailccfnzeightoperatorzzerozQzQznine.tex
deleted file mode 100644
index 2c372e1b..00000000
--- a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozQzQznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-function operator ^^ (bs, n) = #\hyperref[zreplicatezybits]{replicate\_bits}# (bs, n)
diff --git a/cheri/sail_latexcc/sailccfnzzeros.tex b/cheri/sail_latexcc/sailccfnzzeros.tex
deleted file mode 100644
index 38d463fb..00000000
--- a/cheri/sail_latexcc/sailccfnzzeros.tex
+++ /dev/null
@@ -1 +0,0 @@
-function #\hyperref[zzzeros]{zeros}#() = #\hyperref[zreplicatezybits]{replicate\_bits}# (0b0,'n)
diff --git a/cheri/sail_latexcc/sailccgetCapBase.tex b/cheri/sail_latexcc/sailccgetCapBase.tex
deleted file mode 100644
index c7044d1d..00000000
--- a/cheri/sail_latexcc/sailccgetCapBase.tex
+++ /dev/null
@@ -1 +0,0 @@
-val getCapBase : CapStruct -> uint64
diff --git a/cheri/sail_latexcc/sailccgetCapCursor.tex b/cheri/sail_latexcc/sailccgetCapCursor.tex
deleted file mode 100644
index fd5d72d8..00000000
--- a/cheri/sail_latexcc/sailccgetCapCursor.tex
+++ /dev/null
@@ -1 +0,0 @@
-val getCapCursor : CapStruct -> uint64
diff --git a/cheri/sail_latexcc/sailccgetCapHardPerms.tex b/cheri/sail_latexcc/sailccgetCapHardPerms.tex
deleted file mode 100644
index 3b65a7c0..00000000
--- a/cheri/sail_latexcc/sailccgetCapHardPerms.tex
+++ /dev/null
@@ -1 +0,0 @@
-val getCapHardPerms : CapStruct -> bits(11)
diff --git a/cheri/sail_latexcc/sailccgetCapLength.tex b/cheri/sail_latexcc/sailccgetCapLength.tex
deleted file mode 100644
index be84bfb5..00000000
--- a/cheri/sail_latexcc/sailccgetCapLength.tex
+++ /dev/null
@@ -1 +0,0 @@
-val getCapLength : CapStruct -> CapLen effect {escape}
diff --git a/cheri/sail_latexcc/sailccgetCapOffset.tex b/cheri/sail_latexcc/sailccgetCapOffset.tex
deleted file mode 100644
index 668c3df1..00000000
--- a/cheri/sail_latexcc/sailccgetCapOffset.tex
+++ /dev/null
@@ -1 +0,0 @@
-val getCapOffset : CapStruct -> uint64
diff --git a/cheri/sail_latexcc/sailccgetCapPerms.tex b/cheri/sail_latexcc/sailccgetCapPerms.tex
deleted file mode 100644
index b2dabf89..00000000
--- a/cheri/sail_latexcc/sailccgetCapPerms.tex
+++ /dev/null
@@ -1 +0,0 @@
-val getCapPerms : CapStruct -> bits(31)
diff --git a/cheri/sail_latexcc/sailccgetCapTop.tex b/cheri/sail_latexcc/sailccgetCapTop.tex
deleted file mode 100644
index ff0e5f95..00000000
--- a/cheri/sail_latexcc/sailccgetCapTop.tex
+++ /dev/null
@@ -1 +0,0 @@
-val getCapTop : CapStruct -> CapLen
diff --git a/cheri/sail_latexcc/sailccgetsliceint.tex b/cheri/sail_latexcc/sailccgetsliceint.tex
deleted file mode 100644
index 2b30d096..00000000
--- a/cheri/sail_latexcc/sailccgetsliceint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val get_slice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> #\hyperref[zbits]{bits}#('w)
diff --git a/cheri/sail_latexcc/sailccgettimens.tex b/cheri/sail_latexcc/sailccgettimens.tex
deleted file mode 100644
index 74cfd526..00000000
--- a/cheri/sail_latexcc/sailccgettimens.tex
+++ /dev/null
@@ -1 +0,0 @@
-val "get_time_ns" : unit -> int
diff --git a/cheri/sail_latexcc/sailccgtatom.tex b/cheri/sail_latexcc/sailccgtatom.tex
deleted file mode 100644
index b2147a8f..00000000
--- a/cheri/sail_latexcc/sailccgtatom.tex
+++ /dev/null
@@ -1 +0,0 @@
-val gt_atom = {coq: "Z.gtb", _: "gt"}     : forall 'n 'm. (atom('n), atom('m)) -> bool
diff --git a/cheri/sail_latexcc/sailccgtatomrange.tex b/cheri/sail_latexcc/sailccgtatomrange.tex
deleted file mode 100644
index 3c520181..00000000
--- a/cheri/sail_latexcc/sailccgtatomrange.tex
+++ /dev/null
@@ -1 +0,0 @@
-val gt_atom_range = {coq: "gtb_range_r", _: "gt"}     : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
diff --git a/cheri/sail_latexcc/sailccgteqatom.tex b/cheri/sail_latexcc/sailccgteqatom.tex
deleted file mode 100644
index fb3b66b2..00000000
--- a/cheri/sail_latexcc/sailccgteqatom.tex
+++ /dev/null
@@ -1 +0,0 @@
-val gteq_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
diff --git a/cheri/sail_latexcc/sailccgteqatomrange.tex b/cheri/sail_latexcc/sailccgteqatomrange.tex
deleted file mode 100644
index 7aaf633f..00000000
--- a/cheri/sail_latexcc/sailccgteqatomrange.tex
+++ /dev/null
@@ -1 +0,0 @@
-val gteq_atom_range = {coq: "geb_range_r", _: "gteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
diff --git a/cheri/sail_latexcc/sailccgteqint.tex b/cheri/sail_latexcc/sailccgteqint.tex
deleted file mode 100644
index 77271d1f..00000000
--- a/cheri/sail_latexcc/sailccgteqint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val gteq_int = {coq: "Z.geb", _:"gteq"} : (int, int) -> bool
diff --git a/cheri/sail_latexcc/sailccgteqrangeatom.tex b/cheri/sail_latexcc/sailccgteqrangeatom.tex
deleted file mode 100644
index fda25265..00000000
--- a/cheri/sail_latexcc/sailccgteqrangeatom.tex
+++ /dev/null
@@ -1 +0,0 @@
-val gteq_range_atom = {coq: "geb_range_l", _: "gteq"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
diff --git a/cheri/sail_latexcc/sailccgtint.tex b/cheri/sail_latexcc/sailccgtint.tex
deleted file mode 100644
index 2d953eec..00000000
--- a/cheri/sail_latexcc/sailccgtint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val gt_int = {coq: "Z.gtb", _:"gt"} : (int, int) -> bool
diff --git a/cheri/sail_latexcc/sailccgtrangeatom.tex b/cheri/sail_latexcc/sailccgtrangeatom.tex
deleted file mode 100644
index b8635909..00000000
--- a/cheri/sail_latexcc/sailccgtrangeatom.tex
+++ /dev/null
@@ -1 +0,0 @@
-val gt_range_atom = {coq: "gtb_range_l", _: "gt"}     : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
diff --git a/cheri/sail_latexcc/sailccincCapOffset.tex b/cheri/sail_latexcc/sailccincCapOffset.tex
deleted file mode 100644
index 21c08cb5..00000000
--- a/cheri/sail_latexcc/sailccincCapOffset.tex
+++ /dev/null
@@ -1 +0,0 @@
-val incCapOffset : (CapStruct, bits(64)) -> (bool, CapStruct)
diff --git a/cheri/sail_latexcc/sailccintpower.tex b/cheri/sail_latexcc/sailccintpower.tex
deleted file mode 100644
index 0aa13188..00000000
--- a/cheri/sail_latexcc/sailccintpower.tex
+++ /dev/null
@@ -1 +0,0 @@
-val int_power = {ocaml: "int_power", lem: "pow", coq: "Z.pow"} : (int, int) -> int
diff --git a/cheri/sail_latexcc/sailccinttocap.tex b/cheri/sail_latexcc/sailccinttocap.tex
deleted file mode 100644
index 0f4cd328..00000000
--- a/cheri/sail_latexcc/sailccinttocap.tex
+++ /dev/null
@@ -1 +0,0 @@
-val int_to_cap : bits(64) -> CapStruct
diff --git a/cheri/sail_latexcc/sailccisnone.tex b/cheri/sail_latexcc/sailccisnone.tex
deleted file mode 100644
index 76688d37..00000000
--- a/cheri/sail_latexcc/sailccisnone.tex
+++ /dev/null
@@ -1 +0,0 @@
-val is_none : forall ('a : Type). #\hyperref[zoption]{option}#('a) -> bool
diff --git a/cheri/sail_latexcc/sailccissome.tex b/cheri/sail_latexcc/sailccissome.tex
deleted file mode 100644
index 071ac6b6..00000000
--- a/cheri/sail_latexcc/sailccissome.tex
+++ /dev/null
@@ -1 +0,0 @@
-val is_some : forall ('a : Type). #\hyperref[zoption]{option}#('a) -> bool
diff --git a/cheri/sail_latexcc/sailcclength.tex b/cheri/sail_latexcc/sailcclength.tex
deleted file mode 100644
index 248c8507..00000000
--- a/cheri/sail_latexcc/sailcclength.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload length = {bitvector_length, vector_length}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccltatom.tex b/cheri/sail_latexcc/sailccltatom.tex
deleted file mode 100644
index 5cca54df..00000000
--- a/cheri/sail_latexcc/sailccltatom.tex
+++ /dev/null
@@ -1 +0,0 @@
-val lt_atom = {coq: "Z.ltb", _: "lt"}     : forall 'n 'm. (atom('n), atom('m)) -> bool
diff --git a/cheri/sail_latexcc/sailccltatomrange.tex b/cheri/sail_latexcc/sailccltatomrange.tex
deleted file mode 100644
index 19d3375d..00000000
--- a/cheri/sail_latexcc/sailccltatomrange.tex
+++ /dev/null
@@ -1 +0,0 @@
-val lt_atom_range = {coq: "ltb_range_r", _: "lt"}     : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
diff --git a/cheri/sail_latexcc/sailcclteqatom.tex b/cheri/sail_latexcc/sailcclteqatom.tex
deleted file mode 100644
index 26e27e2d..00000000
--- a/cheri/sail_latexcc/sailcclteqatom.tex
+++ /dev/null
@@ -1 +0,0 @@
-val lteq_atom = {coq: "Z.leb", _: "lteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
diff --git a/cheri/sail_latexcc/sailcclteqatomrange.tex b/cheri/sail_latexcc/sailcclteqatomrange.tex
deleted file mode 100644
index 6e951cf7..00000000
--- a/cheri/sail_latexcc/sailcclteqatomrange.tex
+++ /dev/null
@@ -1 +0,0 @@
-val lteq_atom_range = {coq: "leb_range_r", _: "lteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
diff --git a/cheri/sail_latexcc/sailcclteqint.tex b/cheri/sail_latexcc/sailcclteqint.tex
deleted file mode 100644
index 555176be..00000000
--- a/cheri/sail_latexcc/sailcclteqint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val lteq_int = {coq: "Z.leb", _:"lteq"} : (int, int) -> bool
diff --git a/cheri/sail_latexcc/sailcclteqrangeatom.tex b/cheri/sail_latexcc/sailcclteqrangeatom.tex
deleted file mode 100644
index f8fcd32d..00000000
--- a/cheri/sail_latexcc/sailcclteqrangeatom.tex
+++ /dev/null
@@ -1 +0,0 @@
-val lteq_range_atom = {coq: "leb_range_l", _: "lteq"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
diff --git a/cheri/sail_latexcc/sailccltint.tex b/cheri/sail_latexcc/sailccltint.tex
deleted file mode 100644
index 40bd4e85..00000000
--- a/cheri/sail_latexcc/sailccltint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val lt_int = {coq: "Z.ltb", _:"lt"} : (int, int) -> bool
diff --git a/cheri/sail_latexcc/sailccltrangeatom.tex b/cheri/sail_latexcc/sailccltrangeatom.tex
deleted file mode 100644
index d8495496..00000000
--- a/cheri/sail_latexcc/sailccltrangeatom.tex
+++ /dev/null
@@ -1 +0,0 @@
-val lt_range_atom = {coq: "ltb_range_l", _: "lt"}     : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
diff --git a/cheri/sail_latexcc/sailccmask.tex b/cheri/sail_latexcc/sailccmask.tex
deleted file mode 100644
index 35d052db..00000000
--- a/cheri/sail_latexcc/sailccmask.tex
+++ /dev/null
@@ -1 +0,0 @@
-val mask : forall 'm 'n , 'm >= 'n > 0 . #\hyperref[zbits]{bits}#('m) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailccmax.tex b/cheri/sail_latexcc/sailccmax.tex
deleted file mode 100644
index 1ceed42c..00000000
--- a/cheri/sail_latexcc/sailccmax.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload max = {max_atom, max_nat, max_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccmaxatom.tex b/cheri/sail_latexcc/sailccmaxatom.tex
deleted file mode 100644
index 6cbdfa7f..00000000
--- a/cheri/sail_latexcc/sailccmaxatom.tex
+++ /dev/null
@@ -1 +0,0 @@
-val max_atom = {ocaml: "max_int", lem: "max", coq: "max_atom", c:"max_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c >= 'a & 'c >= 'b . atom('c)}
diff --git a/cheri/sail_latexcc/sailccmaxint.tex b/cheri/sail_latexcc/sailccmaxint.tex
deleted file mode 100644
index c537babb..00000000
--- a/cheri/sail_latexcc/sailccmaxint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val max_int = {lem: "max", coq: "Z.max", _: "max_int"} : (int, int) -> int
diff --git a/cheri/sail_latexcc/sailccmaxnat.tex b/cheri/sail_latexcc/sailccmaxnat.tex
deleted file mode 100644
index 1b62334a..00000000
--- a/cheri/sail_latexcc/sailccmaxnat.tex
+++ /dev/null
@@ -1 +0,0 @@
-val max_nat = {lem: "max", coq: "Z.max", _: "max_int"} : (nat, nat) -> nat
diff --git a/cheri/sail_latexcc/sailccmemBitsToCapBits.tex b/cheri/sail_latexcc/sailccmemBitsToCapBits.tex
deleted file mode 100644
index a5c86272..00000000
--- a/cheri/sail_latexcc/sailccmemBitsToCapBits.tex
+++ /dev/null
@@ -1 +0,0 @@
-val memBitsToCapBits : (bool, bits(128)) -> bits(129)
diff --git a/cheri/sail_latexcc/sailccmemBitsToCapBitsonetwoeight.tex b/cheri/sail_latexcc/sailccmemBitsToCapBitsonetwoeight.tex
deleted file mode 100644
index 4eb94a3d..00000000
--- a/cheri/sail_latexcc/sailccmemBitsToCapBitsonetwoeight.tex
+++ /dev/null
@@ -1 +0,0 @@
-val memBitsToCapBits128 : (bool, bits(128)) -> CapReg
diff --git a/cheri/sail_latexcc/sailccmin.tex b/cheri/sail_latexcc/sailccmin.tex
deleted file mode 100644
index 94097198..00000000
--- a/cheri/sail_latexcc/sailccmin.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload min = {min_atom, min_nat, min_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccminatom.tex b/cheri/sail_latexcc/sailccminatom.tex
deleted file mode 100644
index acfea384..00000000
--- a/cheri/sail_latexcc/sailccminatom.tex
+++ /dev/null
@@ -1 +0,0 @@
-val min_atom = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)}
diff --git a/cheri/sail_latexcc/sailccminint.tex b/cheri/sail_latexcc/sailccminint.tex
deleted file mode 100644
index 3d633d08..00000000
--- a/cheri/sail_latexcc/sailccminint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val min_int = {lem: "min", coq: "Z.min", _: "min_int"} : (int, int) -> int
diff --git a/cheri/sail_latexcc/sailccminnat.tex b/cheri/sail_latexcc/sailccminnat.tex
deleted file mode 100644
index 85409bd8..00000000
--- a/cheri/sail_latexcc/sailccminnat.tex
+++ /dev/null
@@ -1 +0,0 @@
-val min_nat = {lem: "min", coq: "Z.min", _: "min_int"} : (nat, nat) -> nat
diff --git a/cheri/sail_latexcc/sailccmipssignextend.tex b/cheri/sail_latexcc/sailccmipssignextend.tex
deleted file mode 100644
index e613567d..00000000
--- a/cheri/sail_latexcc/sailccmipssignextend.tex
+++ /dev/null
@@ -1 +0,0 @@
-val mips_sign_extend : forall 'n 'm , 'm >= 'n . #\hyperref[zbits]{bits}#('n) -> #\hyperref[zbits]{bits}#('m)
diff --git a/cheri/sail_latexcc/sailccmipszzeroextend.tex b/cheri/sail_latexcc/sailccmipszzeroextend.tex
deleted file mode 100644
index adbb4188..00000000
--- a/cheri/sail_latexcc/sailccmipszzeroextend.tex
+++ /dev/null
@@ -1 +0,0 @@
-val mips_zero_extend : forall 'n 'm , 'm >= 'n . #\hyperref[zbits]{bits}#('n) -> #\hyperref[zbits]{bits}#('m)
diff --git a/cheri/sail_latexcc/sailccmod.tex b/cheri/sail_latexcc/sailccmod.tex
deleted file mode 100644
index ab70dd7a..00000000
--- a/cheri/sail_latexcc/sailccmod.tex
+++ /dev/null
@@ -1,7 +0,0 @@
-val mod = {
-  smt: "mod",
-  ocaml: "modulus",
-  lem: "integerMod",
-  c: "tmod_int",
-  coq: "mod_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = #\hyperref[zmod]{mod}#('n, 'm). atom('o)}
diff --git a/cheri/sail_latexcc/sailccmodint.tex b/cheri/sail_latexcc/sailccmodint.tex
deleted file mode 100644
index bd5677aa..00000000
--- a/cheri/sail_latexcc/sailccmodint.tex
+++ /dev/null
@@ -1,7 +0,0 @@
-val mod_int = {
-  smt: "mod",
-  ocaml: "modulus",
-  lem: "integerMod",
-  c: "tmod_int",
-  coq: "Z.rem"
-} : (int, int) -> int
diff --git a/cheri/sail_latexcc/sailccmodulus.tex b/cheri/sail_latexcc/sailccmodulus.tex
deleted file mode 100644
index ca23a339..00000000
--- a/cheri/sail_latexcc/sailccmodulus.tex
+++ /dev/null
@@ -1 +0,0 @@
-val modulus = {ocaml: "modulus", lem: "hardware_mod", coq: "euclid_modulo", _ : "tmod_int"} : forall 'n, 'n > 0 .  (int, atom('n)) -> range(0, 'n - 1)
diff --git a/cheri/sail_latexcc/sailccmultatom.tex b/cheri/sail_latexcc/sailccmultatom.tex
deleted file mode 100644
index bbac3e2f..00000000
--- a/cheri/sail_latexcc/sailccmultatom.tex
+++ /dev/null
@@ -1,2 +0,0 @@
-val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm.
-  (atom('n), atom('m)) -> atom('n * 'm)
diff --git a/cheri/sail_latexcc/sailccmultint.tex b/cheri/sail_latexcc/sailccmultint.tex
deleted file mode 100644
index 08698e6f..00000000
--- a/cheri/sail_latexcc/sailccmultint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val mult_int = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int
diff --git a/cheri/sail_latexcc/sailccnegate.tex b/cheri/sail_latexcc/sailccnegate.tex
deleted file mode 100644
index ce000062..00000000
--- a/cheri/sail_latexcc/sailccnegate.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload negate = {negate_range, negate_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccnegateatom.tex b/cheri/sail_latexcc/sailccnegateatom.tex
deleted file mode 100644
index d1361e63..00000000
--- a/cheri/sail_latexcc/sailccnegateatom.tex
+++ /dev/null
@@ -1 +0,0 @@
-val negate_atom = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. atom('n) -> atom(- 'n)
diff --git a/cheri/sail_latexcc/sailccnegateint.tex b/cheri/sail_latexcc/sailccnegateint.tex
deleted file mode 100644
index 52375787..00000000
--- a/cheri/sail_latexcc/sailccnegateint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val negate_int = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : int -> int
diff --git a/cheri/sail_latexcc/sailccnegaterange.tex b/cheri/sail_latexcc/sailccnegaterange.tex
deleted file mode 100644
index 7a4ad386..00000000
--- a/cheri/sail_latexcc/sailccnegaterange.tex
+++ /dev/null
@@ -1 +0,0 @@
-val negate_range = {ocaml: "minus_big_int", lem: "integerNegate", coq: "negate_range"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n)
diff --git a/cheri/sail_latexcc/sailccneqanything.tex b/cheri/sail_latexcc/sailccneqanything.tex
deleted file mode 100644
index a898649e..00000000
--- a/cheri/sail_latexcc/sailccneqanything.tex
+++ /dev/null
@@ -1 +0,0 @@
-val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool
diff --git a/cheri/sail_latexcc/sailccneqatom.tex b/cheri/sail_latexcc/sailccneqatom.tex
deleted file mode 100644
index be777013..00000000
--- a/cheri/sail_latexcc/sailccneqatom.tex
+++ /dev/null
@@ -1 +0,0 @@
-val neq_atom = {lem: "neq", coq: "neq_atom"} : forall 'n 'm. (atom('n), atom('m)) -> bool
diff --git a/cheri/sail_latexcc/sailccneqbool.tex b/cheri/sail_latexcc/sailccneqbool.tex
deleted file mode 100644
index 0d80dc17..00000000
--- a/cheri/sail_latexcc/sailccneqbool.tex
+++ /dev/null
@@ -1 +0,0 @@
-val neq_bool : (bool, bool) -> bool
diff --git a/cheri/sail_latexcc/sailccneqint.tex b/cheri/sail_latexcc/sailccneqint.tex
deleted file mode 100644
index b233ca6b..00000000
--- a/cheri/sail_latexcc/sailccneqint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val neq_int = {lem: "neq"} : (int, int) -> bool
diff --git a/cheri/sail_latexcc/sailccneqrange.tex b/cheri/sail_latexcc/sailccneqrange.tex
deleted file mode 100644
index d2d8fb0c..00000000
--- a/cheri/sail_latexcc/sailccneqrange.tex
+++ /dev/null
@@ -1 +0,0 @@
-val neq_range = {lem: "neq"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
diff --git a/cheri/sail_latexcc/sailccneqvec.tex b/cheri/sail_latexcc/sailccneqvec.tex
deleted file mode 100644
index f655b3d8..00000000
--- a/cheri/sail_latexcc/sailccneqvec.tex
+++ /dev/null
@@ -1 +0,0 @@
-val neq_vec = {lem: "neq"} : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> bool
diff --git a/cheri/sail_latexcc/sailccnot.tex b/cheri/sail_latexcc/sailccnot.tex
deleted file mode 100644
index 515b3ef9..00000000
--- a/cheri/sail_latexcc/sailccnot.tex
+++ /dev/null
@@ -1 +0,0 @@
-val not = {coq:"negb", _:"not"} : bool -> bool
diff --git a/cheri/sail_latexcc/sailccnotbool.tex b/cheri/sail_latexcc/sailccnotbool.tex
deleted file mode 100644
index 7630f6c2..00000000
--- a/cheri/sail_latexcc/sailccnotbool.tex
+++ /dev/null
@@ -1 +0,0 @@
-val not_bool = {coq: "negb", _: "not"} : bool -> bool
diff --git a/cheri/sail_latexcc/sailccnotvec.tex b/cheri/sail_latexcc/sailccnotvec.tex
deleted file mode 100644
index a560a544..00000000
--- a/cheri/sail_latexcc/sailccnotvec.tex
+++ /dev/null
@@ -1 +0,0 @@
-val not_vec = {c:"not_bits", _:"not_vec"} : forall 'n. #\hyperref[zbits]{bits}#('n) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailccnumofCPtrCmpOp.tex b/cheri/sail_latexcc/sailccnumofCPtrCmpOp.tex
deleted file mode 100644
index 40f1bfa9..00000000
--- a/cheri/sail_latexcc/sailccnumofCPtrCmpOp.tex
+++ /dev/null
@@ -1 +0,0 @@
-val num_of_CPtrCmpOp : CPtrCmpOp -> {'e, 0 <= 'e & 'e <= 7. atom('e)}
diff --git a/cheri/sail_latexcc/sailccnumofClearRegSet.tex b/cheri/sail_latexcc/sailccnumofClearRegSet.tex
deleted file mode 100644
index 14ea7bea..00000000
--- a/cheri/sail_latexcc/sailccnumofClearRegSet.tex
+++ /dev/null
@@ -1 +0,0 @@
-val num_of_ClearRegSet : ClearRegSet -> {'e, 0 <= 'e & 'e <= 3. atom('e)}
diff --git a/cheri/sail_latexcc/sailccones.tex b/cheri/sail_latexcc/sailccones.tex
deleted file mode 100644
index 94fd805f..00000000
--- a/cheri/sail_latexcc/sailccones.tex
+++ /dev/null
@@ -1 +0,0 @@
-val ones : forall 'n, 'n >= 0 . unit -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailccorbits.tex b/cheri/sail_latexcc/sailccorbits.tex
deleted file mode 100644
index 55db5ffa..00000000
--- a/cheri/sail_latexcc/sailccorbits.tex
+++ /dev/null
@@ -1 +0,0 @@
-val or_bits = {c: "or_bits", _: "or_vec"} : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailccorbool.tex b/cheri/sail_latexcc/sailccorbool.tex
deleted file mode 100644
index 4b6bfa15..00000000
--- a/cheri/sail_latexcc/sailccorbool.tex
+++ /dev/null
@@ -1 +0,0 @@
-val or_bool = {coq: "orb", _: "or_bool"} : (bool, bool) -> bool
diff --git a/cheri/sail_latexcc/sailccplainvectoraccess.tex b/cheri/sail_latexcc/sailccplainvectoraccess.tex
deleted file mode 100644
index 94824f77..00000000
--- a/cheri/sail_latexcc/sailccplainvectoraccess.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-val plain_vector_access = {
-  ocaml: "access",
-  lem: "access_list_dec",
-  coq: "vec_access_dec",
-  c: "vector_access"
-} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a
diff --git a/cheri/sail_latexcc/sailccplainvectorupdate.tex b/cheri/sail_latexcc/sailccplainvectorupdate.tex
deleted file mode 100644
index 6880d9bd..00000000
--- a/cheri/sail_latexcc/sailccplainvectorupdate.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-val plain_vector_update = {
-  ocaml: "update",
-  lem: "update_list_dec",
-  coq: "vec_update_dec",
-  c: "vector_update"
-} : forall '#\hyperref[zn]{n}# ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
diff --git a/cheri/sail_latexcc/sailccpowtwo.tex b/cheri/sail_latexcc/sailccpowtwo.tex
deleted file mode 100644
index 41da946e..00000000
--- a/cheri/sail_latexcc/sailccpowtwo.tex
+++ /dev/null
@@ -1 +0,0 @@
-val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
diff --git a/cheri/sail_latexcc/sailccprerrbits.tex b/cheri/sail_latexcc/sailccprerrbits.tex
deleted file mode 100644
index 7d926384..00000000
--- a/cheri/sail_latexcc/sailccprerrbits.tex
+++ /dev/null
@@ -1 +0,0 @@
-val "prerr_bits" : forall 'n. (string, #\hyperref[zbits]{bits}#('n)) -> unit
diff --git a/cheri/sail_latexcc/sailccprerrendline.tex b/cheri/sail_latexcc/sailccprerrendline.tex
deleted file mode 100644
index ad4a94a0..00000000
--- a/cheri/sail_latexcc/sailccprerrendline.tex
+++ /dev/null
@@ -1 +0,0 @@
-val "prerr_endline" : string -> unit
diff --git a/cheri/sail_latexcc/sailccprerrint.tex b/cheri/sail_latexcc/sailccprerrint.tex
deleted file mode 100644
index ce7a7d61..00000000
--- a/cheri/sail_latexcc/sailccprerrint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val "prerr_int" : (string, int) -> unit
diff --git a/cheri/sail_latexcc/sailccprerrstring.tex b/cheri/sail_latexcc/sailccprerrstring.tex
deleted file mode 100644
index 7b849da2..00000000
--- a/cheri/sail_latexcc/sailccprerrstring.tex
+++ /dev/null
@@ -1 +0,0 @@
-val "prerr_string" : string -> unit
diff --git a/cheri/sail_latexcc/sailccprint.tex b/cheri/sail_latexcc/sailccprint.tex
deleted file mode 100644
index 50a64219..00000000
--- a/cheri/sail_latexcc/sailccprint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val print = "print_endline" : string -> unit
diff --git a/cheri/sail_latexcc/sailccprintbits.tex b/cheri/sail_latexcc/sailccprintbits.tex
deleted file mode 100644
index 8783a59a..00000000
--- a/cheri/sail_latexcc/sailccprintbits.tex
+++ /dev/null
@@ -1 +0,0 @@
-val "print_bits" : forall 'n. (string, #\hyperref[zbits]{bits}#('n)) -> unit
diff --git a/cheri/sail_latexcc/sailccprintint.tex b/cheri/sail_latexcc/sailccprintint.tex
deleted file mode 100644
index ddf33afc..00000000
--- a/cheri/sail_latexcc/sailccprintint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val "print_int" : (string, int) -> unit
diff --git a/cheri/sail_latexcc/sailccputchar.tex b/cheri/sail_latexcc/sailccputchar.tex
deleted file mode 100644
index a123c709..00000000
--- a/cheri/sail_latexcc/sailccputchar.tex
+++ /dev/null
@@ -1 +0,0 @@
-val putchar = {c:"sail_putchar", _:"putchar"} : int -> unit
diff --git a/cheri/sail_latexcc/sailccquotient.tex b/cheri/sail_latexcc/sailccquotient.tex
deleted file mode 100644
index 7dba5359..00000000
--- a/cheri/sail_latexcc/sailccquotient.tex
+++ /dev/null
@@ -1 +0,0 @@
-val quotient = {ocaml: "quotient", lem: "integerDiv", coq: "Z.mod"} : (int, int) -> int
diff --git a/cheri/sail_latexcc/sailccquotientnat.tex b/cheri/sail_latexcc/sailccquotientnat.tex
deleted file mode 100644
index 14db4ae0..00000000
--- a/cheri/sail_latexcc/sailccquotientnat.tex
+++ /dev/null
@@ -1 +0,0 @@
-val quotient_nat = {ocaml: "quotient", lem: "integerDiv", coq: "Z.div"} : (nat, nat) -> nat
diff --git a/cheri/sail_latexcc/sailccquotroundzzero.tex b/cheri/sail_latexcc/sailccquotroundzzero.tex
deleted file mode 100644
index 9523cfcc..00000000
--- a/cheri/sail_latexcc/sailccquotroundzzero.tex
+++ /dev/null
@@ -1 +0,0 @@
-val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", coq: "Z.quot", _ : "tdiv_int"} : (int, int) -> int
diff --git a/cheri/sail_latexcc/sailccregderef.tex b/cheri/sail_latexcc/sailccregderef.tex
deleted file mode 100644
index 7f1dc7e8..00000000
--- a/cheri/sail_latexcc/sailccregderef.tex
+++ /dev/null
@@ -1 +0,0 @@
-val _reg_deref = "reg_deref" : forall ('a : Type). #\hyperref[zregister]{register}#('a) -> 'a
diff --git a/cheri/sail_latexcc/sailccremroundzzero.tex b/cheri/sail_latexcc/sailccremroundzzero.tex
deleted file mode 100644
index 9d8113ba..00000000
--- a/cheri/sail_latexcc/sailccremroundzzero.tex
+++ /dev/null
@@ -1 +0,0 @@
-val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", coq: "Z.rem", _ : "tmod_int"} : (int, int) -> int
diff --git a/cheri/sail_latexcc/sailccreplicatebits.tex b/cheri/sail_latexcc/sailccreplicatebits.tex
deleted file mode 100644
index cd7a97d7..00000000
--- a/cheri/sail_latexcc/sailccreplicatebits.tex
+++ /dev/null
@@ -1 +0,0 @@
-val replicate_bits = "replicate_bits" : forall 'n 'm. (#\hyperref[zbits]{bits}#('n), atom('m)) -> #\hyperref[zbits]{bits}#('n * 'm)
diff --git a/cheri/sail_latexcc/sailccroundUp.tex b/cheri/sail_latexcc/sailccroundUp.tex
deleted file mode 100644
index b7e31074..00000000
--- a/cheri/sail_latexcc/sailccroundUp.tex
+++ /dev/null
@@ -1 +0,0 @@
-val roundUp : range(0, 45) -> range(0, 48)
diff --git a/cheri/sail_latexcc/sailccsailccnegatev.tex b/cheri/sail_latexcc/sailccsailccnegatev.tex
deleted file mode 100644
index 4f7aea58..00000000
--- a/cheri/sail_latexcc/sailccsailccnegatev.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload negate = {negate_atom, negate_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailccregderefv.tex b/cheri/sail_latexcc/sailccsailccregderefv.tex
deleted file mode 100644
index f5de92ca..00000000
--- a/cheri/sail_latexcc/sailccsailccregderefv.tex
+++ /dev/null
@@ -1 +0,0 @@
-val "reg_deref" : forall ('a : Type). #\hyperref[zregister]{register}#('a) -> 'a effect {rreg}
diff --git a/cheri/sail_latexcc/sailccsailccsailccsailcczeightoperatorzzerozJzJzninevvv.tex b/cheri/sail_latexcc/sailccsailccsailccsailcczeightoperatorzzerozJzJzninevvv.tex
deleted file mode 100644
index 0f72fdc9..00000000
--- a/cheri/sail_latexcc/sailccsailccsailccsailcczeightoperatorzzerozJzJzninevvv.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator ==) = {eq_bit2}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozBzninevv.tex b/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozBzninevv.tex
deleted file mode 100644
index eacd556c..00000000
--- a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozBzninevv.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator +) = {add_atom, add_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozFzninevv.tex b/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozFzninevv.tex
deleted file mode 100644
index 73c40722..00000000
--- a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozFzninevv.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator /) = {div}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozJzJzninevv.tex b/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozJzJzninevv.tex
deleted file mode 100644
index 47b1d0f6..00000000
--- a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozJzJzninevv.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator ==) = {eq_atom, eq_range, eq_int, eq_bool}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozfivezninevv.tex b/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozfivezninevv.tex
deleted file mode 100644
index 552e0c24..00000000
--- a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozfivezninevv.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator %) = {mod}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozAzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozAzninev.tex
deleted file mode 100644
index afe7a721..00000000
--- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozAzninev.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator *) = {mult_atom, mult_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozBzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozBzninev.tex
deleted file mode 100644
index ddc56bfd..00000000
--- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozBzninev.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator +) = {add_bits, add_bits_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozDzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozDzninev.tex
deleted file mode 100644
index 5d12fdf1..00000000
--- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozDzninev.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator -) = {sub_atom, sub_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozFzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozFzninev.tex
deleted file mode 100644
index 38e9124b..00000000
--- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozFzninev.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator /) = {div_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozJzJzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozJzJzninev.tex
deleted file mode 100644
index 1314a962..00000000
--- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozJzJzninev.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator ==) = {eq_bit, eq_bits}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozQzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozQzninev.tex
deleted file mode 100644
index 05769645..00000000
--- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozQzninev.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator ^) = {sail_mask}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozUzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozUzninev.tex
deleted file mode 100644
index 1ebacbc4..00000000
--- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozUzninev.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator |) = {or_bool}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozfivezninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozfivezninev.tex
deleted file mode 100644
index 14fa73b8..00000000
--- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozfivezninev.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator %) = {mod_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozonezJzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozonezJzninev.tex
deleted file mode 100644
index 527cf596..00000000
--- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozonezJzninev.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator !=) = {neq_atom, neq_range, neq_int, neq_bool}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozsixzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozsixzninev.tex
deleted file mode 100644
index be6f29ef..00000000
--- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozsixzninev.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator &) = {and_bool}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccsailmask.tex b/cheri/sail_latexcc/sailccsailmask.tex
deleted file mode 100644
index 45862747..00000000
--- a/cheri/sail_latexcc/sailccsailmask.tex
+++ /dev/null
@@ -1 +0,0 @@
-val sail_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (atom('len), vector('v, dec, bit)) -> vector('len, dec, bit)
diff --git a/cheri/sail_latexcc/sailccsailsignextend.tex b/cheri/sail_latexcc/sailccsailsignextend.tex
deleted file mode 100644
index dfaa5c86..00000000
--- a/cheri/sail_latexcc/sailccsailsignextend.tex
+++ /dev/null
@@ -1 +0,0 @@
-val sail_sign_extend = "sign_extend" : forall 'n 'm, 'm >= 'n. (#\hyperref[zbits]{bits}#('n), atom('m)) -> #\hyperref[zbits]{bits}#('m)
diff --git a/cheri/sail_latexcc/sailccsailzzeroextend.tex b/cheri/sail_latexcc/sailccsailzzeroextend.tex
deleted file mode 100644
index 53f6fff9..00000000
--- a/cheri/sail_latexcc/sailccsailzzeroextend.tex
+++ /dev/null
@@ -1 +0,0 @@
-val sail_zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (#\hyperref[zbits]{bits}#('n), atom('m)) -> #\hyperref[zbits]{bits}#('m)
diff --git a/cheri/sail_latexcc/sailccsailzzeros.tex b/cheri/sail_latexcc/sailccsailzzeros.tex
deleted file mode 100644
index 9c60aa12..00000000
--- a/cheri/sail_latexcc/sailccsailzzeros.tex
+++ /dev/null
@@ -1 +0,0 @@
-val sail_zeros = "zeros" : forall 'n. atom('n) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailccsealCap.tex b/cheri/sail_latexcc/sailccsealCap.tex
deleted file mode 100644
index 891ae279..00000000
--- a/cheri/sail_latexcc/sailccsealCap.tex
+++ /dev/null
@@ -1 +0,0 @@
-val sealCap : (CapStruct, bits(24)) -> (bool, CapStruct)
diff --git a/cheri/sail_latexcc/sailccsetCapBounds.tex b/cheri/sail_latexcc/sailccsetCapBounds.tex
deleted file mode 100644
index 94fbecaf..00000000
--- a/cheri/sail_latexcc/sailccsetCapBounds.tex
+++ /dev/null
@@ -1 +0,0 @@
-val setCapBounds : (CapStruct, bits(64), bits(65)) -> (bool, CapStruct) effect {escape}
diff --git a/cheri/sail_latexcc/sailccsetCapOffset.tex b/cheri/sail_latexcc/sailccsetCapOffset.tex
deleted file mode 100644
index fef324f7..00000000
--- a/cheri/sail_latexcc/sailccsetCapOffset.tex
+++ /dev/null
@@ -1 +0,0 @@
-val setCapOffset : (CapStruct, bits(64)) -> (bool, CapStruct)
diff --git a/cheri/sail_latexcc/sailccsetCapPerms.tex b/cheri/sail_latexcc/sailccsetCapPerms.tex
deleted file mode 100644
index 617f19fb..00000000
--- a/cheri/sail_latexcc/sailccsetCapPerms.tex
+++ /dev/null
@@ -1 +0,0 @@
-val setCapPerms : (CapStruct, bits(31)) -> CapStruct
diff --git a/cheri/sail_latexcc/sailccsetslicebits.tex b/cheri/sail_latexcc/sailccsetslicebits.tex
deleted file mode 100644
index 8a81bff5..00000000
--- a/cheri/sail_latexcc/sailccsetslicebits.tex
+++ /dev/null
@@ -1,2 +0,0 @@
-val set_slice_bits = "set_slice" : forall 'n 'm.
-  (atom('n), atom('m), #\hyperref[zbits]{bits}#('n), int, #\hyperref[zbits]{bits}#('m)) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailccsetsliceint.tex b/cheri/sail_latexcc/sailccsetsliceint.tex
deleted file mode 100644
index 413bf721..00000000
--- a/cheri/sail_latexcc/sailccsetsliceint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val set_slice_int = "set_slice_int" : forall 'w. (atom('w), int, int, #\hyperref[zbits]{bits}#('w)) -> int
diff --git a/cheri/sail_latexcc/sailccshiftbitsleft.tex b/cheri/sail_latexcc/sailccshiftbitsleft.tex
deleted file mode 100644
index cdb2eb6a..00000000
--- a/cheri/sail_latexcc/sailccshiftbitsleft.tex
+++ /dev/null
@@ -1 +0,0 @@
-val "shift_bits_left" : forall 'n 'm. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('m)) -> #\hyperref[zbits]{bits}#('n) effect {undef}
diff --git a/cheri/sail_latexcc/sailccshiftbitsright.tex b/cheri/sail_latexcc/sailccshiftbitsright.tex
deleted file mode 100644
index dbc72b11..00000000
--- a/cheri/sail_latexcc/sailccshiftbitsright.tex
+++ /dev/null
@@ -1 +0,0 @@
-val "shift_bits_right" : forall 'n 'm. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('m)) -> #\hyperref[zbits]{bits}#('n) effect {undef}
diff --git a/cheri/sail_latexcc/sailccshiftl.tex b/cheri/sail_latexcc/sailccshiftl.tex
deleted file mode 100644
index b2c54c27..00000000
--- a/cheri/sail_latexcc/sailccshiftl.tex
+++ /dev/null
@@ -1 +0,0 @@
-val "shiftl" : forall 'm 'n, 'n >= 0. (#\hyperref[zbits]{bits}#('m), atom('n)) -> #\hyperref[zbits]{bits}#('m)
diff --git a/cheri/sail_latexcc/sailccshiftr.tex b/cheri/sail_latexcc/sailccshiftr.tex
deleted file mode 100644
index f282dcbe..00000000
--- a/cheri/sail_latexcc/sailccshiftr.tex
+++ /dev/null
@@ -1 +0,0 @@
-val "shiftr" : forall 'm 'n, 'n >= 0. (#\hyperref[zbits]{bits}#('m), atom('n)) -> #\hyperref[zbits]{bits}#('m)
diff --git a/cheri/sail_latexcc/sailccshlint.tex b/cheri/sail_latexcc/sailccshlint.tex
deleted file mode 100644
index 8ffbcf6c..00000000
--- a/cheri/sail_latexcc/sailccshlint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val shl_int = "shl_int" : (int, int) -> int
diff --git a/cheri/sail_latexcc/sailccshrint.tex b/cheri/sail_latexcc/sailccshrint.tex
deleted file mode 100644
index 087c17bb..00000000
--- a/cheri/sail_latexcc/sailccshrint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val shr_int = "shr_int" : (int, int) -> int
diff --git a/cheri/sail_latexcc/sailccsigned.tex b/cheri/sail_latexcc/sailccsigned.tex
deleted file mode 100644
index dcdc3049..00000000
--- a/cheri/sail_latexcc/sailccsigned.tex
+++ /dev/null
@@ -1,4 +0,0 @@
-val signed = {
-  c: "sail_signed",
-  _: "sint"
-} : forall 'n, 'n > 0. #\hyperref[zbits]{bits}#('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
diff --git a/cheri/sail_latexcc/sailccsignextend.tex b/cheri/sail_latexcc/sailccsignextend.tex
deleted file mode 100644
index 03f56369..00000000
--- a/cheri/sail_latexcc/sailccsignextend.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload sign_extend = {mips_sign_extend}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccslice.tex b/cheri/sail_latexcc/sailccslice.tex
deleted file mode 100644
index b9bb5a70..00000000
--- a/cheri/sail_latexcc/sailccslice.tex
+++ /dev/null
@@ -1,2 +0,0 @@
-val slice = "slice" : forall 'n 'm 'o, 0 <= 'o < 'm & 'o + 'n <= 'm & 0 <= 'n.
-  (#\hyperref[zbits]{bits}#('m), atom('o), atom('n)) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailccstringofint.tex b/cheri/sail_latexcc/sailccstringofint.tex
deleted file mode 100644
index 05edaa20..00000000
--- a/cheri/sail_latexcc/sailccstringofint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val string_of_int = "string_of_int" : int -> string
diff --git a/cheri/sail_latexcc/sailccsubatom.tex b/cheri/sail_latexcc/sailccsubatom.tex
deleted file mode 100644
index 437e2d4c..00000000
--- a/cheri/sail_latexcc/sailccsubatom.tex
+++ /dev/null
@@ -1,2 +0,0 @@
-val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm.
-  (atom('n), atom('m)) -> atom('n - 'm)
diff --git a/cheri/sail_latexcc/sailccsubint.tex b/cheri/sail_latexcc/sailccsubint.tex
deleted file mode 100644
index 11fdf922..00000000
--- a/cheri/sail_latexcc/sailccsubint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : (int, int) -> int
diff --git a/cheri/sail_latexcc/sailccsubrange.tex b/cheri/sail_latexcc/sailccsubrange.tex
deleted file mode 100644
index 2aad56b6..00000000
--- a/cheri/sail_latexcc/sailccsubrange.tex
+++ /dev/null
@@ -1,2 +0,0 @@
-val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p.
-  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
diff --git a/cheri/sail_latexcc/sailccsubvec.tex b/cheri/sail_latexcc/sailccsubvec.tex
deleted file mode 100644
index b92f07a4..00000000
--- a/cheri/sail_latexcc/sailccsubvec.tex
+++ /dev/null
@@ -1 +0,0 @@
-val sub_vec = {c : "sub_bits", _:"sub_vec"} : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailccsubvecint.tex b/cheri/sail_latexcc/sailccsubvecint.tex
deleted file mode 100644
index 70bf667e..00000000
--- a/cheri/sail_latexcc/sailccsubvecint.tex
+++ /dev/null
@@ -1 +0,0 @@
-val sub_vec_int = {c:"sub_bits_int", _: "sub_vec_int"} : forall 'n. (#\hyperref[zbits]{bits}#('n), int) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailcctobits.tex b/cheri/sail_latexcc/sailcctobits.tex
deleted file mode 100644
index 9dd3c655..00000000
--- a/cheri/sail_latexcc/sailcctobits.tex
+++ /dev/null
@@ -1 +0,0 @@
-val to_bits : forall 'l, 'l >= 0 .(atom('l), int) -> #\hyperref[zbits]{bits}#('l)
diff --git a/cheri/sail_latexcc/sailcctruncate.tex b/cheri/sail_latexcc/sailcctruncate.tex
deleted file mode 100644
index 5f7760f3..00000000
--- a/cheri/sail_latexcc/sailcctruncate.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-val truncate = {
-  ocaml: "vector_truncate",
-  lem: "vector_truncate",
-  coq: "vector_truncate",
-  c: "sail_truncate"
-} : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
diff --git a/cheri/sail_latexcc/sailccuintsixfour.tex b/cheri/sail_latexcc/sailccuintsixfour.tex
deleted file mode 100644
index a0d52c8f..00000000
--- a/cheri/sail_latexcc/sailccuintsixfour.tex
+++ /dev/null
@@ -1 +0,0 @@
-type uint64 = range(0, (2 ^ 64) - 1)
diff --git a/cheri/sail_latexcc/sailccunsigned.tex b/cheri/sail_latexcc/sailccunsigned.tex
deleted file mode 100644
index 47867039..00000000
--- a/cheri/sail_latexcc/sailccunsigned.tex
+++ /dev/null
@@ -1,7 +0,0 @@
-val unsigned = {
-  ocaml: "uint",
-  lem: "uint",
-  interpreter: "uint",
-  c: "sail_unsigned",
-  coq: "uint"
-} : forall 'n. #\hyperref[zbits]{bits}#('n) -> range(0, 2 ^ 'n - 1)
diff --git a/cheri/sail_latexcc/sailccvectoraccess.tex b/cheri/sail_latexcc/sailccvectoraccess.tex
deleted file mode 100644
index a8e8074f..00000000
--- a/cheri/sail_latexcc/sailccvectoraccess.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload vector_access = {bitvector_access, plain_vector_access}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccvectorlength.tex b/cheri/sail_latexcc/sailccvectorlength.tex
deleted file mode 100644
index f41d5bfa..00000000
--- a/cheri/sail_latexcc/sailccvectorlength.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-val vector_length = {
-  ocaml: "length",
-  lem: "length_list",
-  c: "length",
-  coq: "vec_length"
-} : forall '#\hyperref[zn]{n}# ('a : Type). vector('n, dec, 'a) -> atom('n)
diff --git a/cheri/sail_latexcc/sailccvectorsubrange.tex b/cheri/sail_latexcc/sailccvectorsubrange.tex
deleted file mode 100644
index c069c7b6..00000000
--- a/cheri/sail_latexcc/sailccvectorsubrange.tex
+++ /dev/null
@@ -1,7 +0,0 @@
-val vector_subrange = {
-  ocaml: "subrange",
-  lem: "subrange_vec_dec",
-  c: "vector_subrange",
-  coq: "subrange_vec_dec"
-} : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n.
-  (#\hyperref[zbits]{bits}#('n), atom('m), atom('o)) -> #\hyperref[zbits]{bits}#('m - 'o + 1)
diff --git a/cheri/sail_latexcc/sailccvectorupdate.tex b/cheri/sail_latexcc/sailccvectorupdate.tex
deleted file mode 100644
index 1ec4aaef..00000000
--- a/cheri/sail_latexcc/sailccvectorupdate.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload vector_update = {bitvector_update, plain_vector_update}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailccvectorupdatesubrange.tex b/cheri/sail_latexcc/sailccvectorupdatesubrange.tex
deleted file mode 100644
index 6ff4f9f6..00000000
--- a/cheri/sail_latexcc/sailccvectorupdatesubrange.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-val vector_update_subrange = {
-  ocaml: "update_subrange",
-  lem: "update_subrange_vec_dec",
-  c: "vector_update_subrange",
-  coq: "update_subrange_vec_dec"
-} : forall 'n 'm 'o. (#\hyperref[zbits]{bits}#('n), atom('m), atom('o), #\hyperref[zbits]{bits}#('m - ('o - 1))) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailccxorvec.tex b/cheri/sail_latexcc/sailccxorvec.tex
deleted file mode 100644
index b3aa7372..00000000
--- a/cheri/sail_latexcc/sailccxorvec.tex
+++ /dev/null
@@ -1 +0,0 @@
-val xor_vec = {c: "xor_bits" , _: "xor_vec"} : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#('n)
diff --git a/cheri/sail_latexcc/sailcczW.tex b/cheri/sail_latexcc/sailcczW.tex
deleted file mode 100644
index a29ec93f..00000000
--- a/cheri/sail_latexcc/sailcczW.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload ~ = {not_bool, not_vec}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozAsznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozAsznine.tex
deleted file mode 100644
index 0b0a46e2..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozAsznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-val operator *_s = "mults_vec" : forall 'n . (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#(2 * 'n)
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozAuznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozAuznine.tex
deleted file mode 100644
index 5b762ba7..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozAuznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-val operator *_u = "mult_vec" : forall 'n . (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#(2 * 'n)
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozAznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozAznine.tex
deleted file mode 100644
index 2d188f63..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozAznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator *) = {mult_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozBznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozBznine.tex
deleted file mode 100644
index 432e85e5..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozBznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator +) = {add_range, add_int, add_vec, add_vec_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozDznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozDznine.tex
deleted file mode 100644
index d671e6b0..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozDznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator -) = {sub_range, sub_int, sub_vec, sub_vec_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozFznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozFznine.tex
deleted file mode 100644
index 3c2e441c..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozFznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator /) = {quotient_nat, quotient}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozIsznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozIsznine.tex
deleted file mode 100644
index 9b4ebe19..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozIsznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-val operator <_s  : forall 'n, 'n > 0. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> bool
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozIuznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozIuznine.tex
deleted file mode 100644
index 5b54235e..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozIuznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-val operator <_u  : forall 'n, 'n >= 0. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> bool
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozIzIznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozIzIznine.tex
deleted file mode 100644
index 51ff2b6c..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozIzIznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator <<) = {shift_bits_left, shiftl}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozIzJznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozIzJznine.tex
deleted file mode 100644
index d23f28dd..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozIzJznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator <=) = {lteq_atom, lteq_range_atom, lteq_atom_range, lteq_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozIznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozIznine.tex
deleted file mode 100644
index 8e5e3fe9..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozIznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator <) = {lt_atom, lt_range_atom, lt_atom_range, lt_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozJzJznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozJzJznine.tex
deleted file mode 100644
index 57ea823c..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozJzJznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator ==) = {eq_anything}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJsznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJsznine.tex
deleted file mode 100644
index 032e8600..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJsznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-val operator >=_s : forall 'n, 'n > 0. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> bool
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJuznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJuznine.tex
deleted file mode 100644
index eaa72e60..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJuznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-val operator >=_u : forall 'n, 'n >= 0. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> bool
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJznine.tex
deleted file mode 100644
index 5733b740..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator >=) = {gteq_atom, gteq_range_atom, gteq_atom_range, gteq_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzKsznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzKsznine.tex
deleted file mode 100644
index 0f0793a6..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzKsznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-val operator >>_s = "shift_bits_right_arith" : forall 'n 'm. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('m)) -> #\hyperref[zbits]{bits}#('n) effect {undef}
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzKznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzKznine.tex
deleted file mode 100644
index b129e9d2..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzKznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator >>) = {shift_bits_right, shiftr}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozKznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozKznine.tex
deleted file mode 100644
index a8da7e48..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozKznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator >) = {gt_atom, gt_range_atom, gt_atom_range, gt_int}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozQzQznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozQzQznine.tex
deleted file mode 100644
index 185f501e..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozQzQznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-val operator ^^ = {lem: "replicate_bits"} : forall 'n 'm, 'm >= 0 . (#\hyperref[zbits]{bits}#('n), atom('m)) -> #\hyperref[zbits]{bits}#('n * 'm)
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozQznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozQznine.tex
deleted file mode 100644
index 106b6064..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozQznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator ^) = {xor_vec, int_power}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozUznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozUznine.tex
deleted file mode 100644
index 4de737e0..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozUznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator |) = {or_bool, or_bits}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozfiveznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozfiveznine.tex
deleted file mode 100644
index 8d6b54c3..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozfiveznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator %) = {modulus}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozonezJznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozonezJznine.tex
deleted file mode 100644
index 22052668..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozonezJznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator !=) = {neq_atom, neq_int, neq_vec, neq_anything}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozsixznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozsixznine.tex
deleted file mode 100644
index 248fb15e..00000000
--- a/cheri/sail_latexcc/sailcczeightoperatorzzerozsixznine.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload (operator &) = {and_bool, and_bits}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczzeroextend.tex b/cheri/sail_latexcc/sailcczzeroextend.tex
deleted file mode 100644
index 0f754d44..00000000
--- a/cheri/sail_latexcc/sailcczzeroextend.tex
+++ /dev/null
@@ -1 +0,0 @@
-overload zero_extend = {mips_zero_extend}
\ No newline at end of file
diff --git a/cheri/sail_latexcc/sailcczzeros.tex b/cheri/sail_latexcc/sailcczzeros.tex
deleted file mode 100644
index 1c251eda..00000000
--- a/cheri/sail_latexcc/sailcczzeros.tex
+++ /dev/null
@@ -1 +0,0 @@
-val zeros : forall 'n, 'n >= 0 . unit -> #\hyperref[zbits]{bits}#('n)