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: |
|---|---|---|
| indiceswhere-base | ⊦ ar.indicesWhere(φ, 0) = [] | An Axiom |
| indiceswhere-rec | ⊦ n < # ar → ar.indicesWhere(φ, n + 1) = ar.indicesWhere(φ, n) + (φ(ar[n]) ⊃ n + [];[]) | An Axiom |
| indiceswhere | ⊦ ar.indicesWhere(φ) = ar.indicesWhere(φ, # ar) | An Axiom |
| mapindices-rec | ⊦ n < # ar → ar.mapIndices(n ' + nx, f) = (n < # ar ⊃ ar[n, f(ar[n])];ar).mapIndices(nx, f) | An Axiom |
| mapindices-base | ⊦ ar.mapIndices([], f) = ar | An Axiom |
| mapif-def | ⊦ ar.mapIf(φ, f) = ar.mapIndices(ar.indicesWhere(φ), f) | An Axiom |
| mapifn-def | ⊦ ar.mapIf(φ, f, n) = ar.mapIndices(ar.indicesWhere(φ, n), f) | An Axiom |
| mapindices-at | ⊦ ar.mapIndices(ns, f)[n] = (n ∈ ns ∧ n < # ar ⊃ f(ar[n]);ar[n]) | An Axiom |
| mapindices-size | ⊦ # ar.mapIndices(ns, f) = # ar | An Axiom |
| mapset-def | ⊦ n ∈ ns.map(fn) ↔ (∃ n0. n = fn(n0) ∧ n0 ∈ ns) | An Axiom |
| filterset-def | ⊦ n ∈ ns.filter(φn) ↔ n ∈ ns ∧ φn(n) | An Axiom |
| valid-indices | ⊦ valid-indices(ar, nx) ↔ nx < # ar | An Axiom |
| map-at | ⊦ ar.map(f)[n] = (n < # ar ⊃ f(ar[n]);ar[n]) | An Axiom |
| map-size | ⊦ # ar.map(f) = # ar | An Axiom |
| indices-where-in | ⊦ n ∈ ar.indicesWhere(φ) ↔ n < # ar ∧ φ(ar[n]) | A User Theorem |
| indices-where-in-h | ⊦ m ≤ # ar → (n ∈ ar.indicesWhere(φ, m) ↔ n < m ∧ φ(ar[n])) | A User Theorem |
| map-if-at | ⊦ n < # ar → ar.mapIf(φ, f)[n] = (φ(ar[n]) ⊃ f(ar[n]);ar[n]) | A User Theorem |
| map-if-size | ⊦ # ar.mapIf(φ, f) = # ar | A User Theorem |
| map-ifn-0 | ⊦ ar.mapIf(φ, f, 0) = ar | A User Theorem |
| map-ifn-at | ⊦ n < # ar ∧ m ≤ # ar → ar.mapIf(φ, f, m)[n] = (n < m ∧ φ(ar[n]) ⊃ f(ar[n]);ar[n]) | A User Theorem |
| map-ifn-full | ⊦ ar.mapIf(φ, f, # ar) = ar.mapIf(φ, f) | A User Theorem |
| map-ifn-size | n ≤ # ar ⊦ # ar.mapIf(φ, f, n) = # ar | A User Theorem |
| map-indices-append | ⊦ ¬ n ∈ nx ∧ valid-indices(ar, nx) ∧ n < # ar → ar.mapIndices(nx + n ', f) = ar.mapIndices(nx, f)[n, f(ar[n])] | A User Theorem |
| map-indices-at | ⊦ valid-indices(ar, nx) ∧ ¬ dups(nx) ∧ n < # ar → ar.mapIndices(nx, f)[n] = (n ∈ nx ⊃ f(ar[n]);ar[n]) | A User Theorem |
| map-indices-empty | ⊦ ar.mapIndices(∅, f) = ar | A User Theorem |
| map-indices-one | ⊦ n < # ar → ar.mapIndices(n ', f) = ar[n, f(ar[n])] | A User Theorem |
| map-indices-size | ⊦ valid-indices(ar, nx) → # ar.mapIndices(nx, f) = # ar | A User Theorem |
| map-set-empty | ⊦ (∅).map(fn) = ∅ | A User Theorem |
| valid-indices-append | ⊦ valid-indices(ar, nx0 + nx1) ↔ valid-indices(ar, nx0) ∧ valid-indices(ar, nx1) | A User Theorem |
| valid-indices-indiceswhere | ⊦ valid-indices(ar, ar.indicesWhere(φ)) | A User Theorem |
| valid-indices-indiceswhere-h | ⊦ n ≤ # ar → valid-indices(ar, ar.indicesWhere(φ, n)) | A User Theorem |
| valid-indices-indiceswhere-h-strong | ⊦ n ≤ # ar ∧ m ∈ ar.indicesWhere(φ, n) → m < n | A User Theorem |
| valid-indices-nodups | ⊦ ¬ dups(ar.indicesWhere(φ)) | A User Theorem |
| valid-indices-nodups-h | ⊦ n ≤ # ar → ¬ dups(ar.indicesWhere(φ, n)) | A User Theorem |
| valid-indices-nonrec | ⊦ valid-indices(ar, nx) ↔ (∀ n. n ∈ nx → n < # ar) | A User Theorem |
| valid-indices-one | ⊦ valid-indices(ar, n ') ↔ n < # ar | A User Theorem |
| valid-indices-simp | ⊦ nx < # ar → (¬ valid-indices(ar, nx) ↔ false) | A User Theorem |
| valid-indices-write | ⊦ valid-indices(ar[n, a], nx) ↔ valid-indices(ar, nx) | A User Theorem |