This file contains some minor lemmas to ease the prove in the "main" file "HoareRules". Also, those lemmas can be used to deepen the understanding of the weak function.

theorem weak_with_less_BL_weakens (s s' : MState) (L_w L_b L : Set UInt64) (c : Code) : weak s s' L_w L_b c → weak s s' L_w (L_b \ L) c

theorem weak_L_w_with_L_from_L_b (s s' : MState) (L_w L_b L : Set UInt64) (c : Code) : L ⊆ L_b → weak s s' L_w L_b c → weak s s' (L_w ∪ L) (L_b \ L) c

def weakLoop (s : MState) (l : UInt64) (C I : Assertion) : Prop

Loop-style weakening relation used in proving the loop Hoare rule: from state s at label l, the invariant I is maintained until the condition C is met.

Equations

• One or more equations did not get rendered due to their size.