scheme 
iplane1 =
class
  type
   Time,
   Num,
   Place,	
   Status,
   PlaneInfo,
   Table=PlaneInfo-list      	
value
     CreateTable : Table =<..>,
     IsInTable: Num><Table->Bool,     
     AddPlane:PlaneInfo><Table-~->Table,
     DeletePlane:Num><Table-~->Table,
     ChangeTime:Table><Num><Time -~-> Table,
     ChangeStatus:Table><Num><Status -~-> Table,
     GetPlanes: Place><Table->Table,
     GetNum:PlaneInfo->Num,
     GetTimeR:PlaneInfo->Time,
     GetTimeT:PlaneInfo->Time,
     GetPlace:PlaneInfo->Place,
     GetStatus:PlaneInfo->Status,     
     MakePI:Time><Num><Place><Time><Status->PlaneInfo,          
     ThereIsSoPlane:Time><Table->Bool,
     getInfo:Num><Table->PlaneInfo,
     plustime : Time ><Time -> Time,
     Delta:Time,
     default:PlaneInfo    
axiom
     CreateTable is <..>,
     /*GetNum*/
     all n:Num,tt:Time,tr:Time,pl:Place,st:Status :-
         GetNum(MakePI(tt,n,pl,tr,st)) is n,
     /*GetTimeR*/
     all n:Num,tt:Time,tr:Time,pl:Place,st:Status :-
         GetTimeR(MakePI(tt,n,pl,tr,st)) is tr, 
     /*GetTimeT*/
     all n:Num,tt:Time,tr:Time,pl:Place,st:Status :-
         GetTimeT(MakePI(tt,n,pl,tr,st)) is tt,
     /*GetPlace*/
     all n:Num,tt:Time,tr:Time,pl:Place,st:Status :-
         GetPlace(MakePI(tt,n,pl,tr,st)) is pl,
     /*GetStatus*/
     all n:Num,tt:Time,tr:Time,pl:Place,st:Status :-
         GetStatus(MakePI(tt,n,pl,tr,st)) is st,                  
     /*IsInTable*/
     all num:Num :- 
         IsInTable(num,CreateTable) is false,       
     all num:Num,n:Num,tt:Time,tr:Time,pl:Place,st:Status ,tab:Table :-
         IsInTable(num,AddPlane(MakePI(tt,n,pl,tr,st),tab)) is
         if  num = n then true else IsInTable(num,tab) end ,
     all num:Num,n:Num,tab:Table :-         
         IsInTable(num,DeletePlane(n,tab)) is
         if num=n then false else IsInTable(num,tab) end,
     all num:Num,n:Num,tt:Time,st:Status ,tab:Table :-
         IsInTable(num,ChangeStatus(tab,n,st)) is 
         if num=n then true else IsInTable(num,tab) end,
     all num:Num,n:Num,tt:Time,tab:Table :-
         IsInTable(num,ChangeTime(tab,n,tt)) is 
         if num=n then true else IsInTable(num,tab) end ,     
     all num:Num,a:PlaneInfo  :-
         IsInTable(num,AddPlane(a,CreateTable)) is 
         if num=GetNum(a)  then true else false end,      
     all num:Num,a:PlaneInfo , tab :Table :- 
         IsInTable(num,AddPlane(a,tab)) is 
         if (num=GetNum(a)) then true else IsInTable(num,tab) end 	,     
    /*GetPlanes*/
    all pl:Place :-
        GetPlanes(pl,CreateTable ) is CreateTable ,
    all pl:Place,a:PlaneInfo :- 
        GetPlanes(pl,AddPlane(a,CreateTable)) is 
        if  pl=GetPlace(a)  then <.a.> else CreateTable end,
    all pl:Place,tab:Table,a:PlaneInfo :- 
        GetPlanes(pl,AddPlane(a,tab)) is 
        if  pl=GetPlace(a)  then <.a.>^GetPlanes(pl,tab) else GetPlanes(pl,tab) end,
    /*AddTable + ChangeStatus + ChangeTime*/    
    all num:Num,n:Num,tt:Time,tr:Time,pl:Place,st:Status ,tab:Table ,a:PlaneInfo:-
        DeletePlane(num,AddPlane(a,tab))  is
        if GetNum(a)=num then tab else   AddPlane(a,DeletePlane(num,tab)) end ,        
    all num:Num,st:Status,tab:Table ,a:PlaneInfo:-
        ChangeStatus(AddPlane(a,tab),num,st) is
         if (num=GetNum(a)) 
            then AddPlane(MakePI((GetTimeT(a),num,GetPlace(a),GetTimeR(a),st)),tab) 
            else AddPlane(a,ChangeStatus(tab,num,st)) end,
    all num:Num,tr:Time,tab:Table ,a:PlaneInfo:-      
        ChangeTime(AddPlane(a,tab),num,tr) is  
        if (num=GetNum(a))
            then AddPlane(MakePI((GetTimeT(a),num,GetPlace(a),tr,GetStatus(a))),tab) 
            else 
              if (ThereIsSoPlane(tr,tab) \/ tr=GetTimeR(a)) then
                 ChangeTime(AddPlane(a,tab),num,plustime(Delta,tr))
                else
            AddPlane(a,ChangeTime(tab,num,tr)) 
            end
        end ,
   /*IsThereIsSoPlane*/
   all num:Num,n:Num,tt:Time,tr:Time,pl:Place,st:Status ,tab:Table ,a:PlaneInfo:-
       ThereIsSoPlane(tr,CreateTable) is false,
   all tr:Time,tab:Table ,a:PlaneInfo:-
       ThereIsSoPlane(tr,AddPlane(a,tab)) is 
       if GetTimeR(a) = tr then true
          else
          ThereIsSoPlane(tr,tab) 
       end,
    /*getInfo*/
   all num:Num:-      
       getInfo(num,CreateTable) is default,
   all num:Num,tab:Table ,a:PlaneInfo:-
       getInfo(num,AddPlane(a,tab)) is
       if GetNum(a) = num then 
          if (~ThereIsSoPlane(GetTimeR(a),tab)) 
             then a 
             else  getInfo(num,AddPlane(MakePI((GetTimeT(a),GetNum(a),GetPlace(a),plustime(GetTimeR(a),Delta),GetStatus(a))),tab))   
          end 
       else getInfo(num,tab) end
end