Difference between revisions of "Extension Proof Rules"
From Event-B
Jump to navigationJump to searchimported>Nicolas |
imported>WikiSysop |
||
(One intermediate revision by the same user not shown) | |||
Line 10: | Line 10: | ||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_COND}}||<math> \operatorname{COND}(C, E, E) \;\;\defi\;\; E </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_COND}}||<math> \operatorname{COND}(C, E, E) \;\;\defi\;\; E </math>|| || A | ||
|} | |} | ||
− | |||
=== Inference Rules === | === Inference Rules === |
Latest revision as of 15:38, 29 November 2019
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 | |
* | SIMP_MULTI_COND |
![]() |
A |
Inference Rules
Name | Rule | Side Condition | A/M | |
---|---|---|---|---|
* | DATATYPE_DISTINCT_CASE |
![]() |
where ![]() ![]() ![]() ![]() ![]() ![]() |
M
|
* | DATATYPE_INDUCTION |
![]() |
where ![]() ![]() ![]() ![]() ![]() ![]() |
M |