Inference Rules
From Event-B
Revision as of 13:38, 3 July 2009 by imported>Nicolas (added FORALL_INST)
Conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Inference_Rules
Name | Rule | Side Condition | A/M
| |
---|---|---|---|---|
* | HYP | ![]() |
A
| |
* | HYP_OR | ![]() |
A
| |
* | CNTR | ![]() |
A
| |
* | FALSE_HYP | ![]() |
A
| |
* | TRUE_GOAL | ![]() |
A
| |
* | DBL_HYP | ![]() |
A
| |
* | AND_L | ![]() |
A
| |
* | AND_R | ![]() |
A
| |
* | IMP_L1 | ![]() |
A
| |
* | IMP_R | ![]() |
A
| |
* | IMP_AND_L | ![]() |
A
| |
* | IMP_OR_L | ![]() |
A
| |
* | NEG_IN_L | ![]() |
A
| |
* | NEG_IN_R | ![]() |
A
| |
* | XST_L | ![]() |
A
| |
* | ALL_R | ![]() |
A
| |
* | EQL_LR | ![]() |
![]() ![]() |
A
|
* | EQL_RL | ![]() |
![]() ![]() |
A
|
SUBSET_INTER | ![]() |
the ![]() |
A
| |
IN_INTER | ![]() |
the ![]() |
A
| |
NOTIN_INTER | ![]() |
the ![]() |
A
| |
* | CONTRADICT_L | ![]() |
M
| |
* | CONTRADICT_R | ![]() |
M
| |
* | CASE | ![]() |
M
| |
* | MH | ![]() |
M
| |
* | HM | ![]() |
M
| |
* | EQV | ![]() |
M
| |
* | OV_L | ![]() |
the ![]() |
M
|
* | OV_R | ![]() |
the ![]() |
M
|
* | OV_L | ![]() |
the ![]() |
M
|
* | OV_R | ![]() |
the ![]() |
M
|
* | DIS_BINTER_R | ![]() |
the occurrence of ![]() ![]() ![]() |
M
|
* | DIS_SETMINUS_R | ![]() |
the occurrence of ![]() ![]() ![]() |
M
|
* | SIM_REL_IMAGE_R | ![]() |
the occurrence of ![]() |
M
|
* | SIM_FCOMP_R | ![]() |
the occurrence of ![]() |
M
|
* | FIN_SUBSETEQ_R | ![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_BINTER_R | ![]() |
M
| |
* | FIN_SETMINUS_R | ![]() |
M
| |
* | FIN_REL_R | ![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_REL_IMG_R | ![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_REL_RAN_R | ![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_REL_DOM_R | ![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_FUN1_R | ![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_FUN2_R | ![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_FUN_IMG_R | ![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_FUN_RAN_R | ![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_FUN_DOM_R | ![]() |
the user has to write the set corresponding to ![]() |
M
|
* | LOWER_BOUND_L | ![]() |
![]() |
M
|
* | LOWER_BOUND_R | ![]() |
![]() |
M
|
* | UPPER_BOUND_L | ![]() |
![]() |
M
|
* | UPPER_BOUND_R | ![]() |
![]() |
M
|
* | FIN_LT_0 | ![]() |
M
| |
* | FIN_GE_0 | ![]() |
M
| |
* | CARD_INTERV | ![]() |
![]() |
M
|
* | CARD_EMPTY_INTERV | ![]() |
![]() |
M
|
* | CARD_SUBSETEQ | ![]() |
M
| |
* | FORALL_INST | ![]() |
M |