| Symbol | Specification | Kind | Type |
|---|---|---|---|
| # . | Agentlist | f | Agentlist → nat |
| #oc | Agentlist | f | Agent × Agentlist → nat |
| . ' | Agentlist | f | Agent → Agentlist |
| . * . | nat-mult | f | nat × nat → nat |
| . + . | nat-basic2 | f | nat × nat → nat |
| . + . | Agentlist | f | Agent × Agentlist → Agentlist |
| . + . | Agentlist | f | Agent × Agent → Agentlist |
| . + . | Agentlist | f | Agentlist × Agentlist → Agentlist |
| . + . | Agentlist | f | Agentlist × Agent → Agentlist |
| . ++ . | Agentlist | f | Agentlist × Agent → Agentlist |
| . +1 | nat-basic1 | f | nat → nat |
| . - . | nat | f | nat × nat → nat |
| . -1 | nat-basic1 | f | nat → nat |
| . -1l . | Agentlist | f | Agentlist × nat → Agentlist |
| . -1l . | Agentlist | f | Agentlist × Agent → Agentlist |
| . -l . | Agentlist | f | Agentlist × Agent → Agentlist |
| . .butlast | Agentlist | f | Agentlist → Agentlist |
| . .cmd | action | f | action → command |
| . .first | Agentlist | f | Agentlist → Agent |
| . .from | action | f | action → Agent |
| . .id | Agent | f | Agent → nat |
| . .last | Agentlist | f | Agentlist → Agent |
| . .rest | Agentlist | f | Agentlist → Agentlist |
| . .to | action | f | action → Agent |
| . < . | Agentlist | p | Agentlist × Agentlist |
| . < . | nat-basic1 | p | nat × nat |
| . > . | nat | p | nat × nat |
| . [ . ] | Agentlist | f | Agentlist × nat → Agent |
| . [ . ] | Agentlist | f | Agentlist × nat × Agent → Agentlist |
| . \ . | Agentlist | f | Agentlist × Agentlist → Agentlist |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ∈ . | Agentlist | p | Agent × Agentlist |
| . ∪ . | Agentlist | f | Agentlist × Agentlist → Agentlist |
| . ⊆ . | Agentlist | p | Agentlist × Agentlist |
| . ⊆m . | Agentlist | p | Agentlist × Agentlist |
| . ⊑ . | Agentlist | p | Agentlist × Agentlist |
| . ⊒ . | Agentlist | p | Agentlist × Agentlist |
| [] | Agentlist | c | Agentlist |
| a | action | v | action |
| a0 | action | v | action |
| a1 | action | v | action |
| a2 | action | v | action |
| Abort8-UserCmd | command | c | command |
| Abort9-UserCmd | command | c | command |
| action | action | s | |
| Action | action | f | Agent × command × Agent → action |
| afterdeclassifyCCD4ASM-CreditCardCenterCmd | command | c | command |
| ag | Agent | v | Agent |
| ag0 | Agent | v | Agent |
| ag1 | Agent | v | Agent |
| ag2 | action | v | Agent |
| Agent | Agent | s | |
| Agentlist | Agentlist | s | |
| agl | Agentlist | v | Agentlist |
| agl0 | Agentlist | v | Agentlist |
| agl1 | Agentlist | v | Agentlist |
| agl10 | Agentlist | v | Agentlist |
| agl2 | Agentlist | v | Agentlist |
| agl3 | Agentlist | v | Agentlist |
| agl4 | Agentlist | v | Agentlist |
| agl5 | Agentlist | v | Agentlist |
| agl6 | Agentlist | v | Agentlist |
| agl7 | Agentlist | v | Agentlist |
| agl8 | Agentlist | v | Agentlist |
| agl9 | Agentlist | v | Agentlist |
| BookFlightOffer-AirlineCmd | command | c | command |
| BookFlightOfferstate6-AirlineCmd | command | c | command |
| BookFlightOfferstate7-AirlineCmd | command | c | command |
| BookSelected-TravelPlannerCmd | command | c | command |
| BookSelectedstate2-TravelPlannerCmd | command | c | command |
| butlastn | Agentlist | f | nat × Agentlist → Agentlist |
| cmd | command | v | command |
| cmd0 | command | v | command |
| cmd1 | command | v | command |
| cmd2 | command | v | command |
| command | command | s | |
| Confirm-UserCmd-4 | command | c | command |
| ConfirmRelease-UserCmd-3 | command | c | command |
| DeclassifiedCCD-TravelPlannerCmd | command | c | command |
| declassifyCCD4ASM-CreditCardCenterCmd | command | c | command |
| disj | Agentlist | p | Agentlist × Agentlist |
| dups | Agentlist | p | Agentlist |
| exAgent | exAgent | p | Agent |
| exAirline | exAgent | p | Agent |
| exCreditCardCenter | exAgent | p | Agent |
| exTravelAgency | exAgent | p | Agent |
| exTravelPlanner | exAgent | p | Agent |
| exUser | exAgent | p | Agent |
| fillfirst | Agentlist | f | nat × Agent × Agentlist → Agentlist |
| filter | Agentlist | f | Agentlist × Agentlist → Agentlist |
| firstn | Agentlist | f | nat × Agentlist → Agentlist |
| frome | Agentlist | f | Agentlist × Agent → Agentlist |
| GetDeclassifiedCCD-CreditCardCenterCmd | command | c | command |
| GetFlightOffers-AirlineCmd | command | c | command |
| GetFlightOffers-TravelAgencyCmd | command | c | command |
| GetFlightOffers-TravelPlannerCmd | command | c | command |
| GetInputRequestData-UserCmd-1 | command | c | command |
| GetSingleSelection-UserCmd-2 | command | c | command |
| Init-GetInputRequestData-TravelPlannerCmd | command | c | command |
| isAbort8-UserCmd | command | p | command |
| isAbort9-UserCmd | command | p | command |
| isafterdeclassifyCCD4ASM-CreditCardCenterCmd | command | p | command |
| isAirline | Agent | p | Agent |
| isBookFlightOffer-AirlineCmd | command | p | command |
| isBookFlightOfferstate6-AirlineCmd | command | p | command |
| isBookFlightOfferstate7-AirlineCmd | command | p | command |
| isBookSelected-TravelPlannerCmd | command | p | command |
| isBookSelectedstate2-TravelPlannerCmd | command | p | command |
| isConfirm-UserCmd-4 | command | p | command |
| isConfirmRelease-UserCmd-3 | command | p | command |
| isCreditCardCenter | Agent | p | Agent |
| isDeclassifiedCCD-TravelPlannerCmd | command | p | command |
| isdeclassifyCCD4ASM-CreditCardCenterCmd | command | p | command |
| isGetDeclassifiedCCD-CreditCardCenterCmd | command | p | command |
| isGetFlightOffers-AirlineCmd | command | p | command |
| isGetFlightOffers-TravelAgencyCmd | command | p | command |
| isGetFlightOffers-TravelPlannerCmd | command | p | command |
| isGetInputRequestData-UserCmd-1 | command | p | command |
| isGetSingleSelection-UserCmd-2 | command | p | command |
| isInit-GetInputRequestData-TravelPlannerCmd | command | p | command |
| isOkConfirmBooking-TravelPlannerCmd | command | p | command |
| isOkPayCommission-AirlineCmd | command | p | command |
| isPayCommission-TravelAgencyCmd | command | p | command |
| isReleaseCCD-CreditCardCenterCmd | command | p | command |
| isRetFlightOffers-TravelAgencyCmd | command | p | command |
| isRetFlightOffers-TravelPlannerCmd | command | p | command |
| isRetFlightOffersstate1-TravelPlannerCmd | command | p | command |
| isTravelAgency | Agent | p | Agent |
| isTravelPlanner | Agent | p | Agent |
| isUser | Agent | p | Agent |
| lastn | Agentlist | f | nat × Agentlist → Agentlist |
| m | nat-basic2 | v | nat |
| m0 | Agent | v | nat |
| mkAirline | Agent | f | nat → Agent |
| mkCreditCardCenter | Agent | f | nat → Agent |
| mklist | Agentlist | f | Agent × nat → Agentlist |
| mkTravelAgency | Agent | f | nat → Agent |
| mkTravelPlanner | Agent | f | nat → Agent |
| mkUser | Agent | f | nat → Agent |
| n | nat-basic1 | v | nat |
| n0 | nat-basic1 | v | nat |
| n1 | nat-basic1 | v | nat |
| nat | nat-basic1 | s | |
| NUMOFAirline | exAgent | c | nat |
| NUMOFAPPSANDUSERS | exAgent | c | nat |
| NUMOFCreditCardCenter | exAgent | c | nat |
| NUMOFTravelAgency | exAgent | c | nat |
| NUMOFTravelPlanner | exAgent | c | nat |
| NUMOFUser | exAgent | c | nat |
| OkConfirmBooking-TravelPlannerCmd | command | c | command |
| OkPayCommission-AirlineCmd | command | c | command |
| PayCommission-TravelAgencyCmd | command | c | command |
| perm | Agentlist | p | Agentlist × Agentlist |
| pos | Agentlist | f | Agent × Agentlist → nat |
| ReleaseCCD-CreditCardCenterCmd | command | c | command |
| restn | Agentlist | f | nat × Agentlist → Agentlist |
| RetFlightOffers-TravelAgencyCmd | command | c | command |
| RetFlightOffers-TravelPlannerCmd | command | c | command |
| RetFlightOffersstate1-TravelPlannerCmd | command | c | command |
| rev | Agentlist | f | Agentlist → Agentlist |
| rmdup | Agentlist | f | Agentlist → Agentlist |
| sublist | Agentlist | f | nat × nat × Agentlist → Agentlist |