Global Index

other

(293 entries)

Notation Index

other

(3 entries)

Variable Index

other

(3 entries)

Library Index

other

(3 entries)

Lemma Index

other

(106 entries)

Constructor Index

other

(60 entries)

Axiom Index

other

(11 entries)

Inductive Index

other

(38 entries)

Projection Index

other

(18 entries)

Section Index

other

(2 entries)

Definition Index

other

(45 entries)

Record Index

other

(4 entries)

Global Index

A

accD [constructor, in tsimu]
accE [constructor, in tsimu]
accept [inductive, in tsimu]
acceptFrom [inductive, in tsimu]
accPrf [constructor, in tsimu]
AD [definition, in tsimu]
additivity [projection, in tsimu]
ADF_EDT_Atl1Tau [lemma, in tsimu]
AD_ED_cases [lemma, in tsimu]
AG [inductive, in tsimu]
AGprf [constructor, in tsimu]
ALLE [definition, in tsimu]
all_and [lemma, in tsimu]
ALL1 [definition, in tsimu]
ALL2 [definition, in tsimu]
AND [inductive, in tsimu]
ANDprf [constructor, in tsimu]
AND3 [inductive, in tsimu]
AND3prf [constructor, in tsimu]
AND4 [inductive, in tsimu]
AND4prf [constructor, in tsimu]
atleast [definition, in tsimu]
atmost [definition, in tsimu]
atmost1tau [definition, in tsimu]
ATM1_Tau [lemma, in tsimu]
ATM1_skp0 [lemma, in tsimu]
ATM1_skp [lemma, in tsimu]
AX [definition, in tsimu]
AXE1 [definition, in tsimu]
AXT1 [definition, in tsimu]
AXT2 [definition, in tsimu]
AX_EX [lemma, in tsimu]

C

D

Ddly [constructor, in tsimu]
deadlock [definition, in tsimu]
Delay [constructor, in tsimu]
DelaySkipTauWait [lemma, in tsimu]
DelaySkipTau2Wait [lemma, in tsimu]
Delay_preEvt [lemma, in tsimu]
Delay_Delta1 [lemma, in tsimu]
Delay_StateO [lemma, in tsimu]
Delay_StateD [lemma, in tsimu]
Delay_State2 [lemma, in tsimu]
Delay_State1 [lemma, in tsimu]
Delay_proj2 [lemma, in tsimu]
DeltaDelaySkipTau2Wait [lemma, in tsimu]
DeltaDelay_skipTau2Wait [lemma, in tsimu]
DeltaDelay_NZ [lemma, in tsimu]
DeltaEvtZ [lemma, in tsimu]
DeltaTau1Z [lemma, in tsimu]
DeltaTau2Z [lemma, in tsimu]
Delta_StateO [lemma, in tsimu]
Delta_proj2 [lemma, in tsimu]
Delta_proj1 [lemma, in tsimu]
Delta2NZ_EDT [lemma, in tsimu]
determinism [projection, in tsimu]
Devt0 [constructor, in tsimu]
Devt0_exDelay [lemma, in tsimu]
DIV [inductive, in tsimu]
diverge [definition, in tsimu]
divergeFrom [definition, in tsimu]
DIVprf [constructor, in tsimu]
DLab [constructor, in tsimu]
DLabDly [definition, in tsimu]
DLabDlyNZ [lemma, in tsimu]
DLabDly_additivity [lemma, in tsimu]
DLabDly0 [lemma, in tsimu]
DNext [inductive, in tsimu]
DNextTau2_preEvt [lemma, in tsimu]
DNext_tau2_evt [lemma, in tsimu]
DNext_tau2_evt0 [lemma, in tsimu]
DNprf [constructor, in tsimu]
DState [inductive, in tsimu]
DV_EF_Tau2_evt0_EDT [lemma, in tsimu]

E

