Skip to content

Added fupd_plain_soundness_no_lc_strong

Added the lemma fupd_plain_soundness_no_lc_strong, which is a generalisation of the adequacy theorem of the Trillium instance of Iris.

Notably, it lifts the original soundness theorem to be a greatest fixpoint of nested fancy updates. The soundness theorem was primarily conducted by @amintimany .

EDIT: I was confused by the inclusion of £ m in the _no_lc lemmas, but added it here for consistency. Since the proofs are strictly in the realm of has_no_lc it seems superfluous to include them (even for future-proving)

EDIT 2: The theorem that this is used for can be found here

Edited by Jonas Kastberg

Merge request reports