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 < # ar → ⌜ar⌝ [n] = ar[n] | An Axiom |
| tostream-size | ⊦ # ⌜ar⌝ = ⌜# ar⌝ | An Axiom |
| emptystream | ⊦ σ⊥ = ⌜λ n. zero⌝ | An Axiom |
| toar-at | finp(σ), ⌜n⌝ < # σ ⊦ σ.ar[n] = σ[n] | An Axiom |
| toar-size | finp(σ) ⊦ # σ.ar = (# σ).n | An Axiom |
| ar-empty | ⊦ ⌜mkarray(0)⌝ = [] | A User Theorem |
| at-emptystream | ⊦ (σ⊥)[n] = zero | A User Theorem |
| finp-ar | ⊦ ¬ finp(⌜ar⌝ ) ↔ false | A User Theorem |
| from-emptystream | ⊦ σ⊥ from n = σ⊥ | A User Theorem |
| split-prefix-append-to | ⊦ # σ0 = ∞ → ((σ0 to n) + σ1 = σ0 ↔ σ1 = σ0 from n) | A User Theorem |
| toar | ⊦ ⌜ar⌝ .ar = ar | A User Theorem |
| toar-disj | ⊦ ⌜ar⌝ ≠ ⌜nf⌝ | A User Theorem |
| toar-empty | ⊦ [].ar = mkarray(0) | A User Theorem |
| tostream-inj | ⊦ ⌜ar0⌝ = ⌜ar1⌝ ↔ ar0 = ar1 | A User Theorem |