[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	data	f	ListOfData → nat
# .	string-less	f	string → nat
# .	Agentlist	f	Agentlist → nat
#oc	Agentlist	f	Agent × Agentlist → nat
. '	string-append	f	char → string
. '	Agentlist	f	Agent → Agentlist
. * .	int-mult	f	int × int → int
. * .	nat-mult	f	nat × nat → nat
. + .	datafuns	f	Integer × Integer → Integer
. + .	int-basic2	f	int × int → int
. + .	data	f	Data × ListOfData → ListOfData
. + .	nat-basic2	f	nat × nat → nat
. + .	data	f	GPSPos × ListOfGPSPos → ListOfGPSPos
. + .	string-data	f	char × string → string
. + .	data	f	FlightOffer × ListOfFlightOffer → ListOfFlightOffer
. + .	string-append	f	string × string → string
. + .	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	int-basic1	f	int → int
. +1	nat-basic1	f	nat → nat
. - .	datafuns	f	Integer × Integer → Integer
. - .	int-abs	f	int × int → int
. - .	nat	f	nat × nat → nat
. -1	int-basic1	f	int → int
. -1	nat-basic1	f	nat → nat
. -1l .	Agentlist	f	Agentlist × nat → Agentlist
. -1l .	Agentlist	f	Agentlist × Agent → Agentlist
. -l .	Agentlist	f	Agentlist × Agent → Agentlist
. .1	data	f	Data → Data
. .2	data	f	Data → Data
. .Agent	data	f	Data → Agent
. .agentlist	data	f	Message → Agentlist
. .airline	data	f	FlightOffer → String
. .Boolean	data	f	Data → Boolean
. .butlast	Agentlist	f	Agentlist → Agentlist
. .call	name	f	name → string
. .ccd	data	f	Content → CreditCardDetails
. .char1	string-data	f	string → char
. .cmd	action	f	action → command
. .cmd	name	f	name → command
. .content	data	f	Message → Content
. .CreditCardDetails	data	f	Data → CreditCardDetails
. .data	data	f	Content → Data
. .date	data	f	RequestData → String
. .first	data	f	ListOfData → Data
. .first	data	f	ListOfGPSPos → GPSPos
. .first	data	f	ListOfFlightOffer → FlightOffer
. .first	Agentlist	f	Agentlist → Agent
. .FlightOffer	data	f	Data → FlightOffer
. .flightOffer	data	f	Content → FlightOffer
. .flightOffers	data	f	Content → ListOfFlightOffer
. .from	action	f	action → Agent
. .GPSPos	data	f	Data → GPSPos
. .id	Agent	f	Agent → nat
. .id	data	f	Content → Integer
. .id	data	f	FlightOffer → Integer
. .Integer	data	f	Data → Integer
. .last	Agentlist	f	Agentlist → Agent
. .latitude	data	f	GPSPos → String
. .ListOfData	data	f	Data → ListOfData
. .ListOfFlightOffer	data	f	Data → ListOfFlightOffer
. .ListOfGPSPos	data	f	Data → ListOfGPSPos
. .longitude	data	f	GPSPos → String
. .methodname	name	f	name → string
. .msg	data	f	Data → Message
. .name	name	f	name → string
. .nat	data	f	Data → nat
. .receiver	data	f	Content → String
. .RequestData	data	f	Data → RequestData
. .requestData	data	f	Content → RequestData
. .rest	data	f	ListOfData → ListOfData
. .rest	data	f	ListOfGPSPos → ListOfGPSPos
. .rest	data	f	ListOfFlightOffer → ListOfFlightOffer
. .rest	Agentlist	f	Agentlist → Agentlist
. .rstring	string-data	f	string → string
. .selection	data	f	Content → ListOfData
. .String	data	f	Data → String
. .to	action	f	action → Agent
. .value	data	p	Boolean
. .value	data	f	String → string
. .value	data	f	Integer → int
. .what	data	f	Content → Data
. < .	data	p	ListOfData × ListOfData
. < .	Agentlist	p	Agentlist × Agentlist
. < .	datafuns	f	Integer × Integer → Boolean
. < .	string-less	p	char × char
. < .	string-less	p	string × string
. < .	int-basic1	p	int × int
. < .	nat-basic1	p	nat × nat
. <= .	datafuns	f	Integer × Integer → Boolean
. > .	nat	p	nat × nat
. > .	datafuns	f	Integer × Integer → Boolean
. > .	int-abs	p	int × int
. >= .	datafuns	f	Integer × Integer → Boolean
. [ . ]	Agentlist	f	Agentlist × nat → Agent
. [ . ]	Agentlist	f	Agentlist × nat × Agent → Agentlist
. \ .	Agentlist	f	Agentlist × Agentlist → Agentlist
. ≤ .	int-abs	p	int × int
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
. ∈ .	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
[]	data	c	ListOfFlightOffer
[]	data	c	ListOfGPSPos
[]	data	c	ListOfData
~ .	int-abs	f	int → int
a	action	v	action
a_Boolean	data	v	Boolean
a_Boolean0	data	v	Boolean
a_Boolean1	data	v	Boolean
a_Boolean2	data	v	Boolean
a_CreditCardDetails	data	v	CreditCardDetails
a_CreditCardDetails0	data	v	CreditCardDetails
a_CreditCardDetails1	data	v	CreditCardDetails
a_CreditCardDetails2	data	v	CreditCardDetails
a_FlightOffer	data	v	FlightOffer
a_FlightOffer0	data	v	FlightOffer
a_FlightOffer1	data	v	FlightOffer
a_FlightOffer2	data	v	FlightOffer
a_GPSPos	data	v	GPSPos
a_GPSPos0	data	v	GPSPos
a_GPSPos1	data	v	GPSPos
a_GPSPos2	data	v	GPSPos
a_Integer	data	v	Integer
a_Integer0	data	v	Integer
a_Integer1	data	v	Integer
a_Integer2	data	v	Integer
a_ListOfData	data	v	ListOfData
a_ListOfData0	data	v	ListOfData
a_ListOfFlightOffer	data	v	ListOfFlightOffer
a_ListOfFlightOffer0	data	v	ListOfFlightOffer
a_ListOfGPSPos	data	v	ListOfGPSPos
a_ListOfGPSPos0	data	v	ListOfGPSPos
a_RequestData	data	v	RequestData
a_RequestData0	data	v	RequestData
a_RequestData1	data	v	RequestData
a_RequestData2	data	v	RequestData
a_String	data	v	String
a_String0	data	v	String
a_String1	data	v	String
a_String2	data	v	String
a0	action	v	action
a1	action	v	action
a2	action	v	action
Abort8-UserCmd	command	c	command
Abort8-UserCmd#	ASM	pr	action : name × Agent → Data
Abort9-UserCmd	command	c	command
Abort9-UserCmd#	ASM	pr	action : name × Agent → Data
abs	int-abs	f	int → int
action	action	s
Action	action	f	Agent × command × Agent → action
afterdeclassifyCCD4ASM-CreditCardCenterCmd	command	c	command
afterdeclassifyCCD4ASM-CreditCardCenterCmd#	ASM	pr	action : name × Agent → Data
ag	Agent	v	Agent
ag0	Agent	v	Agent
ag1	Agent	v	Agent
ag2	action	v	Agent
ag3	state	v	Agent
ag4	state	v	Agent
ag5	state	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
Airline-flightOffers	name	c	name
allNull	state	p	(name × Agent → Data)
ASM#	ASM	pr	: name × Agent → Data × bool
BookFlightOffer-AirlineCmd	command	c	command
BookFlightOffer-AirlineCmd#	ASM	pr	action : name × Agent → Data
BookFlightOfferstate6-AirlineCmd	command	c	command
BookFlightOfferstate6-AirlineCmd#	ASM	pr	action : name × Agent → Data
BookFlightOfferstate7-AirlineCmd	command	c	command
BookFlightOfferstate7-AirlineCmd#	ASM	pr	action : name × Agent → Data
BookSelected-TravelPlannerCmd	command	c	command
BookSelected-TravelPlannerCmd#	ASM	pr	action : name × Agent → Data
BookSelectedstate2-TravelPlannerCmd	command	c	command
BookSelectedstate2-TravelPlannerCmd#	ASM	pr	action : name × Agent → Data
bool	bool	s
Boolean	data	s
boolvar	bool	v	bool
boolvar0	bool	v	bool
butlastn	Agentlist	f	nat × Agentlist → Agentlist
char	char	s
char	char	v	char
char0	char	v	char
char1	char	v	char
char2	char	v	char
char3	string-less	v	char
cmd	command	v	command
cmd0	command	v	command
cmd1	command	v	command
cmd2	command	v	command
cntnt	data	v	Content
cntnt0	data	v	Content
cntnt1	data	v	Content
command	command	s
Confirm-UserCmd-4	command	c	command
Confirm-UserCmd-4#	ASM	pr	action : name × Agent → Data
ConfirmRelease-UserCmd-3	command	c	command
ConfirmRelease-UserCmd-3#	ASM	pr	action : name × Agent → Data
Content	data	s
CreditCardCenter-ccd	name	c	name
CreditCardDetails	data	s
d	data	v	Data
d0	data	v	Data
d1	data	v	Data
d2	data	v	Data
d4	state	v	Data
d5	state	v	Data
Data	data	s
DeclassifiedCCD-TravelPlannerCmd	command	c	command
DeclassifiedCCD-TravelPlannerCmd#	ASM	pr	action : name × Agent → Data
declassify-count	name	f	string → name
declassifyCCD-CreditCardCenter	localMethods	f	CreditCardDetails → CreditCardDetails
declassifyCCD4ASM-CreditCardCenterCmd	command	c	command
declassifyCCD4ASM-CreditCardCenterCmd#	ASM	pr	action : name × Agent → Data
disj	Agentlist	p	Agentlist × Agentlist
dl	data	v	ListOfData
dl0	data	v	ListOfData
dl1	data	v	ListOfData
dl10	data	v	ListOfData
dl2	data	v	ListOfData
dl3	data	v	ListOfData
dl4	data	v	ListOfData
dl5	data	v	ListOfData
dl6	data	v	ListOfData
dl7	data	v	ListOfData
dl8	data	v	ListOfData
dl9	data	v	ListOfData
DONE	ASMAUX	pr	command × Agent : name × Agent → Data
dups	Agentlist	p	Agentlist
exAgent	exAgent	p	Agent
exAirline	exAgent	p	Agent
exCreditCardCenter	exAgent	p	Agent
EXEC	ASM	pr	action : name × Agent → Data
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
filterOffers-Airline	localMethods	f	RequestData × ListOfFlightOffer → ListOfFlightOffer
firstn	Agentlist	f	nat × Agentlist → Agentlist
FlightOffer	data	s
frome	Agentlist	f	Agentlist × Agent → Agentlist
get	datafuns	f	ListOfData × nat → Data
getConfirmRelease	userMethods	p	nat
GetDeclassifiedCCD-CreditCardCenterCmd	command	c	command
GetDeclassifiedCCD-CreditCardCenterCmd#	ASM	pr	action : name × Agent → Data
GetFlightOffers-AirlineCmd	command	c	command
GetFlightOffers-AirlineCmd#	ASM	pr	action : name × Agent → Data
GetFlightOffers-TravelAgencyCmd	command	c	command
GetFlightOffers-TravelAgencyCmd#	ASM	pr	action : name × Agent → Data
GetFlightOffers-TravelPlannerCmd	command	c	command
GetFlightOffers-TravelPlannerCmd#	ASM	pr	action : name × Agent → Data
GetInputRequestData-UserCmd-1	command	c	command
GetInputRequestData-UserCmd-1#	ASM	pr	action : name × Agent → Data
getMultipleSelection	userMethods	f	ListOfData × nat → ListOfData
getSingleSelection	userMethods	f	ListOfData × nat → Data
GetSingleSelection-UserCmd-2	command	c	command
GetSingleSelection-UserCmd-2#	ASM	pr	action : name × Agent → Data
GPSPos	data	s
i	int-basic1	v	int
i0	int-basic1	v	int
inc	datafuns	f	Data → Data
init	state	p	(name × Agent → Data)
Init-GetInputRequestData-TravelPlannerCmd	command	c	command
Init-GetInputRequestData-TravelPlannerCmd#	ASM	pr	action : name × Agent → Data
InitValue	userMethods	c	Data
int	int-basic1	s
Integer	data	s
isAbort8-UserCmd	command	p	command
isAbort9-UserCmd	command	p	command
isafterdeclassifyCCD4ASM-CreditCardCenterCmd	command	p	command
isAgent	data	p	Data
isAirline	Agent	p	Agent
isBookFlightOffer	data	p	Content
isBookFlightOffer-AirlineCmd	command	p	command
isBookFlightOfferstate6-AirlineCmd	command	p	command
isBookFlightOfferstate7-AirlineCmd	command	p	command
isBookSelected	data	p	Content
isBookSelected-TravelPlannerCmd	command	p	command
isBookSelectedstate2-TravelPlannerCmd	command	p	command
isBoolean	data	p	Data
isConfirm	data	p	Content
isConfirm-UserCmd-4	command	p	command
isConfirmBooking	data	p	Content
isConfirmRelease	data	p	Content
isConfirmRelease-UserCmd-3	command	p	command
isCreditCardCenter	Agent	p	Agent
isCreditCardDetails	data	p	Data
isDeclassifiedCCD	data	p	Content
isDeclassifiedCCD-TravelPlannerCmd	command	p	command
isDeclassify-count	name	p	name
isdeclassifyCCD4ASM-CreditCardCenterCmd	command	p	command
isFlightOffer	data	p	Data
isGetDeclassifiedCCD	data	p	Content
isGetDeclassifiedCCD-CreditCardCenterCmd	command	p	command
isGetFlightOffers	data	p	Content
isGetFlightOffers-AirlineCmd	command	p	command
isGetFlightOffers-TravelAgencyCmd	command	p	command
isGetFlightOffers-TravelPlannerCmd	command	p	command
isGetInputAgent	data	p	Content
isGetInputAirline	data	p	Content
isGetInputBoolean	data	p	Content
isGetInputCreditCardCenter	data	p	Content
isGetInputCreditCardDetails	data	p	Content
isGetInputData	data	p	Content
isGetInputFlightOffer	data	p	Content
isGetInputGPSPos	data	p	Content
isGetInputIFlowUtil	data	p	Content
isGetInputInteger	data	p	Content
isGetInputRequestData	data	p	Content
isGetInputRequestData-UserCmd-1	command	p	command
isGetInputString	data	p	Content
isGetInputTravelAgency	data	p	Content
isGetInputTravelPlanner	data	p	Content
isGetMultipleSelection	data	p	Content
isGetSingleSelection	data	p	Content
isGetSingleSelection-UserCmd-2	command	p	command
isGPSPos	data	p	Data
isInit-GetInputRequestData-TravelPlannerCmd	command	p	command
isInteger	data	p	Data
isListOfData	data	p	Data
isListOfFlightOffer	data	p	Data
isListOfGPSPos	data	p	Data
isLocVar	name	p	name
isMailbox	name	p	name
isMessage	data	p	Data
isNat	data	p	Data
isNull-IFlowUtil	datafuns	f	Data → Boolean
isOkConfirmBooking	data	p	Content
isOkConfirmBooking-TravelPlannerCmd	command	p	command
isOkPayCommission	data	p	Content
isOkPayCommission-AirlineCmd	command	p	command
isPair	data	p	Data
isPayCommission	data	p	Content
isPayCommission-TravelAgencyCmd	command	p	command
isReadSourceCount	name	p	name
isReadSourceInputs	name	p	name
isReleaseCCD	data	p	Content
isReleaseCCD-CreditCardCenterCmd	command	p	command
isRequestData	data	p	Data
isRetFlightOffers	data	p	Content
isRetFlightOffers-TravelAgencyCmd	command	p	command
isRetFlightOffers-TravelPlannerCmd	command	p	command
isRetFlightOffersstate1-TravelPlannerCmd	command	p	command
isShow	data	p	Content
isStart	data	p	Content
isState	name	p	name
isString	data	p	Data
isTravelAgency	Agent	p	Agent
isTravelPlanner	Agent	p	Agent
isTrue	datafuns	p	Data
isUser	Agent	p	Agent
isUser-Confirm	name	p	name
isUser-Confirm-count	name	p	name
isUser-ConfirmedRelease-count	name	p	name
isUser-ConfirmRelease	name	p	name
isUser-ConfirmRelease-count	name	p	name
isUser-ConfirmReleases	name	p	name
isUser-Confirms	name	p	name
isUser-GetInput	name	p	name
isUser-GetInput-count	name	p	name
isUser-GetInputs	name	p	name
isUser-GetMultipleSelection	name	p	name
isUser-GetMultipleSelection-count	name	p	name
isUser-GetMultipleSelections	name	p	name
isUser-GetSingleSelection	name	p	name
isUser-GetSingleSelection-count	name	p	name
isUser-GetSingleSelections	name	p	name
isValidCCD-Airline	localMethods	c	Data
j	int-basic1	v	int
j0	int-basic1	v	int
lastn	Agentlist	f	nat × Agentlist → Agentlist
ListOfData	data	s
ListOfData2ListOfFlightOffer	datafuns	f	ListOfData → ListOfFlightOffer
ListOfData2ListOfGPSPos	datafuns	f	ListOfData → ListOfGPSPos
ListOfFlightOffer	data	s
ListOfFlightOffer2ListOfData	datafuns	f	ListOfFlightOffer → ListOfData
ListOfGPSPos	data	s
ListOfGPSPos2ListOfData	datafuns	f	ListOfGPSPos → ListOfData
locVar	name	f	string → name
m	nat-basic2	v	nat
m0	Agent	v	nat
Mailbox	name	f	command → name
mailboxNotNull	state	p	(name × Agent → Data)
maxOneNotNull	state	p	(name × Agent → Data)
Message	data	s
mkAirline	Agent	f	nat → Agent
mkBookFlightOffer	data	f	Integer × CreditCardDetails → Content
mkBookSelected	data	f	FlightOffer → Content
mkBoolean	data	f	bool → Boolean
mkConfirm	data	c	Content
mkConfirmBooking	data	f	Integer → Content
mkConfirmRelease	data	f	Data × String → Content
mkCreditCardCenter	Agent	f	nat → Agent
mkCreditCardDetails	data	c	CreditCardDetails
mkDataPair	data	f	Data × Data → Data
mkDeclassifiedCCD	data	f	CreditCardDetails → Content
mkFlightOffer	data	f	Integer × String → FlightOffer
mkGetDeclassifiedCCD	data	c	Content
mkGetFlightOffers	data	f	RequestData → Content
mkGetInputAgent	data	c	Content
mkGetInputAirline	data	c	Content
mkGetInputBoolean	data	c	Content
mkGetInputCreditCardCenter	data	c	Content
mkGetInputCreditCardDetails	data	c	Content
mkGetInputData	data	c	Content
mkGetInputFlightOffer	data	c	Content
mkGetInputGPSPos	data	c	Content
mkGetInputIFlowUtil	data	c	Content
mkGetInputInteger	data	c	Content
mkGetInputRequestData	data	c	Content
mkGetInputString	data	c	Content
mkGetInputTravelAgency	data	c	Content
mkGetInputTravelPlanner	data	c	Content
mkGetMultipleSelection	data	f	ListOfData → Content
mkGetSingleSelection	data	f	ListOfData → Content
mkGPSPos	data	f	String × String → GPSPos
mkInteger	data	f	int → Integer
mklist	Agentlist	f	Agent × nat → Agentlist
mkMessage	data	f	Agentlist × Content → Message
mkNat	data	f	nat → Data
mkOkConfirmBooking	data	c	Content
mkOkPayCommission	data	c	Content
mkPayCommission	data	c	Content
mkReleaseCCD	data	f	String → Content
mkRequestData	data	f	String → RequestData
mkRetFlightOffers	data	f	ListOfFlightOffer → Content
mkShow	data	f	Data → Content
mkStart	data	c	Content
mkString	data	f	string → String
mkTravelAgency	Agent	f	nat → Agent
mkTravelPlanner	Agent	f	nat → Agent
mkUser	Agent	f	nat → Agent
msg	data	v	Message
msg0	data	v	Message
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nam	name	v	name
nam0	name	v	name
nam1	name	v	name
nam2	state	v	name
nam3	state	v	name
nam4	state	v	name
nam5	state	v	name
name	name	s
nat	nat-basic1	s
nonNull	datafuns	p	ListOfData
nonNull	datafuns	p	Data
null	data	c	Data
NUMOFAirline	exAgent	c	nat
NUMOFAPPSANDUSERS	exAgent	c	nat
NUMOFCreditCardCenter	exAgent	c	nat
NUMOFTravelAgency	exAgent	c	nat
NUMOFTravelPlanner	exAgent	c	nat
NUMOFUser	exAgent	c	nat
okaction	okaction	p	action
OkConfirmBooking-TravelPlannerCmd	command	c	command
OkConfirmBooking-TravelPlannerCmd#	ASM	pr	action : name × Agent → Data
OkPayCommission-AirlineCmd	command	c	command
OkPayCommission-AirlineCmd#	ASM	pr	action : name × Agent → Data
PayCommission-TravelAgencyCmd	command	c	command
PayCommission-TravelAgencyCmd#	ASM	pr	action : name × Agent → Data
perm	Agentlist	p	Agentlist × Agentlist
pos	string-less	f	char × string → nat
pos	Agentlist	f	Agent × Agentlist → nat
processBooking-Airline	localMethods	f	Integer × CreditCardDetails → Data
ReadSourceCount	name	f	string × string → name
ReadSourceInputs	name	f	string × string → name
ReleaseCCD-CreditCardCenterCmd	command	c	command
ReleaseCCD-CreditCardCenterCmd#	ASM	pr	action : name × Agent → Data
RequestData	data	s
restn	Agentlist	f	nat × Agentlist → Agentlist
RetFlightOffers-TravelAgencyCmd	command	c	command
RetFlightOffers-TravelAgencyCmd#	ASM	pr	action : name × Agent → Data
RetFlightOffers-TravelPlannerCmd	command	c	command
RetFlightOffers-TravelPlannerCmd#	ASM	pr	action : name × Agent → Data
RetFlightOffersstate1-TravelPlannerCmd	command	c	command
RetFlightOffersstate1-TravelPlannerCmd#	ASM	pr	action : name × Agent → Data
rev	Agentlist	f	Agentlist → Agentlist
rmdup	Agentlist	f	Agentlist → Agentlist
s	state	v	name × Agent → Data
s0	state	v	name × Agent → Data
s1	state	v	name × Agent → Data
s2	state	v	name × Agent → Data
s3	state	v	name × Agent → Data
set-airline	datafuns	f	FlightOffer × String → FlightOffer
set-id	datafuns	f	FlightOffer × Integer → FlightOffer
set-latitude	datafuns	f	GPSPos × String → GPSPos
set-longitude	datafuns	f	GPSPos × String → GPSPos
size	datafuns	f	Data → nat
sortedchars	string-less	c	string
state	name	f	string → name
stateNotNull	state	p	(name × Agent → Data)
STEP	ASM	pr	: name × Agent → Data × bool
str	string-data	v	string
str0	string-data	v	string
str1	string-data	v	string
str2	string-data	v	string
str3	string-data	v	string
string	string-data	s
String	data	s
stringvar	string-append	v	string
stringvar0	string-append	v	string
stringvar1	name	v	string
stringvar2	name	v	string
sublist	Agentlist	f	nat × nat × Agentlist → Agentlist
TravelPlanner-flightOffer	name	c	name
usedName	namefuns	p	name × Agent
usedName	namefuns	p	name
User-Confirm	name	f	string → name
User-Confirm-count	name	f	string → name
User-ConfirmedRelease-count	name	f	string → name
User-ConfirmRelease	name	f	string → name
User-ConfirmRelease-count	name	f	string → name
User-ConfirmReleases	name	f	string → name
User-Confirms	name	f	string → name
User-GetInput	name	f	string → name
User-GetInput-count	name	f	string → name
User-GetInputs	name	f	string → name
User-GetMultipleSelection	name	f	string → name
User-GetMultipleSelection-count	name	f	string → name
User-GetMultipleSelections	name	f	string → name
User-GetSingleSelection	name	f	string → name
User-GetSingleSelection-count	name	f	string → name
User-GetSingleSelections	name	f	string → name
wrapAgent2Data	data	f	Agent → Data
wrapBoolean2Data	data	f	Boolean → Data
wrapCreditCardDetails2Data	data	f	CreditCardDetails → Data
wrapFlightOffer2Data	data	f	FlightOffer → Data
wrapGPSPos2Data	data	f	GPSPos → Data
wrapInteger2Data	data	f	Integer → Data
wrapListOfData2Data	data	f	ListOfData → Data
wrapListOfFlightOffer2Data	data	f	ListOfFlightOffer → Data
wrapListOfGPSPos2Data	data	f	ListOfGPSPos → Data
wrapMessage2Data	data	f	Message → Data
wrapRequestData2Data	data	f	RequestData → Data
wrapString2Data	data	f	String → Data