I
M
P
_
N
oninterference_
E
xtension
Small_Step
Definitions
Idempotence
Overapproximation
Correctness_Lemmas
Correctness_Theorem