| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (344 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (99 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (116 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (31 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (32 entries) |
Global Index
A
A [axiom, in ABP.ABP.BISIMULATION.Protocol]A [axiom, in ABP.ABP.TRACES.Protocol]
ABP [definition, in ABP.ABP.BISIMULATION.Protocol]
ABP [definition, in ABP.ABP.TRACES.Protocol]
ACAction [inductive, in ABP.ABP.BISIMULATION.Processes]
ACAction [inductive, in ABP.ABP.TRACES.Processes]
ACK [definition, in ABP.ABP.BISIMULATION.Protocol]
ACK [definition, in ABP.ABP.TRACES.Protocol]
ACKING [definition, in ABP.ABP.BISIMULATION.Protocol]
ACKING [definition, in ABP.ABP.TRACES.Protocol]
ACKING_SinvT [lemma, in ABP.ABP.TRACES.Lemmas]
ACKING_UinvT [lemma, in ABP.ABP.TRACES.Lemmas]
ACKING_UinvR [lemma, in ABP.ABP.TRACES.Lemmas]
ACKING_SinvT [lemma, in ABP.ABP.BISIMULATION.Lemmas]
ACKING_UinvT [lemma, in ABP.ABP.BISIMULATION.Lemmas]
ACKING_UinvR [lemma, in ABP.ABP.BISIMULATION.Lemmas]
ACK_UinvR [lemma, in ABP.ABP.TRACES.Lemmas]
ACK_UinvTC1 [lemma, in ABP.ABP.TRACES.Lemmas]
ACK_UinvTC2 [lemma, in ABP.ABP.TRACES.Lemmas]
ACK_UinvT1 [lemma, in ABP.ABP.TRACES.Lemmas]
ACK_SinvT [lemma, in ABP.ABP.TRACES.Lemmas]
ACK_ULoosed [lemma, in ABP.ABP.TRACES.Lemmas]
ACK_UinvR [lemma, in ABP.ABP.BISIMULATION.Lemmas]
ACK_UinvTC1 [lemma, in ABP.ABP.BISIMULATION.Lemmas]
ACK_UinvTC2 [lemma, in ABP.ABP.BISIMULATION.Lemmas]
ACK_UinvT1 [lemma, in ABP.ABP.BISIMULATION.Lemmas]
ACK_SinvT [lemma, in ABP.ABP.BISIMULATION.Lemmas]
ACK_ULoosed [lemma, in ABP.ABP.BISIMULATION.Lemmas]
ACLISTEN [constructor, in ABP.ABP.BISIMULATION.Processes]
ACLISTEN [constructor, in ABP.ABP.TRACES.Processes]
ACPAR [constructor, in ABP.ABP.BISIMULATION.Processes]
ACPAR [constructor, in ABP.ABP.TRACES.Processes]
ACProcess [inductive, in ABP.ABP.BISIMULATION.Processes]
ACProcess [inductive, in ABP.ABP.TRACES.Processes]
Act [definition, in ABP.ABP.BISIMULATION.Protocol]
Act [definition, in ABP.ABP.TRACES.Protocol]
ACTALK [constructor, in ABP.ABP.BISIMULATION.Processes]
ACTALK [constructor, in ABP.ABP.TRACES.Processes]
Action [abbreviation, in ABP.ABP.BISIMULATION.Protocol]
Action [inductive, in ABP.INTERPRETER.Processes]
Action [abbreviation, in ABP.ABP.TRACES.Protocol]
always [constructor, in ABP.ABP.TRACES.Processes]
Always [inductive, in ABP.ABP.TRACES.Processes]
Always_stable [lemma, in ABP.ABP.TRACES.Processes]
C
Channel [inductive, in ABP.ABP.BISIMULATION.Protocol]Channel [inductive, in ABP.ABP.TRACES.Protocol]
Clear [constructor, in ABP.ABP.BISIMULATION.Processes]
Clear [constructor, in ABP.INTERPRETER.Processes]
Clear [constructor, in ABP.ABP.TRACES.Processes]
compare [lemma, in ABP.ABP.BISIMULATION.Hypotheses]
compare [lemma, in ABP.ABP.TRACES.Hypotheses]
CONS [constructor, in ABP.INTERPRETER.Interpreter]
Correction [library]
correctness [lemma, in ABP.ABP.TRACES.Correction]
Correctness [library]
correctness_cycle [lemma, in ABP.ABP.TRACES.Correction]
D
del [constructor, in ABP.ABP.BISIMULATION.Protocol]del [constructor, in ABP.ABP.TRACES.Protocol]
Disc [constructor, in ABP.ABP.TRACES.Processes]
Discourse [inductive, in ABP.ABP.TRACES.Processes]
disc_mess [lemma, in ABP.ABP.TRACES.Lemmas]
disc_fun [lemma, in ABP.ABP.TRACES.Lemmas]
disc_mess [lemma, in ABP.ABP.BISIMULATION.Lemmas]
disc_fun [lemma, in ABP.ABP.BISIMULATION.Lemmas]
E
eps [constructor, in ABP.ABP.BISIMULATION.Processes]Equity [definition, in ABP.ABP.TRACES.Hypotheses]
Error [constructor, in ABP.INTERPRETER.Interpreter]
Evolve [constructor, in ABP.INTERPRETER.Interpreter]
Evt [inductive, in ABP.ABP.TRACES.Processes]
Evt [library]
Evt_from_Equity [lemma, in ABP.ABP.TRACES.Hypotheses]
Evt_stable [lemma, in ABP.ABP.TRACES.Processes]
Evt1 [lemma, in ABP.ABP.TRACES.Evt]
Evt2 [lemma, in ABP.ABP.TRACES.Evt]
Evt3 [lemma, in ABP.ABP.TRACES.Evt]
Evt45 [lemma, in ABP.ABP.TRACES.Evt]
Exceptions [inductive, in ABP.ABP.TRACES.Hypotheses]
exep2 [constructor, in ABP.ABP.TRACES.Hypotheses]
exep3 [constructor, in ABP.ABP.TRACES.Hypotheses]
exep4 [constructor, in ABP.ABP.TRACES.Hypotheses]
exep5 [constructor, in ABP.ABP.TRACES.Hypotheses]
exep6 [constructor, in ABP.ABP.TRACES.Hypotheses]
F
Fail [constructor, in ABP.INTERPRETER.Interpreter]Fairness [definition, in ABP.ABP.TRACES.Hypotheses]
G
goback [constructor, in ABP.ABP.TRACES.Processes]Guarded [inductive, in ABP.INTERPRETER.Processes]
H
Hypotheses [library]Hypotheses [library]
I
INJ [constructor, in ABP.INTERPRETER.Processes]inj_Tmess [lemma, in ABP.ABP.TRACES.Lemmas]
inj_Lfun [lemma, in ABP.ABP.TRACES.Lemmas]
inj_Tfun [lemma, in ABP.ABP.TRACES.Lemmas]
inj_Tmess [lemma, in ABP.ABP.BISIMULATION.Lemmas]
inj_Lfun [lemma, in ABP.ABP.BISIMULATION.Lemmas]
inj_Tfun [lemma, in ABP.ABP.BISIMULATION.Lemmas]
Interpreter [section, in ABP.INTERPRETER.Interpreter]
Interpreter [library]
Interpreter.A [variable, in ABP.INTERPRETER.Interpreter]
Interpreter.Chnl [variable, in ABP.INTERPRETER.Interpreter]
Interpreter.compare [variable, in ABP.INTERPRETER.Interpreter]
InTrace [definition, in ABP.ABP.TRACES.Hypotheses]
IsClear [definition, in ABP.ABP.TRACES.Hypotheses]
L
Left [constructor, in ABP.INTERPRETER.Interpreter]Lemmas [library]
Lemmas [library]
List [inductive, in ABP.INTERPRETER.Interpreter]
LISTEN [abbreviation, in ABP.ABP.BISIMULATION.Protocol]
LISTEN [constructor, in ABP.INTERPRETER.Processes]
listen [lemma, in ABP.INTERPRETER.Interpreter]
LISTEN [abbreviation, in ABP.ABP.TRACES.Protocol]
Lists [section, in ABP.INTERPRETER.Interpreter]
Lists.A [variable, in ABP.INTERPRETER.Interpreter]
lnk1 [constructor, in ABP.ABP.BISIMULATION.Protocol]
lnk1 [constructor, in ABP.ABP.TRACES.Protocol]
lnk2 [constructor, in ABP.ABP.BISIMULATION.Protocol]
lnk2 [constructor, in ABP.ABP.TRACES.Protocol]
N
NIL [constructor, in ABP.INTERPRETER.Interpreter]Noise [constructor, in ABP.ABP.BISIMULATION.Processes]
Noise [constructor, in ABP.INTERPRETER.Processes]
Noise [constructor, in ABP.ABP.TRACES.Processes]
notyet [constructor, in ABP.ABP.TRACES.Processes]
O
OneDel [definition, in ABP.ABP.TRACES.Hypotheses]OUT [definition, in ABP.ABP.BISIMULATION.Protocol]
OUT [definition, in ABP.ABP.TRACES.Protocol]
OUT_UinvT2 [lemma, in ABP.ABP.TRACES.Lemmas]
OUT_UinvT1 [lemma, in ABP.ABP.TRACES.Lemmas]
OUT_UinvR [lemma, in ABP.ABP.TRACES.Lemmas]
OUT_SinvT [lemma, in ABP.ABP.TRACES.Lemmas]
OUT_UinvT2 [lemma, in ABP.ABP.BISIMULATION.Lemmas]
OUT_UinvT1 [lemma, in ABP.ABP.BISIMULATION.Lemmas]
OUT_UinvR [lemma, in ABP.ABP.BISIMULATION.Lemmas]
OUT_SinvT [lemma, in ABP.ABP.BISIMULATION.Lemmas]
P
palways [constructor, in ABP.ABP.TRACES.Processes]PAlways [inductive, in ABP.ABP.TRACES.Processes]
PAR [constructor, in ABP.INTERPRETER.Processes]
Pointer [inductive, in ABP.INTERPRETER.Interpreter]
Precondition [definition, in ABP.ABP.TRACES.Hypotheses]
Process [definition, in ABP.ABP.BISIMULATION.Protocol]
Process [inductive, in ABP.INTERPRETER.Processes]
Process [definition, in ABP.ABP.TRACES.Protocol]
Processes [section, in ABP.ABP.BISIMULATION.Processes]
Processes [section, in ABP.INTERPRETER.Processes]
Processes [section, in ABP.ABP.TRACES.Processes]
Processes [library]
Processes [library]
Processes [library]
Processes.A [variable, in ABP.ABP.BISIMULATION.Processes]
Processes.A [variable, in ABP.INTERPRETER.Processes]
Processes.A [variable, in ABP.ABP.TRACES.Processes]
Processes.Chnl [variable, in ABP.ABP.BISIMULATION.Processes]
Processes.Chnl [variable, in ABP.INTERPRETER.Processes]
Processes.Chnl [variable, in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes.Parametric_Always.P [variable, in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes.Parametric_Always.Q [variable, in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes.Parametric_Always.B [variable, in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes.Parametric_Always [section, in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes.Basics.P [variable, in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes.Basics [section, in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes.Trans [variable, in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes [section, in ABP.ABP.TRACES.Processes]
Processes.Semantics [section, in ABP.INTERPRETER.Processes]
Processes.Semantics_of_ACProcesses.c [variable, in ABP.ABP.BISIMULATION.Processes]
Processes.Semantics_of_ACProcesses [section, in ABP.ABP.BISIMULATION.Processes]
Processes.Semantics_of_ACProcesses.c [variable, in ABP.ABP.TRACES.Processes]
Processes.Semantics_of_ACProcesses [section, in ABP.ABP.TRACES.Processes]
Processes.Semantics.c [variable, in ABP.INTERPRETER.Processes]
Processes.Weak_Bisimulations.Weak_Transitions.c [variable, in ABP.ABP.BISIMULATION.Processes]
Processes.Weak_Bisimulations.Weak_Transitions [section, in ABP.ABP.BISIMULATION.Processes]
Processes.Weak_Bisimulations.Hidden [variable, in ABP.ABP.BISIMULATION.Processes]
Processes.Weak_Bisimulations.Trans [variable, in ABP.ABP.BISIMULATION.Processes]
Processes.Weak_Bisimulations [section, in ABP.ABP.BISIMULATION.Processes]
Protocol [library]
Protocol [library]
R
Receive [constructor, in ABP.ABP.BISIMULATION.Processes]Receive [constructor, in ABP.INTERPRETER.Processes]
Receive [constructor, in ABP.ABP.TRACES.Processes]
Refuse [constructor, in ABP.INTERPRETER.Interpreter]
REPEAT [definition, in ABP.ABP.BISIMULATION.Protocol]
REPEAT [definition, in ABP.ABP.TRACES.Protocol]
REPEAT_UinvTC2 [lemma, in ABP.ABP.BISIMULATION.Lemmas]
REPEAT_UinvTC1 [lemma, in ABP.ABP.BISIMULATION.Lemmas]
REPEAT_SinvT [lemma, in ABP.ABP.BISIMULATION.Lemmas]
Result [inductive, in ABP.INTERPRETER.Interpreter]
Right [constructor, in ABP.INTERPRETER.Interpreter]
Rtalks [definition, in ABP.ABP.TRACES.Hypotheses]
S
SafeProcTrans [inductive, in ABP.ABP.BISIMULATION.Processes]SafeProcTrans [inductive, in ABP.INTERPRETER.Processes]
SafeProcTrans [inductive, in ABP.ABP.TRACES.Processes]
say [lemma, in ABP.INTERPRETER.Interpreter]
select_mess [definition, in ABP.ABP.TRACES.Lemmas]
select_fun [definition, in ABP.ABP.TRACES.Lemmas]
select_mess [definition, in ABP.ABP.BISIMULATION.Lemmas]
select_fun [definition, in ABP.ABP.BISIMULATION.Lemmas]
SEND [definition, in ABP.ABP.BISIMULATION.Protocol]
SEND [definition, in ABP.ABP.TRACES.Protocol]
SENDING [definition, in ABP.ABP.BISIMULATION.Protocol]
SENDING [definition, in ABP.ABP.TRACES.Protocol]
SENDING_UinvTC1 [lemma, in ABP.ABP.TRACES.Lemmas]
SENDING_UinvR [lemma, in ABP.ABP.TRACES.Lemmas]
SENDING_SinvR [lemma, in ABP.ABP.TRACES.Lemmas]
SENDING_SinvT [lemma, in ABP.ABP.TRACES.Lemmas]
SENDING_UinvT2 [lemma, in ABP.ABP.TRACES.Lemmas]
SENDING_ULoosed [lemma, in ABP.ABP.TRACES.Lemmas]
SENDING_UinvTC1 [lemma, in ABP.ABP.BISIMULATION.Lemmas]
SENDING_UinvR [lemma, in ABP.ABP.BISIMULATION.Lemmas]
SENDING_SinvR [lemma, in ABP.ABP.BISIMULATION.Lemmas]
SENDING_SinvT [lemma, in ABP.ABP.BISIMULATION.Lemmas]
SENDING_UinvT2 [lemma, in ABP.ABP.BISIMULATION.Lemmas]
SENDING_ULoosed [lemma, in ABP.ABP.BISIMULATION.Lemmas]
SEND_UinvR [lemma, in ABP.ABP.TRACES.Lemmas]
SEND_UinvT2 [lemma, in ABP.ABP.TRACES.Lemmas]
SEND_UinvTC1 [lemma, in ABP.ABP.TRACES.Lemmas]
SEND_ULoosed [lemma, in ABP.ABP.TRACES.Lemmas]
SEND_SinvT [lemma, in ABP.ABP.TRACES.Lemmas]
SEND_UinvR [lemma, in ABP.ABP.BISIMULATION.Lemmas]
SEND_UinvTC2 [lemma, in ABP.ABP.BISIMULATION.Lemmas]
SEND_UinvTC1 [lemma, in ABP.ABP.BISIMULATION.Lemmas]
SEND_ULoosed [lemma, in ABP.ABP.BISIMULATION.Lemmas]
SEND_SinvT [lemma, in ABP.ABP.BISIMULATION.Lemmas]
Signal [inductive, in ABP.ABP.BISIMULATION.Processes]
Signal [inductive, in ABP.INTERPRETER.Processes]
Signal [inductive, in ABP.ABP.TRACES.Processes]
Silent [definition, in ABP.ABP.BISIMULATION.Hypotheses]
simulator [lemma, in ABP.INTERPRETER.Interpreter]
start [constructor, in ABP.ABP.TRACES.Processes]
state1 [axiom, in ABP.ABP.BISIMULATION.Correctness]
State1 [lemma, in ABP.ABP.TRACES.Lemmas]
state2 [axiom, in ABP.ABP.BISIMULATION.Correctness]
State2 [lemma, in ABP.ABP.TRACES.Lemmas]
state3 [axiom, in ABP.ABP.BISIMULATION.Correctness]
State3 [lemma, in ABP.ABP.TRACES.Lemmas]
state4 [lemma, in ABP.ABP.BISIMULATION.Correctness]
State4 [lemma, in ABP.ABP.TRACES.Lemmas]
state5 [axiom, in ABP.ABP.BISIMULATION.Correctness]
State5 [lemma, in ABP.ABP.TRACES.Lemmas]
StillHappens [lemma, in ABP.ABP.TRACES.Processes]
stlisten1 [constructor, in ABP.ABP.BISIMULATION.Processes]
stlisten1 [constructor, in ABP.INTERPRETER.Processes]
stlisten1 [constructor, in ABP.ABP.TRACES.Processes]
stlisten2 [constructor, in ABP.ABP.BISIMULATION.Processes]
stlisten2 [constructor, in ABP.INTERPRETER.Processes]
stlisten2 [constructor, in ABP.ABP.TRACES.Processes]
Stop [constructor, in ABP.INTERPRETER.Interpreter]
stpar1 [constructor, in ABP.ABP.BISIMULATION.Processes]
stpar1 [constructor, in ABP.INTERPRETER.Processes]
stpar1 [constructor, in ABP.ABP.TRACES.Processes]
stpar2 [constructor, in ABP.ABP.BISIMULATION.Processes]
stpar2 [constructor, in ABP.INTERPRETER.Processes]
stpar2 [constructor, in ABP.ABP.TRACES.Processes]
stpar3 [constructor, in ABP.ABP.BISIMULATION.Processes]
stpar3 [constructor, in ABP.INTERPRETER.Processes]
stpar3 [constructor, in ABP.ABP.TRACES.Processes]
STrans [abbreviation, in ABP.ABP.BISIMULATION.Hypotheses]
STrans [abbreviation, in ABP.ABP.TRACES.Hypotheses]
sttalk1 [constructor, in ABP.ABP.BISIMULATION.Processes]
sttalk1 [constructor, in ABP.INTERPRETER.Processes]
sttalk1 [constructor, in ABP.ABP.TRACES.Processes]
sttalk2 [constructor, in ABP.ABP.BISIMULATION.Processes]
sttalk2 [constructor, in ABP.INTERPRETER.Processes]
sttalk2 [constructor, in ABP.ABP.TRACES.Processes]
sttalk3 [constructor, in ABP.ABP.BISIMULATION.Processes]
sttalk3 [constructor, in ABP.INTERPRETER.Processes]
sttalk3 [constructor, in ABP.ABP.TRACES.Processes]
Succ [constructor, in ABP.INTERPRETER.Interpreter]
T
TALK [abbreviation, in ABP.ABP.BISIMULATION.Protocol]TALK [constructor, in ABP.INTERPRETER.Processes]
TALK [abbreviation, in ABP.ABP.TRACES.Protocol]
Trace [inductive, in ABP.INTERPRETER.Interpreter]
Trans [definition, in ABP.ABP.BISIMULATION.Hypotheses]
Trans [definition, in ABP.ABP.TRACES.Hypotheses]
Transmit [constructor, in ABP.ABP.BISIMULATION.Processes]
Transmit [constructor, in ABP.INTERPRETER.Processes]
Transmit [constructor, in ABP.ABP.TRACES.Processes]
Tuple [constructor, in ABP.INTERPRETER.Interpreter]
U
unfold_OUT [lemma, in ABP.ABP.TRACES.Lemmas]unfold_ACK [lemma, in ABP.ABP.TRACES.Lemmas]
unfold_ACKING [lemma, in ABP.ABP.TRACES.Lemmas]
unfold_SENDING [lemma, in ABP.ABP.TRACES.Lemmas]
unfold_SEND [lemma, in ABP.ABP.TRACES.Lemmas]
unfold_REPEAT [lemma, in ABP.ABP.BISIMULATION.Lemmas]
unfold_OUT [lemma, in ABP.ABP.BISIMULATION.Lemmas]
unfold_ACK [lemma, in ABP.ABP.BISIMULATION.Lemmas]
unfold_ACKING [lemma, in ABP.ABP.BISIMULATION.Lemmas]
unfold_SENDING [lemma, in ABP.ABP.BISIMULATION.Lemmas]
unfold_SEND [lemma, in ABP.ABP.BISIMULATION.Lemmas]
unfold_process [lemma, in ABP.ABP.BISIMULATION.Processes]
unfold_process [lemma, in ABP.ABP.TRACES.Processes]
Unique [library]
Unique1 [lemma, in ABP.ABP.TRACES.Unique]
Unique2 [lemma, in ABP.ABP.TRACES.Unique]
Unique3 [lemma, in ABP.ABP.TRACES.Unique]
Unique45 [lemma, in ABP.ABP.TRACES.Unique]
UnrelProcTrans [inductive, in ABP.ABP.BISIMULATION.Processes]
UnrelProcTrans [inductive, in ABP.INTERPRETER.Processes]
UnrelProcTrans [inductive, in ABP.ABP.TRACES.Processes]
utlisten1 [constructor, in ABP.ABP.BISIMULATION.Processes]
utlisten1 [constructor, in ABP.INTERPRETER.Processes]
utlisten1 [constructor, in ABP.ABP.TRACES.Processes]
utlisten2 [constructor, in ABP.ABP.BISIMULATION.Processes]
utlisten2 [constructor, in ABP.INTERPRETER.Processes]
utlisten2 [constructor, in ABP.ABP.TRACES.Processes]
utpar1 [constructor, in ABP.ABP.BISIMULATION.Processes]
utpar1 [constructor, in ABP.INTERPRETER.Processes]
utpar1 [constructor, in ABP.ABP.TRACES.Processes]
utpar2 [constructor, in ABP.ABP.BISIMULATION.Processes]
utpar2 [constructor, in ABP.INTERPRETER.Processes]
utpar2 [constructor, in ABP.ABP.TRACES.Processes]
utpar3 [constructor, in ABP.ABP.BISIMULATION.Processes]
utpar3 [constructor, in ABP.INTERPRETER.Processes]
utpar3 [constructor, in ABP.ABP.TRACES.Processes]
utpar4 [constructor, in ABP.ABP.BISIMULATION.Processes]
utpar4 [constructor, in ABP.INTERPRETER.Processes]
utpar4 [constructor, in ABP.ABP.TRACES.Processes]
utpar5 [constructor, in ABP.ABP.BISIMULATION.Processes]
utpar5 [constructor, in ABP.INTERPRETER.Processes]
utpar5 [constructor, in ABP.ABP.TRACES.Processes]
UTrans [abbreviation, in ABP.ABP.BISIMULATION.Hypotheses]
UTrans [abbreviation, in ABP.ABP.TRACES.Hypotheses]
uttalk1 [constructor, in ABP.ABP.BISIMULATION.Processes]
uttalk1 [constructor, in ABP.INTERPRETER.Processes]
uttalk1 [constructor, in ABP.ABP.TRACES.Processes]
uttalk2 [constructor, in ABP.ABP.BISIMULATION.Processes]
uttalk2 [constructor, in ABP.INTERPRETER.Processes]
uttalk2 [constructor, in ABP.ABP.TRACES.Processes]
uttalk3 [constructor, in ABP.ABP.BISIMULATION.Processes]
uttalk3 [constructor, in ABP.INTERPRETER.Processes]
uttalk3 [constructor, in ABP.ABP.TRACES.Processes]
uttalk4 [constructor, in ABP.ABP.BISIMULATION.Processes]
uttalk4 [constructor, in ABP.INTERPRETER.Processes]
uttalk4 [constructor, in ABP.ABP.TRACES.Processes]
W
weak_eq [inductive, in ABP.ABP.BISIMULATION.Processes]weak_derivative [inductive, in ABP.ABP.BISIMULATION.Processes]
Wittness [inductive, in ABP.ABP.TRACES.Processes]
Wright [inductive, in ABP.INTERPRETER.Interpreter]
wright_l [constructor, in ABP.INTERPRETER.Interpreter]
wright_r [constructor, in ABP.INTERPRETER.Interpreter]
wright_f [constructor, in ABP.INTERPRETER.Interpreter]
wright_s [constructor, in ABP.INTERPRETER.Interpreter]
w_eq [constructor, in ABP.ABP.BISIMULATION.Processes]
w_tau_right [constructor, in ABP.ABP.BISIMULATION.Processes]
w_tau_left [constructor, in ABP.ABP.BISIMULATION.Processes]
w_single [constructor, in ABP.ABP.BISIMULATION.Processes]
other
_ || _ [notation, in ABP.ABP.BISIMULATION.Protocol]_ || _ [notation, in ABP.ABP.TRACES.Protocol]
Notation Index
other
_ || _ [in ABP.ABP.BISIMULATION.Protocol]_ || _ [in ABP.ABP.TRACES.Protocol]
Variable Index
I
Interpreter.A [in ABP.INTERPRETER.Interpreter]Interpreter.Chnl [in ABP.INTERPRETER.Interpreter]
Interpreter.compare [in ABP.INTERPRETER.Interpreter]
L
Lists.A [in ABP.INTERPRETER.Interpreter]P
Processes.A [in ABP.ABP.BISIMULATION.Processes]Processes.A [in ABP.INTERPRETER.Processes]
Processes.A [in ABP.ABP.TRACES.Processes]
Processes.Chnl [in ABP.ABP.BISIMULATION.Processes]
Processes.Chnl [in ABP.INTERPRETER.Processes]
Processes.Chnl [in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes.Parametric_Always.P [in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes.Parametric_Always.Q [in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes.Parametric_Always.B [in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes.Basics.P [in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes.Trans [in ABP.ABP.TRACES.Processes]
Processes.Semantics_of_ACProcesses.c [in ABP.ABP.BISIMULATION.Processes]
Processes.Semantics_of_ACProcesses.c [in ABP.ABP.TRACES.Processes]
Processes.Semantics.c [in ABP.INTERPRETER.Processes]
Processes.Weak_Bisimulations.Weak_Transitions.c [in ABP.ABP.BISIMULATION.Processes]
Processes.Weak_Bisimulations.Hidden [in ABP.ABP.BISIMULATION.Processes]
Processes.Weak_Bisimulations.Trans [in ABP.ABP.BISIMULATION.Processes]
Library Index
C
CorrectionCorrectness
E
EvtH
HypothesesHypotheses
I
InterpreterL
LemmasLemmas
P
ProcessesProcesses
Processes
Protocol
Protocol
U
UniqueLemma Index
A
ACKING_SinvT [in ABP.ABP.TRACES.Lemmas]ACKING_UinvT [in ABP.ABP.TRACES.Lemmas]
ACKING_UinvR [in ABP.ABP.TRACES.Lemmas]
ACKING_SinvT [in ABP.ABP.BISIMULATION.Lemmas]
ACKING_UinvT [in ABP.ABP.BISIMULATION.Lemmas]
ACKING_UinvR [in ABP.ABP.BISIMULATION.Lemmas]
ACK_UinvR [in ABP.ABP.TRACES.Lemmas]
ACK_UinvTC1 [in ABP.ABP.TRACES.Lemmas]
ACK_UinvTC2 [in ABP.ABP.TRACES.Lemmas]
ACK_UinvT1 [in ABP.ABP.TRACES.Lemmas]
ACK_SinvT [in ABP.ABP.TRACES.Lemmas]
ACK_ULoosed [in ABP.ABP.TRACES.Lemmas]
ACK_UinvR [in ABP.ABP.BISIMULATION.Lemmas]
ACK_UinvTC1 [in ABP.ABP.BISIMULATION.Lemmas]
ACK_UinvTC2 [in ABP.ABP.BISIMULATION.Lemmas]
ACK_UinvT1 [in ABP.ABP.BISIMULATION.Lemmas]
ACK_SinvT [in ABP.ABP.BISIMULATION.Lemmas]
ACK_ULoosed [in ABP.ABP.BISIMULATION.Lemmas]
Always_stable [in ABP.ABP.TRACES.Processes]
C
compare [in ABP.ABP.BISIMULATION.Hypotheses]compare [in ABP.ABP.TRACES.Hypotheses]
correctness [in ABP.ABP.TRACES.Correction]
correctness_cycle [in ABP.ABP.TRACES.Correction]
D
disc_mess [in ABP.ABP.TRACES.Lemmas]disc_fun [in ABP.ABP.TRACES.Lemmas]
disc_mess [in ABP.ABP.BISIMULATION.Lemmas]
disc_fun [in ABP.ABP.BISIMULATION.Lemmas]
E
Evt_from_Equity [in ABP.ABP.TRACES.Hypotheses]Evt_stable [in ABP.ABP.TRACES.Processes]
Evt1 [in ABP.ABP.TRACES.Evt]
Evt2 [in ABP.ABP.TRACES.Evt]
Evt3 [in ABP.ABP.TRACES.Evt]
Evt45 [in ABP.ABP.TRACES.Evt]
I
inj_Tmess [in ABP.ABP.TRACES.Lemmas]inj_Lfun [in ABP.ABP.TRACES.Lemmas]
inj_Tfun [in ABP.ABP.TRACES.Lemmas]
inj_Tmess [in ABP.ABP.BISIMULATION.Lemmas]
inj_Lfun [in ABP.ABP.BISIMULATION.Lemmas]
inj_Tfun [in ABP.ABP.BISIMULATION.Lemmas]
L
listen [in ABP.INTERPRETER.Interpreter]O
OUT_UinvT2 [in ABP.ABP.TRACES.Lemmas]OUT_UinvT1 [in ABP.ABP.TRACES.Lemmas]
OUT_UinvR [in ABP.ABP.TRACES.Lemmas]
OUT_SinvT [in ABP.ABP.TRACES.Lemmas]
OUT_UinvT2 [in ABP.ABP.BISIMULATION.Lemmas]
OUT_UinvT1 [in ABP.ABP.BISIMULATION.Lemmas]
OUT_UinvR [in ABP.ABP.BISIMULATION.Lemmas]
OUT_SinvT [in ABP.ABP.BISIMULATION.Lemmas]
R
REPEAT_UinvTC2 [in ABP.ABP.BISIMULATION.Lemmas]REPEAT_UinvTC1 [in ABP.ABP.BISIMULATION.Lemmas]
REPEAT_SinvT [in ABP.ABP.BISIMULATION.Lemmas]
S
say [in ABP.INTERPRETER.Interpreter]SENDING_UinvTC1 [in ABP.ABP.TRACES.Lemmas]
SENDING_UinvR [in ABP.ABP.TRACES.Lemmas]
SENDING_SinvR [in ABP.ABP.TRACES.Lemmas]
SENDING_SinvT [in ABP.ABP.TRACES.Lemmas]
SENDING_UinvT2 [in ABP.ABP.TRACES.Lemmas]
SENDING_ULoosed [in ABP.ABP.TRACES.Lemmas]
SENDING_UinvTC1 [in ABP.ABP.BISIMULATION.Lemmas]
SENDING_UinvR [in ABP.ABP.BISIMULATION.Lemmas]
SENDING_SinvR [in ABP.ABP.BISIMULATION.Lemmas]
SENDING_SinvT [in ABP.ABP.BISIMULATION.Lemmas]
SENDING_UinvT2 [in ABP.ABP.BISIMULATION.Lemmas]
SENDING_ULoosed [in ABP.ABP.BISIMULATION.Lemmas]
SEND_UinvR [in ABP.ABP.TRACES.Lemmas]
SEND_UinvT2 [in ABP.ABP.TRACES.Lemmas]
SEND_UinvTC1 [in ABP.ABP.TRACES.Lemmas]
SEND_ULoosed [in ABP.ABP.TRACES.Lemmas]
SEND_SinvT [in ABP.ABP.TRACES.Lemmas]
SEND_UinvR [in ABP.ABP.BISIMULATION.Lemmas]
SEND_UinvTC2 [in ABP.ABP.BISIMULATION.Lemmas]
SEND_UinvTC1 [in ABP.ABP.BISIMULATION.Lemmas]
SEND_ULoosed [in ABP.ABP.BISIMULATION.Lemmas]
SEND_SinvT [in ABP.ABP.BISIMULATION.Lemmas]
simulator [in ABP.INTERPRETER.Interpreter]
State1 [in ABP.ABP.TRACES.Lemmas]
State2 [in ABP.ABP.TRACES.Lemmas]
State3 [in ABP.ABP.TRACES.Lemmas]
state4 [in ABP.ABP.BISIMULATION.Correctness]
State4 [in ABP.ABP.TRACES.Lemmas]
State5 [in ABP.ABP.TRACES.Lemmas]
StillHappens [in ABP.ABP.TRACES.Processes]
U
unfold_OUT [in ABP.ABP.TRACES.Lemmas]unfold_ACK [in ABP.ABP.TRACES.Lemmas]
unfold_ACKING [in ABP.ABP.TRACES.Lemmas]
unfold_SENDING [in ABP.ABP.TRACES.Lemmas]
unfold_SEND [in ABP.ABP.TRACES.Lemmas]
unfold_REPEAT [in ABP.ABP.BISIMULATION.Lemmas]
unfold_OUT [in ABP.ABP.BISIMULATION.Lemmas]
unfold_ACK [in ABP.ABP.BISIMULATION.Lemmas]
unfold_ACKING [in ABP.ABP.BISIMULATION.Lemmas]
unfold_SENDING [in ABP.ABP.BISIMULATION.Lemmas]
unfold_SEND [in ABP.ABP.BISIMULATION.Lemmas]
unfold_process [in ABP.ABP.BISIMULATION.Processes]
unfold_process [in ABP.ABP.TRACES.Processes]
Unique1 [in ABP.ABP.TRACES.Unique]
Unique2 [in ABP.ABP.TRACES.Unique]
Unique3 [in ABP.ABP.TRACES.Unique]
Unique45 [in ABP.ABP.TRACES.Unique]
Axiom Index
A
A [in ABP.ABP.BISIMULATION.Protocol]A [in ABP.ABP.TRACES.Protocol]
S
state1 [in ABP.ABP.BISIMULATION.Correctness]state2 [in ABP.ABP.BISIMULATION.Correctness]
state3 [in ABP.ABP.BISIMULATION.Correctness]
state5 [in ABP.ABP.BISIMULATION.Correctness]
Constructor Index
A
ACLISTEN [in ABP.ABP.BISIMULATION.Processes]ACLISTEN [in ABP.ABP.TRACES.Processes]
ACPAR [in ABP.ABP.BISIMULATION.Processes]
ACPAR [in ABP.ABP.TRACES.Processes]
ACTALK [in ABP.ABP.BISIMULATION.Processes]
ACTALK [in ABP.ABP.TRACES.Processes]
always [in ABP.ABP.TRACES.Processes]
C
Clear [in ABP.ABP.BISIMULATION.Processes]Clear [in ABP.INTERPRETER.Processes]
Clear [in ABP.ABP.TRACES.Processes]
CONS [in ABP.INTERPRETER.Interpreter]
D
del [in ABP.ABP.BISIMULATION.Protocol]del [in ABP.ABP.TRACES.Protocol]
Disc [in ABP.ABP.TRACES.Processes]
E
eps [in ABP.ABP.BISIMULATION.Processes]Error [in ABP.INTERPRETER.Interpreter]
Evolve [in ABP.INTERPRETER.Interpreter]
exep2 [in ABP.ABP.TRACES.Hypotheses]
exep3 [in ABP.ABP.TRACES.Hypotheses]
exep4 [in ABP.ABP.TRACES.Hypotheses]
exep5 [in ABP.ABP.TRACES.Hypotheses]
exep6 [in ABP.ABP.TRACES.Hypotheses]
F
Fail [in ABP.INTERPRETER.Interpreter]G
goback [in ABP.ABP.TRACES.Processes]I
INJ [in ABP.INTERPRETER.Processes]L
Left [in ABP.INTERPRETER.Interpreter]LISTEN [in ABP.INTERPRETER.Processes]
lnk1 [in ABP.ABP.BISIMULATION.Protocol]
lnk1 [in ABP.ABP.TRACES.Protocol]
lnk2 [in ABP.ABP.BISIMULATION.Protocol]
lnk2 [in ABP.ABP.TRACES.Protocol]
N
NIL [in ABP.INTERPRETER.Interpreter]Noise [in ABP.ABP.BISIMULATION.Processes]
Noise [in ABP.INTERPRETER.Processes]
Noise [in ABP.ABP.TRACES.Processes]
notyet [in ABP.ABP.TRACES.Processes]
P
palways [in ABP.ABP.TRACES.Processes]PAR [in ABP.INTERPRETER.Processes]
R
Receive [in ABP.ABP.BISIMULATION.Processes]Receive [in ABP.INTERPRETER.Processes]
Receive [in ABP.ABP.TRACES.Processes]
Refuse [in ABP.INTERPRETER.Interpreter]
Right [in ABP.INTERPRETER.Interpreter]
S
start [in ABP.ABP.TRACES.Processes]stlisten1 [in ABP.ABP.BISIMULATION.Processes]
stlisten1 [in ABP.INTERPRETER.Processes]
stlisten1 [in ABP.ABP.TRACES.Processes]
stlisten2 [in ABP.ABP.BISIMULATION.Processes]
stlisten2 [in ABP.INTERPRETER.Processes]
stlisten2 [in ABP.ABP.TRACES.Processes]
Stop [in ABP.INTERPRETER.Interpreter]
stpar1 [in ABP.ABP.BISIMULATION.Processes]
stpar1 [in ABP.INTERPRETER.Processes]
stpar1 [in ABP.ABP.TRACES.Processes]
stpar2 [in ABP.ABP.BISIMULATION.Processes]
stpar2 [in ABP.INTERPRETER.Processes]
stpar2 [in ABP.ABP.TRACES.Processes]
stpar3 [in ABP.ABP.BISIMULATION.Processes]
stpar3 [in ABP.INTERPRETER.Processes]
stpar3 [in ABP.ABP.TRACES.Processes]
sttalk1 [in ABP.ABP.BISIMULATION.Processes]
sttalk1 [in ABP.INTERPRETER.Processes]
sttalk1 [in ABP.ABP.TRACES.Processes]
sttalk2 [in ABP.ABP.BISIMULATION.Processes]
sttalk2 [in ABP.INTERPRETER.Processes]
sttalk2 [in ABP.ABP.TRACES.Processes]
sttalk3 [in ABP.ABP.BISIMULATION.Processes]
sttalk3 [in ABP.INTERPRETER.Processes]
sttalk3 [in ABP.ABP.TRACES.Processes]
Succ [in ABP.INTERPRETER.Interpreter]
T
TALK [in ABP.INTERPRETER.Processes]Transmit [in ABP.ABP.BISIMULATION.Processes]
Transmit [in ABP.INTERPRETER.Processes]
Transmit [in ABP.ABP.TRACES.Processes]
Tuple [in ABP.INTERPRETER.Interpreter]
U
utlisten1 [in ABP.ABP.BISIMULATION.Processes]utlisten1 [in ABP.INTERPRETER.Processes]
utlisten1 [in ABP.ABP.TRACES.Processes]
utlisten2 [in ABP.ABP.BISIMULATION.Processes]
utlisten2 [in ABP.INTERPRETER.Processes]
utlisten2 [in ABP.ABP.TRACES.Processes]
utpar1 [in ABP.ABP.BISIMULATION.Processes]
utpar1 [in ABP.INTERPRETER.Processes]
utpar1 [in ABP.ABP.TRACES.Processes]
utpar2 [in ABP.ABP.BISIMULATION.Processes]
utpar2 [in ABP.INTERPRETER.Processes]
utpar2 [in ABP.ABP.TRACES.Processes]
utpar3 [in ABP.ABP.BISIMULATION.Processes]
utpar3 [in ABP.INTERPRETER.Processes]
utpar3 [in ABP.ABP.TRACES.Processes]
utpar4 [in ABP.ABP.BISIMULATION.Processes]
utpar4 [in ABP.INTERPRETER.Processes]
utpar4 [in ABP.ABP.TRACES.Processes]
utpar5 [in ABP.ABP.BISIMULATION.Processes]
utpar5 [in ABP.INTERPRETER.Processes]
utpar5 [in ABP.ABP.TRACES.Processes]
uttalk1 [in ABP.ABP.BISIMULATION.Processes]
uttalk1 [in ABP.INTERPRETER.Processes]
uttalk1 [in ABP.ABP.TRACES.Processes]
uttalk2 [in ABP.ABP.BISIMULATION.Processes]
uttalk2 [in ABP.INTERPRETER.Processes]
uttalk2 [in ABP.ABP.TRACES.Processes]
uttalk3 [in ABP.ABP.BISIMULATION.Processes]
uttalk3 [in ABP.INTERPRETER.Processes]
uttalk3 [in ABP.ABP.TRACES.Processes]
uttalk4 [in ABP.ABP.BISIMULATION.Processes]
uttalk4 [in ABP.INTERPRETER.Processes]
uttalk4 [in ABP.ABP.TRACES.Processes]
W
wright_l [in ABP.INTERPRETER.Interpreter]wright_r [in ABP.INTERPRETER.Interpreter]
wright_f [in ABP.INTERPRETER.Interpreter]
wright_s [in ABP.INTERPRETER.Interpreter]
w_eq [in ABP.ABP.BISIMULATION.Processes]
w_tau_right [in ABP.ABP.BISIMULATION.Processes]
w_tau_left [in ABP.ABP.BISIMULATION.Processes]
w_single [in ABP.ABP.BISIMULATION.Processes]
Inductive Index
A
ACAction [in ABP.ABP.BISIMULATION.Processes]ACAction [in ABP.ABP.TRACES.Processes]
ACProcess [in ABP.ABP.BISIMULATION.Processes]
ACProcess [in ABP.ABP.TRACES.Processes]
Action [in ABP.INTERPRETER.Processes]
Always [in ABP.ABP.TRACES.Processes]
C
Channel [in ABP.ABP.BISIMULATION.Protocol]Channel [in ABP.ABP.TRACES.Protocol]
D
Discourse [in ABP.ABP.TRACES.Processes]E
Evt [in ABP.ABP.TRACES.Processes]Exceptions [in ABP.ABP.TRACES.Hypotheses]
G
Guarded [in ABP.INTERPRETER.Processes]L
List [in ABP.INTERPRETER.Interpreter]P
PAlways [in ABP.ABP.TRACES.Processes]Pointer [in ABP.INTERPRETER.Interpreter]
Process [in ABP.INTERPRETER.Processes]
R
Result [in ABP.INTERPRETER.Interpreter]S
SafeProcTrans [in ABP.ABP.BISIMULATION.Processes]SafeProcTrans [in ABP.INTERPRETER.Processes]
SafeProcTrans [in ABP.ABP.TRACES.Processes]
Signal [in ABP.ABP.BISIMULATION.Processes]
Signal [in ABP.INTERPRETER.Processes]
Signal [in ABP.ABP.TRACES.Processes]
T
Trace [in ABP.INTERPRETER.Interpreter]U
UnrelProcTrans [in ABP.ABP.BISIMULATION.Processes]UnrelProcTrans [in ABP.INTERPRETER.Processes]
UnrelProcTrans [in ABP.ABP.TRACES.Processes]
W
weak_eq [in ABP.ABP.BISIMULATION.Processes]weak_derivative [in ABP.ABP.BISIMULATION.Processes]
Wittness [in ABP.ABP.TRACES.Processes]
Wright [in ABP.INTERPRETER.Interpreter]
Section Index
I
Interpreter [in ABP.INTERPRETER.Interpreter]L
Lists [in ABP.INTERPRETER.Interpreter]P
Processes [in ABP.ABP.BISIMULATION.Processes]Processes [in ABP.INTERPRETER.Processes]
Processes [in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes.Parametric_Always [in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes.Basics [in ABP.ABP.TRACES.Processes]
Processes.Properties_of_Processes [in ABP.ABP.TRACES.Processes]
Processes.Semantics [in ABP.INTERPRETER.Processes]
Processes.Semantics_of_ACProcesses [in ABP.ABP.BISIMULATION.Processes]
Processes.Semantics_of_ACProcesses [in ABP.ABP.TRACES.Processes]
Processes.Weak_Bisimulations.Weak_Transitions [in ABP.ABP.BISIMULATION.Processes]
Processes.Weak_Bisimulations [in ABP.ABP.BISIMULATION.Processes]
Abbreviation Index
A
Action [in ABP.ABP.BISIMULATION.Protocol]Action [in ABP.ABP.TRACES.Protocol]
L
LISTEN [in ABP.ABP.BISIMULATION.Protocol]LISTEN [in ABP.ABP.TRACES.Protocol]
S
STrans [in ABP.ABP.BISIMULATION.Hypotheses]STrans [in ABP.ABP.TRACES.Hypotheses]
T
TALK [in ABP.ABP.BISIMULATION.Protocol]TALK [in ABP.ABP.TRACES.Protocol]
U
UTrans [in ABP.ABP.BISIMULATION.Hypotheses]UTrans [in ABP.ABP.TRACES.Hypotheses]
Definition Index
A
ABP [in ABP.ABP.BISIMULATION.Protocol]ABP [in ABP.ABP.TRACES.Protocol]
ACK [in ABP.ABP.BISIMULATION.Protocol]
ACK [in ABP.ABP.TRACES.Protocol]
ACKING [in ABP.ABP.BISIMULATION.Protocol]
ACKING [in ABP.ABP.TRACES.Protocol]
Act [in ABP.ABP.BISIMULATION.Protocol]
Act [in ABP.ABP.TRACES.Protocol]
E
Equity [in ABP.ABP.TRACES.Hypotheses]F
Fairness [in ABP.ABP.TRACES.Hypotheses]I
InTrace [in ABP.ABP.TRACES.Hypotheses]IsClear [in ABP.ABP.TRACES.Hypotheses]
O
OneDel [in ABP.ABP.TRACES.Hypotheses]OUT [in ABP.ABP.BISIMULATION.Protocol]
OUT [in ABP.ABP.TRACES.Protocol]
P
Precondition [in ABP.ABP.TRACES.Hypotheses]Process [in ABP.ABP.BISIMULATION.Protocol]
Process [in ABP.ABP.TRACES.Protocol]
R
REPEAT [in ABP.ABP.BISIMULATION.Protocol]REPEAT [in ABP.ABP.TRACES.Protocol]
Rtalks [in ABP.ABP.TRACES.Hypotheses]
S
select_mess [in ABP.ABP.TRACES.Lemmas]select_fun [in ABP.ABP.TRACES.Lemmas]
select_mess [in ABP.ABP.BISIMULATION.Lemmas]
select_fun [in ABP.ABP.BISIMULATION.Lemmas]
SEND [in ABP.ABP.BISIMULATION.Protocol]
SEND [in ABP.ABP.TRACES.Protocol]
SENDING [in ABP.ABP.BISIMULATION.Protocol]
SENDING [in ABP.ABP.TRACES.Protocol]
Silent [in ABP.ABP.BISIMULATION.Hypotheses]
T
Trans [in ABP.ABP.BISIMULATION.Hypotheses]Trans [in ABP.ABP.TRACES.Hypotheses]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (344 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (99 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (116 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (31 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (32 entries) |