scheme 
mytest =
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) is (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)) is if (h1<h2) then true else if h1=h2 then m1 < m2 else false end end,
  
  plustime:Time><Time->Time
  plustime((h1,m1),(h2,m2)) is ((h1+h2+(m1+m2)/60)\24,(m1+m2)\60),
  
  ThereIsSoPlane:Time><Table->Bool
  ThereIsSoPlane(time,tab) is 
   if (tab=<..>) then false else
      let(a,b,c,d,e)=(hd tab) in
       if (time=d) then true else
        ThereIsSoPlane(time,tl tab) end end end,       
        
  GetPlanes: Place><Table->Table
  GetPlanes(place,tab) is
  if tab=<..> then tab
   else
   let (a,b,c,d,e) = (hd tab) in
    if (c=place) then <.hd tab.>^GetPlanes(place,tl tab) 
     else   GetPlanes(place,tl tab) 
    end
  end
  end,        
  
  getInfo:Nat><Table-~->PlaneInfo
  getInfo(num,tab) is
   let (a,b,c,d,e) = (hd tab) in 
    if (num=b) then  (a,b,c,d,e) 
      else
      getInfo(num,tl tab)
    end
   end
  pre  ~IsInTable(num,tab),   
    
  AddPlaneMain:PlaneInfo><Table-~->Table
  AddPlaneMain((tt,num,place,tr,st),tab) is
   if (ThereIsSoPlane(tr,tab)) then 
       AddPlaneMain((tt,num,place,plustime((0,2),tt),st),tab)
       else
       AddPlane((tt,num,place,tr,st),tab)
       end
  pre ~IsInTable(num,tab),
       
  AddPlane:PlaneInfo><Table-~->Table
  AddPlane((tt,num,place,tr,st),tab) is
   if (tab=<..>) then tab^<.(tt,num,place,tr,st).> else
    let (a,b,c,d,e)= (hd tab) in
     case (less(tt,a)) of
     true-> <.(tt,num,place,tr,st).>^tab,
     false-><.hd tab.>^AddPlane((tt,num,place,tr,st),tl tab)
     end
    end
   end  
   pre ~IsInTable(num,tab),
        
  DeletePlane:Nat><Table-~->Table
  DeletePlane(num,tab) is  
     if (tab=<..>) then tab 
      else 
       let(a,b,c,d,e)=(hd tab) in
        if (num=b) then (tl tab) 
         else <.hd tab.>^DeletePlane(num,tl tab)
        end
       end
     end            
  pre IsInTable(num,tab),
          
  ChangeTime:Table><Nat><Time -~-> Table
  ChangeTime(tab,num,time) is
   if(ThereIsSoPlane(time,tab)) then
     let (a1,b1,c1,d1,e1) =getInfo(num,tab) in
        AddPlaneMain((a1,b1,c1,d1,layout),DeletePlane(num,tab))
     end
   else          
    if(tab=<..>) then tab else
      let(a,b,c,d,e) = (hd tab)  in
       if (num=b) then <.(time,b,c,d,e).>^(tl tab) else <.hd tab.>^ChangeTime(tl tab,num,time) end        
      end
    end      
   end
  pre IsInTable(num,tab),
     
  ChangeStatus:Table><Nat><Status -~-> Table
  ChangeStatus(tab,num,stat) is
   if(tab=<..>) then tab else 
    let (a,b,c,d,e)=(hd tab) in
     if (num=b) then <.(a,b,c,d,stat).>^(tl tab) else
      <.hd tab.>^ChangeStatus(tl tab,num,stat) 
     end 
    end
   end
  pre IsInTable(num,tab),
  
  /*drivers ---- ???*/
  
  Trasing:Text-> Unit
  Trasing(T) is (),
  
  IsInTableDriver:Nat><Table->Bool  
  IsInTableDriver(num,tab) is 
   if IsInTable(num,tab) = (exists (a,b,c,d,e): PlaneInfo :-(a,b,c,d,e) isin (elems tab) /\ b=num )
    then 
     true
    else
     local in Trasing("In IsInTable");false end
    end,
  
  lessDriver:Time><Time->Bool
  lessDriver((h1,m1),(h2,m2)) is 
   if less((h1,m1),(h2,m2)) = if (h1<h2) then true else if h1=h2 then m1 < m2 else false end end
    then 
     true
    else
   local in Trasing("In less");false end
   end,
  
  plustimeDriver:Time><Time->Bool
  plustimeDriver((h1,m1),(h2,m2)) is 
   if (plustime((h1,m1),(h2,m2))=((h1+h2+(m1+m2)/60)\24,(m1+m2)\60))
    then 
     true
    else
     local in Trasing("In plustime");false end
    end,
    
  ThereIsSoPlaneDrive:Time><Table->Bool
  ThereIsSoPlaneDrive(time,tab) is
   if ThereIsSoPlane(time,tab)=(exists (a,b,c,d,e) : PlaneInfo :- (a,b,c,d,e) isin (elems tab) /\ d=time)
        then 
         true 
        else
         local in Trasing ("In ThereIsSoPlane");false end
        end ,
        
  GetPlanesDriver: Place><Table->Bool
  GetPlanesDriver(place,tab) is   
   if  let res=GetPlanes(place,tab) in
       (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        
  		then true
  		else
  		local in Trasing("in GetPlanes");false end  		
  		end,
  		
  getInfoDriver:Nat><Table-~->Bool
  getInfoDriver(num,tab) is
  if(~IsInTable(num,tab))
   then 
    local in Trasing("pre in getInfo"); false end
   else
    if let (a,b,c,d,e)=getInfo(num,tab) in
       (((a,b,c,d,e) isin (elems tab) )/\(b=num))   end
       then 
        true
       else
        local  in Trasing("in getInfo"); false end
       end
    end   ,
        
    
  AddPlaneMainDriver:PlaneInfo><Table -> Bool
  AddPlaneMainDriver((tt,num,place,tr,st),tab) is
   if (IsInTable(num,tab))
  then 
   local in Trasing("pre in AddPlane ");false end
  else
  if  let res=AddPlaneMain((tt,num,place,tr,st),tab) in
      (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)  
        )
      end
     then
      true
     else
      local in Trasing("in addPlaneMain");false end
  end  end,
    
  DeletePlaneDriver:Nat><Table -> Bool
  DeletePlaneDriver(num,tab) is   
    if ~IsInTable(num,tab)
     then 
    local in Trasing("in pre DeletePlane");false end
    else
     if let res=DeletePlane(num,tab) in
      (
           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
          )
     end
     then
      true
     else
      local in Trasing("in DeletePlane)");false end
   end  
 end,
 
  ChangeTimeDriver:Table><Nat><Time -> Bool
  ChangeTimeDriver(tab,num,time) is
   if ~IsInTable(num,tab)
     then 
     local in Trasing("in pre ChangeTime ");false end
   else
    if  let res =  ChangeTime(tab,num,time) in
      (
            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)
           )
      end
     then
      true
     else
      local in Trasing("in ChangeTime");false end
   end  
  end,
  
  ChangeStatusDriver:Table><Nat><Status -> Bool
  ChangeStatusDriver(tab,num,stat) is
   if ~IsInTable(num,tab)
     then 
     local in Trasing("in pre ChangeStatus");false end
    else
     if  let res=ChangeStatus(tab,num,stat) in
         (
            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=stat/\
            (elems tab)\{(a1,b1,c1,d1,e1)}=(elems res)\{(a,b,c,d,e)})
           )      
      end
     then
      true
     else
      local in Trasing("in ChangeStatus");false end
   end  
  end 
end