ED [inductive, in tsimu]
EDT_ADF [lemma, in tsimu]
EDT_prj1 [lemma, in tsimu]
EDT_inf_t [lemma, in tsimu]
ED_intro [constructor, in tsimu]
EE [constructor, in tsimu]
Eevt [constructor, in tsimu]
EF [inductive, in tsimu]
EF_tau2_elim [lemma, in tsimu]
EF_tau2Z_intro [lemma, in tsimu]
EF_tau2_WAIT [lemma, in tsimu]
EF_tau2_evt0 [lemma, in tsimu]
EF_tau2 [lemma, in tsimu]
EF0 [constructor, in tsimu]
EF1 [constructor, in tsimu]
ELab [constructor, in tsimu]
Enil [constructor, in tsimu]
Etau [constructor, in tsimu]
EU [inductive, in tsimu]
EU0 [constructor, in tsimu]
EU1 [constructor, in tsimu]
Event [variable, in tsimu]
EX [inductive, in tsimu]
EXE [definition, in tsimu]
exec [inductive, in tsimu]
execFrom [inductive, in tsimu]
EXE1 [inductive, in tsimu]
EXE1prf [constructor, in tsimu]
EXE2 [inductive, in tsimu]
EXE2prf [constructor, in tsimu]
EXE2_ex2 [lemma, in tsimu]
exInit [constructor, in tsimu]
EXprf [constructor, in tsimu]
EXT2 [inductive, in tsimu]
EXT2prf [constructor, in tsimu]
EX1 [definition, in tsimu]
EX2 [definition, in tsimu]

H

hasInit [inductive, in tsimu]

I

IMP [inductive, in tsimu]
IMPprf [constructor, in tsimu]
Init [projection, in tsimu]
Init [projection, in lts]
isDelay [definition, in tsimu]
isDevt [definition, in tsimu]
isDevt_dec [definition, in tsimu]
isEvt [definition, in tsimu]
isEvt1 [definition, in tsimu]
isTauD [definition, in tsimu]
isTauNonZeno [definition, in tsimu]
isTauNonZeno_nonZenoTauPath [lemma, in tsimu]
isTauZeno [inductive, in tsimu]
isTau2 [definition, in tsimu]
istlt [constructor, in time]
istz [constructor, in tsimu]
isWait [definition, in tsimu]

L

LEvent [projection, in tsimu]
LEvent [projection, in lts]
LEvents [inductive, in tsimu]
LTS [record, in lts]
LTS [section, in lts]
lts [library]
LTS.Event [variable, in lts]

M

mkLTS [constructor, in lts]
mkPState [constructor, in tsimu]
mono [lemma, in tsimu]
monotonous [definition, in tsimu]

N

ndeadlock_nDL1 [lemma, in tsimu]
ndeadlock_nDL2 [lemma, in tsimu]
nDL1 [definition, in tsimu]
nDL1_ndeadlock [lemma, in tsimu]
nDL2 [definition, in tsimu]
nDL2_ndeadlock [lemma, in tsimu]
NEprf [constructor, in tsimu]
Next [projection, in tsimu]
Next [projection, in lts]
NextD_inf_t_ex [constructor, in tsimu]
NextD_inf_t [inductive, in tsimu]
NextEvt [inductive, in tsimu]
nonZenoTauPath [definition, in tsimu]
nonZenoTauPath_isTauNonZeno [lemma, in tsimu]
notDelay [definition, in tsimu]

O

OK [constructor, in tsimu]
one_step [lemma, in tsimu]
open_or_closed [lemma, in tsimu]
OState [inductive, in tsimu]

P

pCFprf [constructor, in tsimu]
pCheck [definition, in tsimu]
pCheckFrom [inductive, in tsimu]
pCheckFrom_check [lemma, in tsimu]
pCheckFrom_EFD [lemma, in tsimu]
pCheckFrom_preEvt [lemma, in tsimu]
pCheckFrom_NextTau [lemma, in tsimu]
pCheckFrom_NextEvt [lemma, in tsimu]
pCheckFrom_state [lemma, in tsimu]
pCheck_refines [lemma, in tsimu]
pCheck_check [lemma, in tsimu]
PC1 [constructor, in tsimu]
PC2 [constructor, in tsimu]
PO1 [projection, in tsimu]
PO2 [projection, in tsimu]
preDly [definition, in tsimu]
preEvt [definition, in tsimu]
preevt0 [lemma, in tsimu]
pre_DLabDly_next [lemma, in tsimu]
pre_DLabDly_cut [lemma, in tsimu]
pre_DLabDly_evt0 [lemma, in tsimu]
prod_open_imp_proj_open [lemma, in tsimu]
prod_open_cond [record, in tsimu]
prod_closed_cases [inductive, in tsimu]
PState [record, in tsimu]

