HoareRules

Statistics

Metric	Count
Definitions	0
Theorems `BL_SUBSET`, `BL_TO_WL`, `POST_WEAK`, `PRE_STR`, `S_COND`, `S_LOOP`, `S_SEQ`, `S_SEQ'`, `WL_TO_BL`	9
Total	9

Name	Kind	Assumes	Proves	Validates	Depends On
`BL_SUBSET` 📖	mathematical	`hoare_triple_up`	`hoare_triple_up`	—	`weak_with_less_BL_weakens`
`BL_TO_WL` 📖	mathematical	`hoare_triple_up`	`hoare_triple_up`	—	`weak_L_w_with_L_from_L_b`
`POST_WEAK` 📖	mathematical	`hoare_triple_up`	`hoare_triple_up`	—	`MState.runNSteps_code_remains`
`PRE_STR` 📖	mathematical	`hoare_triple_up`	`hoare_triple_up`	—	—
`S_COND` 📖	mathematical	`hoare_triple_up` `Assertion.And` `Assertion.Not`	`hoare_triple_up`	—	`excluded_middle_implication`
`S_LOOP` 📖	mathematical	`hoare_triple_up` `ProgramCounter` `MState.pc`	`hoare_triple_up`	—	`MState.code_remains_same` `Nat.add_gt_zero` `MState.runNSteps_add` `MState.run_n_plus_m_pc_not_in_set`
`S_SEQ` 📖	mathematical	`hoare_triple_up`	`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'` 📖	mathematical	`hoare_triple_up`	`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` 📖	mathematical	`ProgramCounter` `MState.pc` `hoare_triple_up`	`hoare_triple_up`	—	`MState.runNSteps_diff`

---