docs: timeless rule for invariants

docs/derived.tex

@@ -202,6 +202,18 @@ The following rules can be derived for Hoare triples.
 \inferH{Ht-false}
   {}
   {\hoare{\FALSE}{\expr}{\Ret \val. \prop}[\mask]}
+\and
+\inferH{Ht-inv}
+  {\hoare{\later\propC*\prop}{\expr}{\Ret\val.\later\propC*\propB}[\mask] \and
+   \physatomic{\expr}
+  }
+  {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]}
+\and
+\inferH{Ht-inv-timeless}
+  {\hoare{\propC*\prop}{\expr}{\Ret\val.\propC*\propB}[\mask] \and
+   \physatomic{\expr} \and \timeless\propC
+  }
+  {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]}
 \end{mathparpagebreakable}
 
 \paragraph{Lifting of operational semantics.}