R

refines [definition, in tsimu]
right_open_prod [lemma, in tsimu]
right_open_is_unb [definition, in tsimu]
right_closed [definition, in tsimu]
right_open [definition, in tsimu]

S

skipTauWait [inductive, in tsimu]
skipTauWaitAtl1Tau [inductive, in tsimu]
skipTauWaitAtl1TauLeft [lemma, in tsimu]
skipTauWaitAtl1TauRight [lemma, in tsimu]
skipTauWaitAtl1Tau_skipTauWait [lemma, in tsimu]
skipTauWaitNZ [inductive, in tsimu]
skipTauWaitNZ_max_intro [lemma, in tsimu]
skipTauWait_skipTauWaitNZ [lemma, in tsimu]
skipTauWait1 [inductive, in tsimu]
skipTau2Wait [inductive, in tsimu]
skipTau2Wait_cutDelta1 [lemma, in tsimu]
skipTau2Wait_StateO [lemma, in tsimu]
skipTau2Wait_proj2 [lemma, in tsimu]
skipTau2Wait_Delta1 [lemma, in tsimu]
skipTau2Z_preEvt [lemma, in tsimu]
skip_delta_sim [lemma, in tsimu]
SSCG [definition, in tsimu]
State [projection, in tsimu]
State [projection, in lts]
StateD [projection, in tsimu]
StateO [projection, in tsimu]
State1 [projection, in tsimu]
State2 [projection, in tsimu]
stw1t [constructor, in tsimu]
st2wd [constructor, in tsimu]
st2we [constructor, in tsimu]
st2wn [constructor, in tsimu]

T

tadd [axiom, in time]
Tau [constructor, in tsimu]
TauSkipTauWait [lemma, in tsimu]
tau_delta_exch [definition, in tsimu]
tau0 [constructor, in tsimu]
tau1 [constructor, in tsimu]
Tau1 [constructor, in tsimu]
Tau2 [constructor, in tsimu]
Tau2Obs [lemma, in tsimu]
Tau2Proj1 [lemma, in tsimu]
Tau2SkipTau2Wait [lemma, in tsimu]
Tau2_skipTau2Wait [lemma, in tsimu]
Tau2_StateO [lemma, in tsimu]
Tau2_StateD [lemma, in tsimu]
Tau2_proj2 [lemma, in tsimu]
Tau2_proj1 [lemma, in tsimu]
teq_0_dec [axiom, in time]
Time [axiom, in time]
time [library]
timedPred [inductive, in tsimu]
TLabel [inductive, in tsimu]
tle [inductive, in time]
tleDiff [constructor, in time]
tle_lt_cases [lemma, in time]
tle_mono_l [lemma, in time]
tle_refl [lemma, in time]
tle_n_0 [lemma, in time]
tle_trans [lemma, in time]
tle_total [axiom, in time]
tlt [inductive, in time]
tlt_plus_nlt [lemma, in time]
tmin [definition, in time]
tmin_nz [lemma, in time]
tmin_ler [lemma, in time]
tmin_lel [lemma, in time]
tpDly [constructor, in tsimu]
tpGt [constructor, in tsimu]
tplus_opp_l [axiom, in time]
tplus_assoc [axiom, in time]
tplus_eq_0 [axiom, in time]
tplus_n_0 [axiom, in time]
tplus_0_n [axiom, in time]
tpTau [constructor, in tsimu]
Trace [inductive, in tsimu]
TrDiv [constructor, in tsimu]
TrEvent [constructor, in tsimu]
tsimu [library]
TTS [record, in tsimu]
TTS [section, in tsimu]
TTS.Event [variable, in tsimu]
tunb [axiom, in time]

W

WAIT [constructor, in tsimu]
wait_additivity [lemma, in tsimu]
wait2_additivity [lemma, in tsimu]
wdly1 [constructor, in tsimu]
wnop [constructor, in tsimu]
wtau [constructor, in tsimu]
wtau1 [constructor, in tsimu]