Extension Proof Rules

From Event-B
Revision as of 10:23, 9 September 2010 by imported>Nicolas (Extension Rewrite Rules moved to Extension Proof Rules: Gathering rewrite and inference rules for extensions in the same page.)
Jump to navigationJump to search

Rules that are marked with a * in the first column are implemented in the latest version of Rodin. Rules without a * are planned to be implemented in future versions. Other conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Rewrite_Rules.


  Name Rule Side Condition A/M
SIMP_SPECIAL_COND_BTRUE
  \operatorname{COND}(\btrue, E_1, E_2)  \;\;\defi\;\;  E_1 A
SIMP_SPECIAL_COND_BFALSE
  \operatorname{COND}(\bfalse, E_1, E_2)  \;\;\defi\;\;  E_2 A