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: |
|---|---|---|
| vals-empty | ⊦ val2vals(noval) = [] | An Axiom |
| vals-rec | ⊦ val2vals(val ++ val0) = val + val2vals(val0) | An Axiom |
| bytevalues-empty | ⊦ bytevalues([]) = [] | An Axiom |
| bytevalues-rec | ⊦ bytevalues(val ' + vals) = val .byteval + bytevalues(vals) | An Axiom |
| intvalues-empty | ⊦ intvalues([]) = [] | An Axiom |
| intvalues-rec | ⊦ intvalues(val ' + vals) = val .intval + intvalues(vals) | An Axiom |
| posints-value | ⊦ posints(val) ↔ posints(intvalues(val2vals(val))) | An Axiom |
| posints-empty | ⊦ posints([]) | An Axiom |
| posints-rec | ⊦ posints(i ' + ints) ↔ 0 ≤ i ∧ posints(ints) | An Axiom |
| posints-values | ⊦ posints(vals) ↔ posints(intvalues(vals)) | An Axiom |
| mkvalsb-rec | ⊦ mkjavavalues(by ' + bytes) = byteval(by) ' + mkjavavalues(bytes) | An Axiom |
| mkvalsb-empty | ⊦ mkjavavalues([]) = [] | An Axiom |
| is_bytelist-rec | ⊦ is_bytelist(val ' + vals) ↔ is_bytevalue(val) ∧ is_bytelist(vals) | An Axiom |
| is_bytelist-empty | ⊦ is_bytelist([]) | An Axiom |
| vals2ints-rec | ⊦ vals2ints(val ' + vals) = val2int(val) + vals2ints(vals) | An Axiom |
| vals2ints-empty | ⊦ vals2ints([]) = [] | An Axiom |
| vals2val-rec | ⊦ vals2val(val ' + vals) = val ++ vals2val(vals) | An Axiom |
| vals2val-empty | ⊦ vals2val([]) = noval | An Axiom |
| mkjval-def | ⊦ mkjavavalue(bytes) = vals2val(mkjavavalues(bytes)) | An Axiom |
| is_bytelistlist-rec | ⊦ is_bytelistlist(val ' + vals) ↔ is_bytelist(val2vals(val)) ∧ is_bytelistlist(vals) | An Axiom |
| is_bytelistlist-empty | ⊦ is_bytelistlist([]) | An Axiom |
| ints2bytes-rec | ⊦ is2bs(i ' + ints) = i2b(i) ' + is2bs(ints) | An Axiom |
| ints2bytes-empty | ⊦ is2bs([]) = [] | An Axiom |
| bytes2ints-rec | ⊦ bs2is(by ' + bytes) = b2i(by) ' + bs2is(bytes) | An Axiom |
| bytes2ints-empty | ⊦ bs2is([]) = [] | An Axiom |
| mkvalsr-rec | ⊦ mkjavavalues(r ' + refs) = refval(r) ' + mkjavavalues(refs) | An Axiom |
| mkvalsr-empty | ⊦ mkjavavalues([]) = [] | An Axiom |
| intvalues-rec-01 | ⊦ intvalues(i ' + ints) = intval(i) + intvalues(ints) | An Axiom |
| intvalues-empty-02 | ⊦ intvalues([]) = [] | An Axiom |
| nonnullrefs-yes | ⊦ is_referencevalue(val) ∧ val .refval ≠ jvmref → (val ' + vals) .nonnullrefs = val .refval + vals .nonnullrefs | An Axiom |
| nonnullrefs-no | ⊦ ¬ is_referencevalue(val) ∨ val .refval = jvmref → (val ' + vals) .nonnullrefs = vals .nonnullrefs | An Axiom |
| nonnullrefs-empty | ⊦ [] .nonnullrefs = [] | An Axiom |
| bytes2ints-one | ⊦ bs2is(by ') = b2i(by) ' | A User Theorem |
| bytevals-at | ⊦ n < # vals → (bytevalues(vals)[n]) = vals[n] .byteval | A User Theorem |
| bytevals-inj | ⊦ is_bytelist(vals) → mkjavavalues(bytevalues(vals)) = vals | A User Theorem |
| bytevalues-empty-01 | ⊦ bytevalues(vals) = [] ↔ vals = [] | A User Theorem |
| bytevalues-eq | ⊦ (∀ val. val ∈ vals ∨ val ∈ vals0 → is_bytevalue(val)) → (bytevalues(vals) = bytevalues(vals0) ↔ vals = vals0) | A User Theorem |
| bytevalues-len | ⊦ # bytevalues(vals) = # vals | A User Theorem |
| bytevalues-one | ⊦ bytevalues(val ') = val .byteval ' | A User Theorem |
| ibbis | ⊦ is2bs(bs2is(bytes)) = bytes | A User Theorem |
| ints2bytes-at | ⊦ n < # ints → (is2bs(ints)[n]) = i2b(ints[n]) | A User Theorem |
| ints2bytes-butlast | ⊦ ints ≠ [] → is2bs(ints) .butlast = is2bs(ints .butlast) | A User Theorem |
| ints2bytes-empty-01 | ⊦ is2bs(ints) = [] ↔ ints = [] | A User Theorem |
| ints2bytes-len | ⊦ # is2bs(ints) = # ints | A User Theorem |
| ints2bytes-one | ⊦ is2bs(i ') = i2b(i) ' | A User Theorem |
| intvalues-append | ⊦ intvalues(vals + vals0) = intvalues(vals) + intvalues(vals0) | A User Theorem |
| intvalues-at | ⊦ m < # vals → (intvalues(vals)[m]) = vals[m] .intval | A User Theorem |
| intvalues-empty-01 | ⊦ intvalues(vals) = [] ↔ vals = [] | A User Theorem |
| intvalues-len | ⊦ # intvalues(vals) = # vals | A User Theorem |
| intvalues-mklist | ⊦ intvalues(mklist(intval(i), n)) = mklist(i, n) | A User Theorem |
| intvalues-one | ⊦ intvalues(val ') = val .intval ' | A User Theorem |
| intvalues-put-sw | ⊦ m < # vals → intvalues(vals[m, val]) = (intvalues(vals)[m, val .intval]) | A User Theorem |
| is_bytelist | ⊦ is_bytelist(byteval(by) ' + vals) ↔ is_bytelist(vals) | A User Theorem |
| is_bytelist-one | ⊦ is_bytelist(val ') ↔ is_bytevalue(val) | A User Theorem |
| is_bytes-vals | ⊦ is_bytelist(mkjavavalues(bytes)) | A User Theorem |
| isbytelist-all | ⊦ is_bytelist(vals) ↔ (∀ val. val ∈ vals → is_bytevalue(val)) | A User Theorem |
| javavalues-in | ⊦ val ∈ mkjavavalues(refs) ↔ is_referencevalue(val) ∧ val .refval ∈ refs | A User Theorem |
| javavalues-is-bytevalue | ⊦ val ∈ mkjavavalues(int2bytes(i)) → is_bytevalue(val) | A User Theorem |
| mkjava-bvs | ⊦ bytevalues(mkjavavalues(bytes)) = bytes | A User Theorem |
| mkjava-empty | ⊦ mkjavavalues(bytes) = [] ↔ bytes = [] | A User Theorem |
| mkjava-len | ⊦ # mkjavavalues(bytes) = # bytes | A User Theorem |
| mkjavavalues | ⊦ ¬ is_bytevalue(val) → ¬ val ∈ mkjavavalues(bytes) | A User Theorem |
| mkjavavalues-append | ⊦ mkjavavalues(refs + refs0) = mkjavavalues(refs) + mkjavavalues(refs0) | A User Theorem |
| mkjavavalues-append-01 | ⊦ mkjavavalues(bytes + bytes0) = mkjavavalues(bytes) + mkjavavalues(bytes0) | A User Theorem |
| mkjavavalues-byte-lastrec | ⊦ is_bytevalue(val) → mkjavavalues(bytes + val .byteval) = mkjavavalues(bytes) + val | A User Theorem |
| mkjavavalues-byte-lastrec-01 | ⊦ is_bytevalue(val) → mkjavavalues(bytes + val .byteval ') = mkjavavalues(bytes) + val | A User Theorem |
| mkjavavalues-empty | ⊦ mkjavavalues(refs) = [] ↔ refs = [] | A User Theorem |
| mkjavavalues-rec | ⊦ refs ≠ [] → mkjavavalues(refs) = refval(refs .first) + mkjavavalues(refs .rest) | A User Theorem |
| mkjavavalues-restn | ⊦ n ≤ # bytes → restn(n, mkjavavalues(bytes)) = mkjavavalues(restn(n, bytes)) | A User Theorem |
| mkvals-single | ⊦ mkjavavalues(by ') = byteval(by) ' | A User Theorem |
| mkvalsr-at | ⊦ n < # refs → (mkjavavalues(refs)[n]) = refval(refs[n]) | A User Theorem |
| mkvalsr-len | ⊦ # mkjavavalues(refs) = # refs | A User Theorem |
| mkvalsr-one | ⊦ mkjavavalues(r ') = refval(r) ' | A User Theorem |
| mkvalues-butlast | ⊦ bytes ≠ [] → mkjavavalues(bytes) .butlast = mkjavavalues(bytes .butlast) | A User Theorem |
| mkvalues-last | ⊦ bytes ≠ [] → mkjavavalues(bytes) .last = byteval(bytes .last) | A User Theorem |
| nonnullrefs-append | ⊦ (vals + vals0) .nonnullrefs = vals .nonnullrefs + vals0 .nonnullrefs | A User Theorem |
| nonnullrefs-dups | ⊦ dups(vals .nonnullrefs) ↔ (∃ r, m, n. vals[m] = refval(r) ∧ vals[n] = refval(r) ∧ r ≠ jvmref ∧ m ≠ n ∧ m < # vals ∧ n < # vals) | A User Theorem |
| nonnullrefs-dups-firstoc | ⊦ dups(vals .nonnullrefs) ↔ (∃ r, vals0, vals1, vals2. vals = vals0 + (refval(r) + (vals1 + (refval(r) + vals2))) ∧ r ≠ jvmref ∧ ¬ refval(r) ∈ vals0 ∧ ¬ refval(r) ∈ vals1) | A User Theorem |
| nonnullrefs-in | ⊦ r ∈ vals .nonnullrefs ↔ r ≠ jvmref ∧ (∃ m. vals[m] = refval(r) ∧ m < # vals) | A User Theorem |
| nonnullrefs-in-firstoc | ⊦ r ∈ vals .nonnullrefs ↔ r ≠ jvmref ∧ (∃ vals0, vals1. vals = vals0 + (refval(r) + vals1) ∧ ¬ refval(r) ∈ vals0) | A User Theorem |
| nonnullrefs-null | ⊦ ¬ jvmref ∈ vals .nonnullrefs | A User Theorem |
| nonnullrefs-ok | ⊦ r ≠ jvmref → (refval(r) ' + vals) .nonnullrefs = r ' + vals .nonnullrefs | A User Theorem |
| nonnullrefs-one | ⊦ r ≠ jvmref → refval(r) ' .nonnullrefs = r ' | A User Theorem |
| nonnullrefs-one-no | ⊦ ¬ is_referencevalue(val) ∨ val .refval = jvmref → val ' .nonnullrefs = [] | A User Theorem |
| nonnullrefs-one-yes | ⊦ is_referencevalue(val) ∧ val .refval ≠ jvmref → val ' .nonnullrefs = val .refval ' | A User Theorem |
| posints-one | ⊦ posints(i ') ↔ 0 ≤ i | A User Theorem |
| posints-rec-01 | ⊦ 0 < i → (posints(i ' + ints) ↔ posints(ints)) | A User Theorem |
| posints-rec-02 | ⊦ 0 ≤ i → (posints(i ' + ints) ↔ posints(ints)) | A User Theorem |
| val-inj-01 | ⊦ val2vals(vals2val(vals)) = vals | A User Theorem |
| vals-at | ⊦ 0 ≤ n ∧ n < # bytes → (mkjavavalues(bytes)[n]) = byteval(bytes[n]) | A User Theorem |
| vals2int-one | ⊦ vals2ints(val ') = val2int(val) ' | A User Theorem |
| vals2ints-empty-01 | ⊦ vals2ints(vals) = [] ↔ vals = [] | A User Theorem |
| vals2ints-len | ⊦ # vals2ints(vals) = # vals | A User Theorem |
| vals2val-single | ⊦ vals2val(val ') = val ++ noval | A User Theorem |