Skip to main content

Module proofs

planarian_policy

Module proofs 

Source
Expand description

The properties SPEC §7 and §17a ask of decide, proved about decide_spec; decide is proved equal to it (its ensures).