HoareRules

📁 Source: MRiscX/Hoare/HoareRules.lean

Statistics

Metric	Count
Definitions «term_∧∧_», «term∼_»	2
Theorems BL_SUBSET, BL_TO_WL, POST_WEAK, PRE_STR, S_COND, S_LOOP', S_SEQ, S_SEQ', WL_TO_BL	9
Total	11
⚠️ With sorry S_LOOP'	1

(root)

Definitions

Name	Category	Theorems
«term_∧∧_» 📖	CompOp	—
«term∼_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
BL_SUBSET 📖	—	hoare_triple_up	—	—	weak_with_less_BL_weakens
BL_TO_WL 📖	—	hoare_triple_up	—	—	weak_L_w_with_L_from_L_b
POST_WEAK 📖	—	hoare_triple_up	—	—	MState.runNSteps_code_remains
PRE_STR 📖	—	hoare_triple_up	—	—	—
S_COND 📖	—	hoare_triple_up	—	—	excluded_middle_implication
S_LOOP' 📖 ⚠️	—	hoare_triple_up ProgramCounter MState.pc	—	—	excluded_middle_implication
S_SEQ 📖	—	hoare_triple_up	—	—	MState.runNSteps_code_remains Nat.add_gt_zero MState.run_n_m_steps_comp MState.run_n_plus_m_intersect'
S_SEQ' 📖	—	hoare_triple_up	—	—	MState.runNSteps_code_remains Nat.add_gt_zero MState.run_n_m_steps_comp MState.run_n_plus_m_intersect'
WL_TO_BL 📖	—	ProgramCounter MState.pc hoare_triple_up	—	—	MState.runNSteps_diff

---

← Back to Index