Commit 88fe918b authored by Ike Mulder's avatar Ike Mulder
Browse files


parent 518525f8
......@@ -46,6 +46,7 @@ The main workhorse of Diaframe. It performs a single *chunk of steps* of the aut
- `e = K e'` and we can find a specification `SPEC {{ L }} e' {{ U }}`: new goal is `|={⊤}=> L ∗ (∀ v, U -∗ WP (K v) {{ Φ }})`
- `G = |={E1, E2}=> ∃.. x, L ∗ G'`: perform steps of the automation until `L` has been proven, and `G'` remains.
- `G = ⊳ G'`: introduce all laters in the context, continue with goal `G'`.
Note that case 2 and 4 may indeed perform multiple of the steps described in the paper, which is why we say that `iStepS` performs a chunk of steps.
#### iStepsS
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment