enrich data with
   functions 
      isNull-IFlowUtil : Data → Boolean;
      comment: ok;
       
       . + . : Integer × Integer → Integer;
      comment: ok;
       
       . - . : Integer × Integer → Integer prio 8 left;
      comment: ok, prio is necessary;
       
       . < . : Integer × Integer → Boolean prio 5;
      comment: ok, prio is necessary;
       
       . <= . : Integer × Integer → Boolean prio 5;
      comment: ok, prio is necessary;
       
       . > . : Integer × Integer → Boolean prio 5;
      comment: ok, prio is necessary;
       
       . >= . : Integer × Integer → Boolean prio 5;
      comment: ok, prio is necessary;
       
      inc : Data → Data;
      comment: ok, data must a Nat.;
       
      size : Data → nat;
      comment: ok, data must be a ListOfData.;
       
      get : ListOfData × nat → Data;
      comment: ok, returns null for bad indices.;
       
      ListOfFlightOffer2ListOfData : ListOfFlightOffer → ListOfData;
      comment: ok;
       
      ListOfData2ListOfFlightOffer : ListOfData → ListOfFlightOffer;
      comment: ok;
       
      ListOfGPSPos2ListOfData : ListOfGPSPos → ListOfData;
      comment: ok;
       
      ListOfData2ListOfGPSPos : ListOfData → ListOfGPSPos;
      comment: ok;
       
      set-id : FlightOffer × Integer → FlightOffer;
      comment: todo;
       
      set-airline : FlightOffer × String → FlightOffer;
      comment: todo;
       
      set-latitude : GPSPos × String → GPSPos;
      comment: todo;
       
      set-longitude : GPSPos × String → GPSPos;
      comment: todo;
       
   predicates 
      isTrue : Data;
      comment: ok;
       
      nonNull : Data;
      comment: ok;
       
      nonNull : ListOfData;
      comment: ok;
       
   
   axioms 
      plus-def :  ⊦ a_Integer + a_Integer0 = mkInteger(a_Integer .value + a_Integer0 .value);
      minus-def :  ⊦ a_Integer - a_Integer0 = mkInteger(a_Integer .value - a_Integer0 .value);
      ls-def :  ⊦ (a_Integer < a_Integer0) = mkBoolean(a_Integer .value < a_Integer0 .value);
      le-def :  ⊦ (a_Integer <= a_Integer0) = mkBoolean(a_Integer .value ≤ a_Integer0 .value);
      gr-def :  ⊦ (a_Integer > a_Integer0) = mkBoolean(a_Integer .value > a_Integer0 .value);
      ge-def :  ⊦ (a_Integer >= a_Integer0) = mkBoolean(a_Integer .value ≥ a_Integer0 .value);
      listOfFlightOffer-empty-def :  ⊦ ListOfFlightOffer2ListOfData([]) = [];
      used for : s, ls;
       
      listOfFlightOffer-rec-def
      : ⊦ 
          ListOfFlightOffer2ListOfData(a_FlightOffer + a_ListOfFlightOffer)
        = wrapFlightOffer2Data(a_FlightOffer) + ListOfFlightOffer2ListOfData(a_ListOfFlightOffer);
      used for : s, ls;
       
      listOfFlightOffer-notNull :  ⊦ a_ListOfFlightOffer ≠ [] → ListOfFlightOffer2ListOfData(a_ListOfFlightOffer) .first ≠ null;
      used for : s, ls, generated;
       
      listOfFlightOffer-empty :  ⊦ ListOfFlightOffer2ListOfData(a_ListOfFlightOffer) = [] ↔ a_ListOfFlightOffer = [];
      used for : s, ls, generated;
       
      ListOfData2ListOfFlightOffer-empty-def :  ⊦ ListOfData2ListOfFlightOffer([]) = [];
      used for : s, ls;
       
      ListOfData2ListOfFlightOffer-rec-def :  ⊦ ListOfData2ListOfFlightOffer(d + dl) = d .FlightOffer + ListOfData2ListOfFlightOffer(dl);
      used for : s, ls;
       
      listOfGPSPos-empty-def :  ⊦ ListOfGPSPos2ListOfData([]) = [];
      used for : s, ls;
       
      listOfGPSPos-rec-def
      :  ⊦ ListOfGPSPos2ListOfData(a_GPSPos + a_ListOfGPSPos) = wrapGPSPos2Data(a_GPSPos) + ListOfGPSPos2ListOfData(a_ListOfGPSPos);
      used for : s, ls;
       
      listOfGPSPos-notNull :  ⊦ a_ListOfGPSPos ≠ [] → ListOfGPSPos2ListOfData(a_ListOfGPSPos) .first ≠ null;
      used for : s, ls, generated;
       
      listOfGPSPos-empty :  ⊦ ListOfGPSPos2ListOfData(a_ListOfGPSPos) = [] ↔ a_ListOfGPSPos = [];
      used for : s, ls, generated;
       
      ListOfData2ListOfGPSPos-empty-def :  ⊦ ListOfData2ListOfGPSPos([]) = [];
      used for : s, ls;
       
      ListOfData2ListOfGPSPos-rec-def :  ⊦ ListOfData2ListOfGPSPos(d + dl) = d .GPSPos + ListOfData2ListOfGPSPos(dl);
      used for : s, ls;
       
      isNull-IFlowUtil-def :  ⊦ isNull-IFlowUtil(d) = mkBoolean(d = null);
      used for : s, ls;
       
      get-empty :  ⊦ get([], n) = null;
      used for : s, ls;
       
      get-found :  ⊦ get(d + dl, 0) = d;
      used for : s, ls;
       
      get-rec :  ⊦ n ≠ 0 → get(d + dl, n) = get(dl, n -1);
      isTrue-def :  ⊦ isTrue(d) ↔ isBoolean(d) ∧ d .Boolean .value;
      inc-def :  ⊦ inc(d) = mkNat(d .nat + 1);
      size-def :  ⊦ size(d) = # d .ListOfData;
      nonNull-def :  ⊦ nonNull(d) ↔ nonNull(d .ListOfData);
      nonNull-empty :  ⊦ nonNull([]);
      used for : s, ls;
       
      nonNull-rec :  ⊦ nonNull(d + dl) ↔ d ≠ null ∧ nonNull(dl);
      used for : s, ls;
       
      size :  ⊦ # dl = 0 ↔ dl = [];
      used for : s, ls, generated;
       
      size-empty :  ⊦ size(wrapListOfData2Data([])) = 0;
      used for : s, ls, generated;
       
      size-wrap :  ⊦ size(wrapListOfData2Data(d + dl)) = size(wrapListOfData2Data(dl)) + 1;
      used for : s, ls, generated;
       
      nonNull-wrap :  ⊦ nonNull(wrapListOfData2Data(d + dl)) ↔ d ≠ null ∧ nonNull(wrapListOfData2Data(dl));
      used for : s, ls, generated;
       
      get-too-large :  ⊦ ¬ n < # dl → get(dl, n) = null;
      used for : s, ls, generated;
       
      get-zero-empty :  ⊦ dl = [] → get(dl, 0) = null;
      used for : generated;
       
      get-zero-nonempty :  ⊦ dl ≠ [] → get(dl, 0) = dl .first;
      used for : generated;
       
      get-rec :  ⊦ dl ≠ [] → get(dl, n + 1) = get(dl .rest, n);
      used for : generated;
       
      nonNull-get-num : n < m ⊦ size(wrapListOfData2Data(dl)) = ((* m)) ∧ nonNull(wrapListOfData2Data(dl)) → get(dl, (* n)) ≠ null;
      used for : s, ls, generated;
       
end enrich