scheme 
TimeTable =
class
 type
   Time=Nat><Nat,
   Place=Text,	
   Status==layout|fligh|arrived,
   PlaneInfo=Time><Nat><Place><Time><Status,
   Table=PlaneInfo-list
 value
  CreateTable:Table =<..>  , 
  
  IsInTable: Nat><Table->Bool
  IsInTable(num,tab) as res
   post res=(exists (a,b,c,d,e): PlaneInfo :- 
       (a,b,c,d,e) isin (elems tab) /\ b=num ),
  
  less:Time><Time->Bool
  less((h1,m1),(h2,m2)) as res
      post   res = if (h1<h2) then true else if h1=h2 then m1 < m2
        else false
      end 
     end,

  AddPlane:PlaneInfo><Table->Table
  AddPlane((tt,num,place,tr,st),tab) as res
    post 
    true=(exists (a,b,c,d,e) : PlaneInfo :- 
          ((a,b,c,d,e) isin (elems res)) /\ 
          (tt=a /\ num=b /\ place=c )  /\
          (~(exists (a1,b1,c1,d1,e1): PlaneInfo :-
	  (a1,b1,c1,d1,e1)~=(a,b,c,d,e) /\ d1=d)) /\
          ({(a,b,c,d,e)}=(elems res ) \ (elems tab))/\
          (card (elems res))=(card (elems tab)) +1 /\ 
          less(tr,d)  
        ),
   DeletePlane:Nat><Table->Table
   DeletePlane(num,tab) as res
    post 
     true=(
           exists(a,b,c,d,e):PlaneInfo :-
           {(a,b,c,d,e)}= (elems tab)\(elems res) /\
           b=num /\
           ( a,b,c,d,e ) isin (elems tab) /\
           ~((a,b,c,d,e) isin (elems res))/\
           ~(exists (a1,b1,c1,d1,e1): PlaneInfo :- (a1,b1,c1,d1,e1)
	   isin  (elems res) /\b1=num ) /\
           (card (elems res))=(card (elems tab))-1
          ) ,
    ChangeTime:Table><Nat><Time -> Table
    ChangeTime(tab,num,time) as res
     post
      true=(
            exists (a,b,c,d,e) : PlaneInfo :-
            (a,b,c,d,e) isin (elems res) /\
            (exists (a1,b1,c1,d1,e1) : PlaneInfo :- (a1,b1,c1,d1,e1)
	    isin (elems tab) /\ a1=a /\ b=b1 /\ c1=c  /\ b=num /\less(time,d)/\
            (elems tab)\{(a1,b1,c1,d1,e1)}=(elems res)\{(a,b,c,d,e)}) /\
            ~(exists (a2,b2,c2,d2,e2) : PlaneInfo :- (a2,b2,c2,d2,e2)
	    isin (elems res) /\ d2=d) /\
            (less(time,d) \/ time=d)
           ) ,
   ChangeStatus:Table><Nat><Status -> Table
    ChangeStatus(tab,num,status) as res
     post
      true=(
            exists (a,b,c,d,e) : PlaneInfo :-
            (a,b,c,d,e) isin (elems res) /\
            (exists (a1,b1,c1,d1,e1) : PlaneInfo :- (a1,b1,c1,d1,e1)
	    isin (elems tab) /\ a1=a /\ b=b1 /\ c1=c  /\ b=num /\ e=status/\
            (elems tab)\{(a1,b1,c1,d1,e1)}=(elems res)\{(a,b,c,d,e)})
           ) ,

  GetPlanes: Place><Table->Table
  GetPlanes(place,tab) as res
    post  (all (a,b,c,d,e): PlaneInfo :- 
              (a,b,c,d,e) isin (elems res) /\
              c =place /\
              ( ~ (exists (a1,b1,c1,d1,e1) : PlaneInfo :-
	                  (a1,b1,c1,d1,e1) isin (elems tab)\(elems
			  res) /\ c1=place)))
                           



end