======================================
F_OI_OBSERVER (invariant admissibility)
Successfully verified.
======================================
F_OI_PARITY_OBSERVER (invariant admissibility)
Successfully verified.
======================================
F_OI_OBSERVER.make (creator, inherited by F_OI_PARITY_OBSERVER)
Successfully verified.
======================================
F_OI_PARITY_OBSERVER.is_synchronized
Successfully verified.
======================================
F_OI_PARITY_OBSERVER.notify
Successfully verified.
======================================
F_OI_SIGN_OBSERVER (invariant admissibility)
Successfully verified.
======================================
F_OI_OBSERVER.make (creator, inherited by F_OI_SIGN_OBSERVER)
Successfully verified.
======================================
F_OI_SIGN_OBSERVER.is_synchronized
Successfully verified.
======================================
F_OI_SIGN_OBSERVER.notify
Successfully verified.
======================================
F_OI_SUBJECT (invariant admissibility)
Successfully verified.
======================================
F_OI_SUBJECT.make (creator)
Successfully verified.
======================================
F_OI_SUBJECT.update
Successfully verified.
======================================
F_OI_SUBJECT.register
Successfully verified.