This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| tostream-at | ⊦ n < # buf → ⌜buf⌝ [n] = buf[n] | An Axiom |
| tostream-size | ⊦ # ⌜buf⌝ = ⌜# buf⌝ | An Axiom |
| emptystream | ⊦ σ⊥ = ⌜λ n. zero⌝ | An Axiom |
| tobuf-at | finp(σ), ⌜n⌝ < # σ ⊦ σ.buf[n] = σ[n] | An Axiom |
| tobuf-size | finp(σ) ⊦ # σ.buf = (# σ).n | An Axiom |
| at-emptystream | ⊦ (σ⊥)[n] = zero | A User Theorem |
| buf-empty | ⊦ ⌜mkbuf(0)⌝ = [] | A User Theorem |
| emptystream-cancel | ⊦ # σ ≠ ∞ → (σ + σ⊥ = σ⊥ ↔ σ = σ⊥ to (# σ).n) | A User Theorem |
| finp-buf | ⊦ ¬ finp(⌜buf⌝ ) ↔ false | A User Theorem |
| from-empty | ⊦ ⌜buf⌝ from # buf = [] | A User Theorem |
| from-emptystream | ⊦ σ⊥ from n = σ⊥ | A User Theorem |
| from-to-rest | ⊦ # buf = n + m → (⌜buf⌝ from n) to m = ⌜buf⌝ from n | A User Theorem |
| split-prefix-append-to | ⊦ # σ0 = ∞ → ((σ0 to n) + σ1 = σ0 ↔ σ1 = σ0 from n) | A User Theorem |
| tobuf | ⊦ ⌜buf⌝ .buf = buf | A User Theorem |
| tobuf-disj | ⊦ ⌜buf⌝ ≠ ⌜nf⌝ | A User Theorem |
| tobuf-empty | ⊦ [].buf = mkbuf(0) | A User Theorem |
| tobuf-rev | ⊦ # σ ≠ ∞ → ⌜σ.buf⌝ = σ | A User Theorem |
| tostream-inj | ⊦ ⌜buf0⌝ = ⌜buf1⌝ ↔ buf0 = buf1 | A User Theorem |
| tostream-to-same | ⊦ ⌜buf⌝ to # buf = ⌜buf⌝ | A User Theorem |