Extension Proof Rules

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	$\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

Inference Rules

	Name	Rule	Side Condition	A/M