Extension Proof Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Nicolas m Extension Rewrite Rules moved to Extension Proof Rules: Gathering rewrite and inference rules for extensions in the same page. |
imported>Nicolas mNo edit summary |
||
| Line 2: | Line 2: | ||
Rules without a <tt>*</tt> are planned to be implemented in future versions. | Rules without a <tt>*</tt> are planned to be implemented in future versions. | ||
Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]]. | Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]]. | ||
== Rewrite Rules == | |||
{{RRHeader}} | {{RRHeader}} | ||
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_COND_BTRUE}}||<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COND_BTRUE}}||<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math>|| || A | ||
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_COND_BFALSE}}||<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COND_BFALSE}}||<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math>|| || A | ||
|} | |} | ||
== Inference Rules == | |||
{{RRHeader}} | |||
|} | |||
[[Category:User documentation|The Proving Perspective]] | [[Category:User documentation|The Proving Perspective]] | ||
[[Category:Rodin Platform|The Proving Perspective]] | [[Category:Rodin Platform|The Proving Perspective]] | ||
[[Category:User manual|The Proving Perspective]] | [[Category:User manual|The Proving Perspective]] | ||
Revision as of 10:27, 9 September 2010
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.
Rewrite Rules
| Name | Rule | Side Condition | A/M | |
|---|---|---|---|---|
| * | SIMP_SPECIAL_COND_BTRUE |
 |
A | |
| * | SIMP_SPECIAL_COND_BFALSE |
 |
A |
Inference Rules
| Name | Rule | Side Condition | A/M |
|---|
