Extension Proof Rules
From Event-B
Revision as of 17:15, 3 September 2010 by imported>Nicolas (added rules SIMP_SPECIAL_COND_BTRUE and SIMP_SPECIAL_COND_BFALSE)
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 |
A | |||
SIMP_SPECIAL_COND_BFALSE |
A |