timedef : CONTEXT =
BEGIN
natlim: TYPE = [0..29];
time: TYPE = DATATYPE
    fintime(dur: natlim),
    infinity
  END; 
    zero:time = fintime(0);
    one:time = fintime(1);
    two:time = fintime(2);
    three:time = fintime(3);
    four:time = fintime(4);
    nineteen:time = fintime(19);
    twenty:time = fintime(20);
    twenty_nine:time = fintime(29);
    thirty:time = fintime(30);  

    leq(t1:time,t2:time):bool =
       IF fintime?(t1) AND fintime?(t2) THEN dur(t1) <= dur(t2)
       ELSE infinity?(t2)
       ENDIF;

    geq(t1:time,t2:time):bool =
       IF fintime?(t1) AND fintime?(t2) THEN dur(t1) >= dur(t2)
       ELSE infinity?(t1)
       ENDIF;

    less(t1:time,t2:time):bool =
       IF fintime?(t1) AND fintime?(t2) THEN dur(t1) < dur(t2)
       ELSE NOT (infinity?(t1)) AND infinity?(t2)
       ENDIF;
      

    greater(t1:time,t2:time):bool =
       IF fintime?(t1) AND fintime?(t2) THEN dur(t1) > dur(t2)
       ELSE NOT(infinity?(t2)) AND infinity?(t1)
       ENDIF;

    plus(t1:time,t2:time):time =
       IF fintime?(t1) AND fintime?(t2) THEN fintime(dur(t1) + dur(t2))
       ELSE infinity
       ENDIF;

    minus(t1:time, t2:{t: time | fintime?(t)}):time =
       IF fintime?(t1) AND dur(t1) >= dur(t2) THEN fintime(dur(t1) - dur(t2))
       ELSE infinity
       ENDIF;

    fintime_unique: LEMMA
       (FORALL (z1,z2:nat):(fintime(z1) = fintime(z2)) => (z1 = z2));

    fintime_elim_1: LEMMA
       (FORALL (z:nat, t:{t: time | fintime?(t)}):
      %(FORALL (z:nat, t:time):
         (fintime(z) = t) => (z = dur(t)));
        %(fintime(z) = t) = (z = dur(t)));

    fintime_elim_2: LEMMA
       (FORALL (z:nat, t:{t: time | fintime?(t)}):
      %(FORALL (z:nat, t:time):
         (t = fintime(z)) => (dur(t) = z));
        %(t = fintime(z)) = (dur(t) = z));

    fintime_dur: LEMMA
       (FORALL  (t:{t: time | fintime?(t)}): fintime(dur(t)) = t);

    trans_order: LEMMA
       (FORALL (t1,t2,t3:time): leq(t1, t2) AND  leq(t2, t3) => leq(t1,  t3));



END