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: |
|---|---|---|
| plus-def | ⊦ a_Integer + a_Integer0 = mkInteger(a_Integer .value + a_Integer0 .value) | An Axiom |
| minus-def | ⊦ a_Integer - a_Integer0 = mkInteger(a_Integer .value - a_Integer0 .value) | An Axiom |
| ls-def | ⊦ (a_Integer < a_Integer0) = mkBoolean(a_Integer .value < a_Integer0 .value) | An Axiom |
| le-def | ⊦ (a_Integer <= a_Integer0) = mkBoolean(a_Integer .value ≤ a_Integer0 .value) | An Axiom |
| gr-def | ⊦ (a_Integer > a_Integer0) = mkBoolean(a_Integer .value > a_Integer0 .value) | An Axiom |
| ge-def | ⊦ (a_Integer >= a_Integer0) = mkBoolean(a_Integer .value ≥ a_Integer0 .value) | An Axiom |
| listOfFlightOffer-empty-def | ⊦ ListOfFlightOffer2ListOfData([]) = [] | An Axiom |
| listOfFlightOffer-rec-def | ⊦ ListOfFlightOffer2ListOfData(a_FlightOffer + a_ListOfFlightOffer) = wrapFlightOffer2Data(a_FlightOffer) + ListOfFlightOffer2ListOfData(a_ListOfFlightOffer) | An Axiom |
| listOfFlightOffer-notNull | ⊦ a_ListOfFlightOffer ≠ [] → ListOfFlightOffer2ListOfData(a_ListOfFlightOffer) .first ≠ null | An Axiom |
| listOfFlightOffer-empty | ⊦ ListOfFlightOffer2ListOfData(a_ListOfFlightOffer) = [] ↔ a_ListOfFlightOffer = [] | An Axiom |
| ListOfData2ListOfFlightOffer-empty-def | ⊦ ListOfData2ListOfFlightOffer([]) = [] | An Axiom |
| ListOfData2ListOfFlightOffer-rec-def | ⊦ ListOfData2ListOfFlightOffer(d + dl) = d .FlightOffer + ListOfData2ListOfFlightOffer(dl) | An Axiom |
| listOfGPSPos-empty-def | ⊦ ListOfGPSPos2ListOfData([]) = [] | An Axiom |
| listOfGPSPos-rec-def | ⊦ ListOfGPSPos2ListOfData(a_GPSPos + a_ListOfGPSPos) = wrapGPSPos2Data(a_GPSPos) + ListOfGPSPos2ListOfData(a_ListOfGPSPos) | An Axiom |
| listOfGPSPos-notNull | ⊦ a_ListOfGPSPos ≠ [] → ListOfGPSPos2ListOfData(a_ListOfGPSPos) .first ≠ null | An Axiom |
| listOfGPSPos-empty | ⊦ ListOfGPSPos2ListOfData(a_ListOfGPSPos) = [] ↔ a_ListOfGPSPos = [] | An Axiom |
| ListOfData2ListOfGPSPos-empty-def | ⊦ ListOfData2ListOfGPSPos([]) = [] | An Axiom |
| ListOfData2ListOfGPSPos-rec-def | ⊦ ListOfData2ListOfGPSPos(d + dl) = d .GPSPos + ListOfData2ListOfGPSPos(dl) | An Axiom |
| isNull-IFlowUtil-def | ⊦ isNull-IFlowUtil(d) = mkBoolean(d = null) | An Axiom |
| get-empty | ⊦ get([], n) = null | An Axiom |
| get-found | ⊦ get(d + dl, 0) = d | An Axiom |
| get-rec-01 | ⊦ n ≠ 0 → get(d + dl, n) = get(dl, n -1) | An Axiom |
| isTrue-def | ⊦ isTrue(d) ↔ isBoolean(d) ∧ d .Boolean .value | An Axiom |
| inc-def | ⊦ inc(d) = mkNat(d .nat + 1) | An Axiom |
| size-def | ⊦ size(d) = # d .ListOfData | An Axiom |
| nonNull-def | ⊦ nonNull(d) ↔ nonNull(d .ListOfData) | An Axiom |
| nonNull-empty | ⊦ nonNull([]) | An Axiom |
| nonNull-rec | ⊦ nonNull(d + dl) ↔ d ≠ null ∧ nonNull(dl) | An Axiom |
| size | ⊦ # dl = 0 ↔ dl = [] | An Axiom |
| size-empty | ⊦ size(wrapListOfData2Data([])) = 0 | An Axiom |
| size-wrap | ⊦ size(wrapListOfData2Data(d + dl)) = size(wrapListOfData2Data(dl)) + 1 | An Axiom |
| nonNull-wrap | ⊦ nonNull(wrapListOfData2Data(d + dl)) ↔ d ≠ null ∧ nonNull(wrapListOfData2Data(dl)) | An Axiom |
| get-too-large | ⊦ ¬ n < # dl → get(dl, n) = null | An Axiom |
| get-zero-empty | ⊦ dl = [] → get(dl, 0) = null | An Axiom |
| get-zero-nonempty | ⊦ dl ≠ [] → get(dl, 0) = dl .first | An Axiom |
| get-rec-02 | ⊦ dl ≠ [] → get(dl, n + 1) = get(dl .rest, n) | An Axiom |
| nonNull-get-num | n < m ⊦ size(wrapListOfData2Data(dl)) = ((* m)) ∧ nonNull(wrapListOfData2Data(dl)) → get(dl, (* n)) ≠ null | An Axiom |