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

(579 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

(31 entries)

Module 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

(8 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

(1 entry)

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

(241 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

(15 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

(26 entries)

Projection 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

(75 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

(15 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

(1 entry)

Instance 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)

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

(148 entries)

Record 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

(16 entries)

---

Global Index

A

add_sr [definition, in LblStr]
ah1 [projection, in LblStr]
ah1b [projection, in LblStr]
ah1c [projection, in LblStr]
ah1d [projection, in LblStr]
ah13 [projection, in LblStr]
ah14 [projection, in LblStr]
ah15 [projection, in LblStr]
ah16 [projection, in LblStr]
ah17 [projection, in LblStr]
ah18 [projection, in LblStr]
ah2 [projection, in LblStr]
ah3 [projection, in LblStr]
ah4 [projection, in LblStr]
ah5 [projection, in LblStr]
ah8 [projection, in LblStr]
ah9 [projection, in LblStr]
alpha [inductive, in LblStr]
alpha_inl [lemma, in LblStr]
and_not_true [lemma, in LblStr]
apply [definition, in LblStr]
apply_inl [definition, in LblStr]
apply_inr [definition, in LblStr]
apply_spar_ter [lemma, in LblStr]
apply_spar_bis [lemma, in LblStr]
apply_spar [lemma, in LblStr]
apply_gpar [lemma, in LblStr]
AsInstanceOfSuperposition2 [module, in LblStr]
AsInstanceOfSuperposition2.actMax [definition, in LblStr]
AsInstanceOfSuperposition2.Clk [definition, in LblStr]
AsInstanceOfSuperposition2.Clk_TIdem [lemma, in LblStr]
AsInstanceOfSuperposition2.Clk_TDiag [lemma, in LblStr]
AsInstanceOfSuperposition2.Clk_Det [lemma, in LblStr]
AsInstanceOfSuperposition2.CLK_Idem [lemma, in LblStr]
AsInstanceOfSuperposition2.CLK_Diag [lemma, in LblStr]
AsInstanceOfSuperposition2.CLK_Trans_Det [lemma, in LblStr]
AsInstanceOfSuperposition2.CLK_Trans [definition, in LblStr]
AsInstanceOfSuperposition2.Ctrl [definition, in LblStr]
AsInstanceOfSuperposition2.GASRT_Trans [definition, in LblStr]
AsInstanceOfSuperposition2.GAT_Trans [definition, in LblStr]
AsInstanceOfSuperposition2.GA_SR_Idem [lemma, in LblStr]
AsInstanceOfSuperposition2.GA_SR_Diag [lemma, in LblStr]
AsInstanceOfSuperposition2.GA_SR_Det [lemma, in LblStr]
AsInstanceOfSuperposition2.GA_SR [definition, in LblStr]
AsInstanceOfSuperposition2.sem [definition, in LblStr]
AsInstanceOfSuperposition2.sem_prod [lemma, in LblStr]
AsInstanceOfSuperposition2.sem_ok [lemma, in LblStr]
AsInstanceOfSuperposition2.std_sem [definition, in LblStr]
AsInstanceOfSuperposition2.TA [definition, in LblStr]
assoc_hyp [record, in LblStr]
asynclr_par_assoc [lemma, in LblStr]
asyncl_par_assoc [lemma, in LblStr]
async_par_com [lemma, in LblStr]
atl2 [projection, in LblStr]
atl3 [projection, in LblStr]
atl4 [projection, in LblStr]
Atl4 [record, in LblStr]

B

binit [projection, in LblStr]
bisim [record, in LblStr]
bisim_trans [lemma, in LblStr]
bisim_sym [lemma, in LblStr]
bisim_refl [lemma, in LblStr]
bmap [projection, in LblStr]
btr12 [projection, in LblStr]
btr21 [projection, in LblStr]

C

CCS [module, in LblStr]
CCS.CCS_prod_assoc [lemma, in LblStr]
CCS.CCS_prod [definition, in LblStr]
CCS.CCS_LS_Assoc [lemma, in LblStr]
CCS.CCS_LS [definition, in LblStr]
CCS.CCS_Lbl [inductive, in LblStr]
CCS.Neg [constructor, in LblStr]
CCS.Pos [constructor, in LblStr]
CCS.Tau [constructor, in LblStr]
Clock [definition, in LblStr]
Compl [definition, in LblStr]
Compl_EMPTY [lemma, in LblStr]
Compl_UNIV [lemma, in LblStr]
Compositionnel [definition, in LblStr]
CSP [module, in LblStr]
CSP.CSP_prod_assoc [lemma, in LblStr]
CSP.CSP_prod [definition, in LblStr]
CSP.CSP_LS_Assoc [lemma, in LblStr]
CSP.CSP_LS [definition, in LblStr]
ctrans [definition, in LblStr]
ctrans_LE [lemma, in LblStr]

D

dist_par [definition, in LblStr]
dom_nopt_L [lemma, in LblStr]
dom_prod [lemma, in LblStr]
dom_sum [lemma, in LblStr]
dom_id [lemma, in LblStr]

E

eh1 [projection, in LblStr]
eh2 [projection, in LblStr]
eh3 [projection, in LblStr]
EMPTY [definition, in LblStr]
emptyCmd [definition, in LblStr]
EMPTY_and_r [lemma, in LblStr]
EMPTY_and_l [lemma, in LblStr]
EMPTY_prj2 [lemma, in LblStr]
EMPTY_prj1 [lemma, in LblStr]
EMPTY_extr [lemma, in LblStr]
EMPTY_extl [lemma, in LblStr]
EMPTY_Incl [lemma, in LblStr]
EMPTY_iprd_r [lemma, in LblStr]
EMPTY_iprd_l [lemma, in LblStr]
EMPTY_inc [lemma, in LblStr]
Equiv [definition, in LblStr]
Equiv_prod [lemma, in LblStr]
Equiv_sum [lemma, in LblStr]
Equiv_trans [lemma, in LblStr]
Equiv_sym [lemma, in LblStr]
Equiv_refl [lemma, in LblStr]
estb_r [projection, in LblStr]
estb_l [projection, in LblStr]
extl [definition, in LblStr]
Extl [definition, in LblStr]
extl_mono [lemma, in LblStr]
extr [definition, in LblStr]
Extr [definition, in LblStr]
extr_mono [lemma, in LblStr]
e_stable_prod [lemma, in LblStr]
e_stable_sum [lemma, in LblStr]
e_stable_id [lemma, in LblStr]
e_stable_nopt [lemma, in LblStr]
e_stable [record, in LblStr]

G

gen_par_assoc_CN [lemma, in LblStr]
gen_par_assoc_gen [lemma, in LblStr]
getLLab [definition, in LblStr]
getRLab [definition, in LblStr]
Guard_LE [lemma, in LblStr]

H

hasRcompo [definition, in LblStr]

I

inAlpha [constructor, in LblStr]
Incl [definition, in LblStr]
Incl_opt_nopt [lemma, in LblStr]
Incl_prod [lemma, in LblStr]
Incl_sum [lemma, in LblStr]
Incl_UNIV [lemma, in LblStr]
Incl_trans [lemma, in LblStr]
Incl_refl [lemma, in LblStr]
inc_trans [lemma, in LblStr]
inc_UNIV [lemma, in LblStr]
Init [projection, in LblStr]
inl_par [lemma, in LblStr]
Inter [inductive, in LblStr]
Interv [definition, in LblStr]
inter_prj2_monor [lemma, in LblStr]
inter_prj2_monol [lemma, in LblStr]
inter_prj1_monor [lemma, in LblStr]
inter_prj1_monol [lemma, in LblStr]
inter_inc_r [lemma, in LblStr]
inter_inc_l [lemma, in LblStr]
Inter_intro [constructor, in LblStr]
In_UNIV [lemma, in LblStr]
IProd [inductive, in LblStr]
IProd_intro [constructor, in LblStr]
ip_prod_dist [lemma, in LblStr]
ip_sum_dist [lemma, in LblStr]
isA [projection, in LblStr]
isACI [record, in LblStr]
isAssoc [record, in LblStr]
isAssoc1 [projection, in LblStr]
isAssoc2 [projection, in LblStr]
isAssoc3 [projection, in LblStr]
isAssoc4 [projection, in LblStr]
isAssoc5 [projection, in LblStr]
isC [projection, in LblStr]
isComm [record, in LblStr]
isComm1 [projection, in LblStr]
isComm2 [projection, in LblStr]
isCompat [definition, in LblStr]
isDet [definition, in LblStr]
isDet_Clock [lemma, in LblStr]
isDet_apply_inl [lemma, in LblStr]
isDet_outr [lemma, in LblStr]
isDet_outl [lemma, in LblStr]
isDet_union [lemma, in LblStr]
isDet_tr [lemma, in LblStr]
isDiag [definition, in LblStr]
isEnabled [definition, in LblStr]
isEnabledOrEmpty [definition, in LblStr]
isEnabledOrEmpty_tr [lemma, in LblStr]
isEnabled_tr [lemma, in LblStr]
isI [projection, in LblStr]
isIdem [definition, in LblStr]
isIMono [definition, in LblStr]
isInj [definition, in LblStr]
isInj_inl [lemma, in LblStr]
isInj_prod [lemma, in LblStr]
isInj_sum [lemma, in LblStr]
isInj_id [lemma, in LblStr]
isInj_nopt [lemma, in LblStr]
isInj_opt [lemma, in LblStr]
isInj_snd [lemma, in LblStr]
isInj_extr [lemma, in LblStr]
isInj_extl [lemma, in LblStr]
isJoin [definition, in LblStr]
isLLab [definition, in LblStr]
isLLab_stable [lemma, in LblStr]
isMono [definition, in LblStr]
isRcompat [definition, in LblStr]
isRcompo [definition, in LblStr]
isRcompo_prod [lemma, in LblStr]
isRcompo_sum [lemma, in LblStr]
isRLab [definition, in LblStr]
isStratified [record, in LblStr]
isStr1l [projection, in LblStr]
isStr1r [projection, in LblStr]
isStr2l1 [projection, in LblStr]
isStr2l2 [projection, in LblStr]
isStr2r1 [projection, in LblStr]
isStr2r2 [projection, in LblStr]
isSurj [definition, in LblStr]
isTDiag [definition, in LblStr]
isTDiag_Clock [lemma, in LblStr]
isTDiag_apply_inl [lemma, in LblStr]
isTDiag_outr [lemma, in LblStr]
isTDiag_outl [lemma, in LblStr]
isTDiag_union [lemma, in LblStr]
isTDiag_tr [lemma, in LblStr]
isTIdem [definition, in LblStr]
isTIdem_Clock [lemma, in LblStr]
isTIdem_apply_inl [lemma, in LblStr]
isTIdem_outr [lemma, in LblStr]
isTIdem_outl [lemma, in LblStr]
isTIdem_union [lemma, in LblStr]
isTIdem_tr [lemma, in LblStr]
isTotal [definition, in LblStr]
is_tle [constructor, in LblStr]
is_tr_eq [constructor, in LblStr]

L

Label [projection, in LblStr]
LblStr [record, in LblStr]
LblStr [library]
lbl_all [definition, in LblStr]
Lcnd [projection, in LblStr]
Lcnd_sum_LL [lemma, in LblStr]
Left [constructor, in LblStr]
Lerr [projection, in LblStr]
le_prd_l [lemma, in LblStr]
le_prd_r [lemma, in LblStr]
le_prd_elim [lemma, in LblStr]
le_prd_intro [lemma, in LblStr]
le_trans [lemma, in LblStr]
le_anti [lemma, in LblStr]
le_refl [lemma, in LblStr]
LLab [constructor, in LblStr]
Lprd [projection, in LblStr]
Lprd_sum_LL [lemma, in LblStr]
LR [constructor, in LblStr]
LRel [definition, in LblStr]
lsapply [inductive, in LblStr]
lsapplyPrf [constructor, in LblStr]
LSet [definition, in LblStr]
LSopt [definition, in LblStr]
LSoptAssoc [lemma, in LblStr]
LSoptComm [lemma, in LblStr]
LSoptIdem [lemma, in LblStr]
LSoptPS [lemma, in LblStr]
LSprod [definition, in LblStr]
LSprodAssoc [lemma, in LblStr]
LSprodComm [lemma, in LblStr]
LSprodIdem [lemma, in LblStr]
LSprodPS [lemma, in LblStr]
LSsum [definition, in LblStr]
LSsumAssoc [lemma, in LblStr]
LSsumComm [lemma, in LblStr]
LSsumIdem [lemma, in LblStr]
LSsumPS [lemma, in LblStr]
LS_le [definition, in LblStr]
LS_inj [definition, in LblStr]
LTS [record, in LblStr]
lts_outr [definition, in LblStr]
lts_opt [definition, in LblStr]
lts_outl [definition, in LblStr]
lts_inr [definition, in LblStr]
lts_inl [definition, in LblStr]
lts1 [definition, in LblStr]

M

mkBisim [constructor, in LblStr]
mkCmd [definition, in LblStr]
mkCmd_LE [lemma, in LblStr]
mkLS [constructor, in LblStr]
mkLTS [constructor, in LblStr]
mkRefines [constructor, in LblStr]
mkTransfo [constructor, in LblStr]
mkTTrans [constructor, in LblStr]
M_BASIC_ELEMS.GA_PS [lemma, in LblStr]
M_BASIC_ELEMS.GA_Mono [lemma, in LblStr]
M_BASIC_ELEMS.GA_Trans [definition, in LblStr]
M_BASIC_ELEMS.ClkAction_Trans [definition, in LblStr]
M_BASIC_ELEMS.Action_Mono [lemma, in LblStr]
M_BASIC_ELEMS.Guard_Mono [lemma, in LblStr]
M_BASIC_ELEMS.Action_Trans [definition, in LblStr]
M_BASIC_ELEMS.Guard_Trans [definition, in LblStr]
M_BASIC_ELEMS.TrSum_Idem [lemma, in LblStr]
M_BASIC_ELEMS.TrSum_Diag [lemma, in LblStr]
M_BASIC_ELEMS.TrSum_Det [lemma, in LblStr]
M_BASIC_ELEMS.TrProd_Det_r [lemma, in LblStr]
M_BASIC_ELEMS.TrProd_Det_l [lemma, in LblStr]
M_BASIC_ELEMS.TrSum_TotalOrEmpty [lemma, in LblStr]
M_BASIC_ELEMS.TrProd_Mono [lemma, in LblStr]
M_BASIC_ELEMS.Tr_Mono [definition, in LblStr]
M_BASIC_ELEMS.LS_le_LRLR [lemma, in LblStr]
M_BASIC_ELEMS.TrRecv_TotalOrEmpty [lemma, in LblStr]
M_BASIC_ELEMS.TrRecv [definition, in LblStr]
M_BASIC_ELEMS.TrSR [definition, in LblStr]
M_BASIC_ELEMS.TrSum [definition, in LblStr]
M_BASIC_ELEMS.TrProd [definition, in LblStr]
M_BASIC_ELEMS.TrTotalOrEmpty [definition, in LblStr]
M_BASIC_ELEMS.TrIdem [definition, in LblStr]
M_BASIC_ELEMS.TrDiag [definition, in LblStr]
M_BASIC_ELEMS.TrDet [definition, in LblStr]
M_BASIC_ELEMS.Transition [definition, in LblStr]
M_BASIC_ELEMS.Transitions [section, in LblStr]
M_BASIC_ELEMS.GA [definition, in LblStr]
M_BASIC_ELEMS.GuardPS [lemma, in LblStr]
M_BASIC_ELEMS.Guard [definition, in LblStr]
M_BASIC_ELEMS.ActionPS [lemma, in LblStr]
M_BASIC_ELEMS.Action_idem [lemma, in LblStr]
M_BASIC_ELEMS.Action_assoc [lemma, in LblStr]
M_BASIC_ELEMS.Action_comm [lemma, in LblStr]
M_BASIC_ELEMS.action_eq [lemma, in LblStr]
M_BASIC_ELEMS.Action [definition, in LblStr]
M_BASIC_ELEMS.act_ok [projection, in LblStr]
M_BASIC_ELEMS.act_nop [projection, in LblStr]
M_BASIC_ELEMS.act_reset [projection, in LblStr]
M_BASIC_ELEMS.action [record, in LblStr]
M_BASIC_ELEMS.INVARIANT [definition, in LblStr]
M_BASIC_ELEMS.InvPS [lemma, in LblStr]
M_BASIC_ELEMS.Invariant [definition, in LblStr]
M_BASIC_ELEMS [module, in LblStr]
M_INVARIANT.isem_ok [lemma, in LblStr]
M_INVARIANT.ictrans_LE [lemma, in LblStr]
M_INVARIANT.std_isem [definition, in LblStr]
M_INVARIANT.ittrans [definition, in LblStr]
M_INVARIANT.ictrans [definition, in LblStr]
M_INVARIANT.isem_prod [lemma, in LblStr]
M_INVARIANT.isem [definition, in LblStr]
M_INVARIANT.uZero [instance, in LblStr]
M_INVARIANT.isTIdem_IClock [lemma, in LblStr]
M_INVARIANT.isTDiag_IClock [lemma, in LblStr]
M_INVARIANT.isDet_IClock [lemma, in LblStr]
M_INVARIANT.IClock [definition, in LblStr]
M_INVARIANT.ITA [definition, in LblStr]
M_INVARIANT.INVARIANT_PS [lemma, in LblStr]
M_INVARIANT.INVARIANT_idem [lemma, in LblStr]
M_INVARIANT.INVARIANT_assoc [lemma, in LblStr]
M_INVARIANT.INVARIANT_comm [lemma, in LblStr]
M_INVARIANT.INVARIANT [definition, in LblStr]
M_INVARIANT [module, in LblStr]
M_ACTION.SRAction_PS [lemma, in LblStr]
M_ACTION.SRAction [definition, in LblStr]
M_ACTION.GuardedAction_PS [lemma, in LblStr]
M_ACTION.GuardedAction_idem [lemma, in LblStr]
M_ACTION.GuardedAction_assoc [lemma, in LblStr]
M_ACTION.GuardedAction_comm [lemma, in LblStr]
M_ACTION.GuardedAction [definition, in LblStr]
M_ACTION.CkLabel_eq [lemma, in LblStr]
M_ACTION.gaNop [definition, in LblStr]
M_ACTION.gaRst [definition, in LblStr]
M_ACTION.gaGuard [definition, in LblStr]
M_ACTION.CkOK [projection, in LblStr]
M_ACTION.CkNop [projection, in LblStr]
M_ACTION.CkRst [projection, in LblStr]
M_ACTION.CkGuard [projection, in LblStr]
M_ACTION.CkLabel [record, in LblStr]
M_ACTION [module, in LblStr]

N

ne_ex [constructor, in LblStr]
NopRst_LE [lemma, in LblStr]
Nop_LE [lemma, in LblStr]
notIdem [definition, in LblStr]
notIsLLab_stable [lemma, in LblStr]
notTotal [definition, in LblStr]
not_false [lemma, in LblStr]
not_empty [inductive, in LblStr]
not_LLab [lemma, in LblStr]
not_in_EMPTY [lemma, in LblStr]

O

optUnit [instance, in LblStr]
outl_par [lemma, in LblStr]
outr_par [lemma, in LblStr]

P

papply [definition, in LblStr]
papp_prod [lemma, in LblStr]
papp_sum_L [lemma, in LblStr]
par_idem_det [lemma, in LblStr]
par_idem_tot [lemma, in LblStr]
par_sat [lemma, in LblStr]
par_alpha_inc [lemma, in LblStr]
par_com [lemma, in LblStr]
par_assoc_weak [lemma, in LblStr]
Prd [definition, in LblStr]
prd_mkCmd [lemma, in LblStr]
prjl [definition, in LblStr]
prjr [definition, in LblStr]
Prj1 [inductive, in LblStr]
prj1_mono [lemma, in LblStr]
Prj1_intro [constructor, in LblStr]
Prj2 [inductive, in LblStr]
prj2_mono [lemma, in LblStr]
Prj2_intro [constructor, in LblStr]
prod [definition, in LblStr]
prod_compat [lemma, in LblStr]
PTrans [inductive, in LblStr]
p_prod [definition, in LblStr]
p_sum [definition, in LblStr]

R

ran_id [lemma, in LblStr]
ran_prod [lemma, in LblStr]
ran_sum [lemma, in LblStr]
rcompo_comp [lemma, in LblStr]
rcompo_id [lemma, in LblStr]
rcompo_snd [lemma, in LblStr]
rcompo_nopt [lemma, in LblStr]
rcompo_opt [lemma, in LblStr]
rcompo_extl [lemma, in LblStr]
rcompo_extr [lemma, in LblStr]
rcompo_outl [lemma, in LblStr]
rcompo_outr [lemma, in LblStr]
rcompo_inr [lemma, in LblStr]
rcompo_inl [lemma, in LblStr]
refines [record, in LblStr]
Restr [definition, in LblStr]
Right [constructor, in LblStr]
rinit [projection, in LblStr]
RLab [constructor, in LblStr]
rmap [projection, in LblStr]
Rprod [definition, in LblStr]
Rst_LE [lemma, in LblStr]
Rsum [definition, in LblStr]
rtr12 [projection, in LblStr]
rtr21 [projection, in LblStr]
r_id [definition, in LblStr]

S

sat_UNIV [lemma, in LblStr]
sem [definition, in LblStr]
sem_prod [lemma, in LblStr]
sem_ok [lemma, in LblStr]
Sprod [definition, in LblStr]
sr_PS [lemma, in LblStr]
sr_idem [lemma, in LblStr]
sr_assoc [lemma, in LblStr]
sr_comm [lemma, in LblStr]
stable [record, in LblStr]
stable_prod [lemma, in LblStr]
stable_sum [lemma, in LblStr]
stable_comp [lemma, in LblStr]
stable_id [lemma, in LblStr]
stable_opt [lemma, in LblStr]
stable_snd [lemma, in LblStr]
stable_extl [lemma, in LblStr]
stable_inl [lemma, in LblStr]
stable_inter [lemma, in LblStr]
stable_EMPTY [lemma, in LblStr]
stable_UNIV [lemma, in LblStr]
stable_e_stable [lemma, in LblStr]
State [projection, in LblStr]
stb_pr [projection, in LblStr]
stb_pl [projection, in LblStr]
stb_er [projection, in LblStr]
stb_el [projection, in LblStr]
std_sem [definition, in LblStr]
SumLabs [inductive, in LblStr]
SUPERPOSITION [module, in LblStr]
SUPERPOSITION.isMax_inl [definition, in LblStr]
SUPERPOSITION.isMono [definition, in LblStr]
SUPERPOSITION.isMono_extr [definition, in LblStr]
SUPERPOSITION.isMono_inl [definition, in LblStr]
SUPERPOSITION.spsem [definition, in LblStr]
SUPERPOSITION.spsem_prod [lemma, in LblStr]
SUPERPOSITION.spsem_ok [lemma, in LblStr]
SUPERPOSITION.std_spsem [definition, in LblStr]
SUPERPOSITION2 [module, in LblStr]
SUPERPOSITION2.isMono_sr_inl [definition, in LblStr]
SUPERPOSITION2.isMono_inl [definition, in LblStr]
SUPERPOSITION2.isRecv_inl [definition, in LblStr]
SUPERPOSITION2.spsem [definition, in LblStr]
SUPERPOSITION2.spsem_prod [lemma, in LblStr]
SUPERPOSITION2.spsem_ok [lemma, in LblStr]
SUPERPOSITION2.std_spsem [definition, in LblStr]
SUPERPOSITION2.tr_inl_psum [lemma, in LblStr]
sync_async [lemma, in LblStr]

T

TA [definition, in LblStr]
tadd [axiom, in LblStr]
tadd_eq0 [axiom, in LblStr]
tadd_reg_l [axiom, in LblStr]
tadd_assoc [axiom, in LblStr]
tadd_n_0 [axiom, in LblStr]
teq_dec [axiom, in LblStr]
tfr_sat_rl [lemma, in LblStr]
tfr_nopt [definition, in LblStr]
tfr_opt [definition, in LblStr]
tfr_nrcv [definition, in LblStr]
tfr_rcv [definition, in LblStr]
tfr_nsnd [definition, in LblStr]
tfr_snd [definition, in LblStr]
tfr_ran_intro [constructor, in LblStr]
tfr_ran [inductive, in LblStr]
tfr_prd [projection, in LblStr]
tfr_cnd [projection, in LblStr]
tfr_img [projection, in LblStr]
tfr_map [projection, in LblStr]
tfr_dom [projection, in LblStr]
TIME [definition, in LblStr]
Time [axiom, in LblStr]
TIME_PS [lemma, in LblStr]
TIME_idem [lemma, in LblStr]
TIME_assoc [lemma, in LblStr]
TIME_comm [lemma, in LblStr]
tle [inductive, in LblStr]
tle_trans [lemma, in LblStr]
tle_anti [lemma, in LblStr]
tle_refl [lemma, in LblStr]
tmin [axiom, in LblStr]
tmin_tt [lemma, in LblStr]
tmin_l [axiom, in LblStr]
tmin_r [axiom, in LblStr]
tmin_intro [axiom, in LblStr]
tmin_assoc [axiom, in LblStr]
tmin_comm [axiom, in LblStr]
Trans [projection, in LblStr]
Transfo [definition, in LblStr]
transfo [record, in LblStr]
trans_eq [inductive, in LblStr]
tr_sat [lemma, in LblStr]
tr_all [lemma, in LblStr]
tr_compat [lemma, in LblStr]
tr_prod [definition, in LblStr]
tr_sum [definition, in LblStr]
tr_inl_psum [lemma, in LblStr]
tr_id [definition, in LblStr]
tr_extr [definition, in LblStr]
tr_extl [definition, in LblStr]
tr_outr [definition, in LblStr]
tr_outl [definition, in LblStr]
tr_inr [definition, in LblStr]
tr_inl [definition, in LblStr]
tr_comp [definition, in LblStr]
ttrans [definition, in LblStr]
TTrans [inductive, in LblStr]

U

union [definition, in LblStr]
Union [inductive, in LblStr]
Union_r [constructor, in LblStr]
Union_l [constructor, in LblStr]
unit [projection, in LblStr]
Unit [record, in LblStr]
unit_r [projection, in LblStr]
unit_l [projection, in LblStr]
unit_def [projection, in LblStr]
UNIV [definition, in LblStr]
UNIV_prod [lemma, in LblStr]
UNIV_sum [lemma, in LblStr]

V

V [axiom, in LblStr]

Z

Zero [axiom, in LblStr]

other

_ |t| _ [notation, in LblStr]
_ |{ _ }| _ [notation, in LblStr]
_ |[ _ , _ , _ ]| _ [notation, in LblStr]
_ =[ _ ]= _ [notation, in LblStr]
_ == _ [notation, in LblStr]
_ |= _ [notation, in LblStr]
_ *tr* _ [notation, in LblStr]
_ +tr+ _ [notation, in LblStr]
_ =tr= _ [notation, in LblStr]
_ @tr@ _ [notation, in LblStr]
_ !? [notation, in LblStr]
_ *r* _ [notation, in LblStr]
_ +r+ _ [notation, in LblStr]
_ *p* _ [notation, in LblStr]
_ +p+ _ [notation, in LblStr]
_ ? [notation, in LblStr]
_ +l+ _ [notation, in LblStr]
_ *l* _ [notation, in LblStr]
_ or _ [notation, in LblStr]
_ & _ [notation, in LblStr]
_ .2 [notation, in LblStr]
_ .1 [notation, in LblStr]
_ ! [notation, in LblStr]
_ *ip* _ [notation, in LblStr]
_ <:> _ [notation, in LblStr]
_ <: _ [notation, in LblStr]
! _ [notation, in LblStr]
# _ [notation, in LblStr]
[ _ ] _ [notation, in LblStr]
[[ _ ]] [notation, in LblStr]
{{ _ }} [notation, in LblStr]

---

Notation Index

other

_ |t| _ [in LblStr]
_ |{ _ }| _ [in LblStr]
_ |[ _ , _ , _ ]| _ [in LblStr]
_ =[ _ ]= _ [in LblStr]
_ == _ [in LblStr]
_ |= _ [in LblStr]
_ *tr* _ [in LblStr]
_ +tr+ _ [in LblStr]
_ =tr= _ [in LblStr]
_ @tr@ _ [in LblStr]
_ !? [in LblStr]
_ *r* _ [in LblStr]
_ +r+ _ [in LblStr]
_ *p* _ [in LblStr]
_ +p+ _ [in LblStr]
_ ? [in LblStr]
_ +l+ _ [in LblStr]
_ *l* _ [in LblStr]
_ or _ [in LblStr]
_ & _ [in LblStr]
_ .2 [in LblStr]
_ .1 [in LblStr]
_ ! [in LblStr]
_ *ip* _ [in LblStr]
_ <:> _ [in LblStr]
_ <: _ [in LblStr]
! _ [in LblStr]
# _ [in LblStr]
[ _ ] _ [in LblStr]
[[ _ ]] [in LblStr]
{{ _ }} [in LblStr]

---

Module Index

A

AsInstanceOfSuperposition2 [in LblStr]

C

CCS [in LblStr]
CSP [in LblStr]

M

M_BASIC_ELEMS [in LblStr]
M_INVARIANT [in LblStr]
M_ACTION [in LblStr]

S

SUPERPOSITION [in LblStr]
SUPERPOSITION2 [in LblStr]

---

Library Index

L

LblStr

---

Lemma Index

A

alpha_inl [in LblStr]
and_not_true [in LblStr]
apply_spar_ter [in LblStr]
apply_spar_bis [in LblStr]
apply_spar [in LblStr]
apply_gpar [in LblStr]
AsInstanceOfSuperposition2.Clk_TIdem [in LblStr]
AsInstanceOfSuperposition2.Clk_TDiag [in LblStr]
AsInstanceOfSuperposition2.Clk_Det [in LblStr]
AsInstanceOfSuperposition2.CLK_Idem [in LblStr]
AsInstanceOfSuperposition2.CLK_Diag [in LblStr]
AsInstanceOfSuperposition2.CLK_Trans_Det [in LblStr]
AsInstanceOfSuperposition2.GA_SR_Idem [in LblStr]
AsInstanceOfSuperposition2.GA_SR_Diag [in LblStr]
AsInstanceOfSuperposition2.GA_SR_Det [in LblStr]
AsInstanceOfSuperposition2.sem_prod [in LblStr]
AsInstanceOfSuperposition2.sem_ok [in LblStr]
asynclr_par_assoc [in LblStr]
asyncl_par_assoc [in LblStr]
async_par_com [in LblStr]

B

bisim_trans [in LblStr]
bisim_sym [in LblStr]
bisim_refl [in LblStr]

C

CCS.CCS_prod_assoc [in LblStr]
CCS.CCS_LS_Assoc [in LblStr]
Compl_EMPTY [in LblStr]
Compl_UNIV [in LblStr]
CSP.CSP_prod_assoc [in LblStr]
CSP.CSP_LS_Assoc [in LblStr]
ctrans_LE [in LblStr]

D

dom_nopt_L [in LblStr]
dom_prod [in LblStr]
dom_sum [in LblStr]
dom_id [in LblStr]

E

EMPTY_and_r [in LblStr]
EMPTY_and_l [in LblStr]
EMPTY_prj2 [in LblStr]
EMPTY_prj1 [in LblStr]
EMPTY_extr [in LblStr]
EMPTY_extl [in LblStr]
EMPTY_Incl [in LblStr]
EMPTY_iprd_r [in LblStr]
EMPTY_iprd_l [in LblStr]
EMPTY_inc [in LblStr]
Equiv_prod [in LblStr]
Equiv_sum [in LblStr]
Equiv_trans [in LblStr]
Equiv_sym [in LblStr]
Equiv_refl [in LblStr]
extl_mono [in LblStr]
extr_mono [in LblStr]
e_stable_prod [in LblStr]
e_stable_sum [in LblStr]
e_stable_id [in LblStr]
e_stable_nopt [in LblStr]

G

gen_par_assoc_CN [in LblStr]
gen_par_assoc_gen [in LblStr]
Guard_LE [in LblStr]

I

Incl_opt_nopt [in LblStr]
Incl_prod [in LblStr]
Incl_sum [in LblStr]
Incl_UNIV [in LblStr]
Incl_trans [in LblStr]
Incl_refl [in LblStr]
inc_trans [in LblStr]
inc_UNIV [in LblStr]
inl_par [in LblStr]
inter_prj2_monor [in LblStr]
inter_prj2_monol [in LblStr]
inter_prj1_monor [in LblStr]
inter_prj1_monol [in LblStr]
inter_inc_r [in LblStr]
inter_inc_l [in LblStr]
In_UNIV [in LblStr]
ip_prod_dist [in LblStr]
ip_sum_dist [in LblStr]
isDet_Clock [in LblStr]
isDet_apply_inl [in LblStr]
isDet_outr [in LblStr]
isDet_outl [in LblStr]
isDet_union [in LblStr]
isDet_tr [in LblStr]
isEnabledOrEmpty_tr [in LblStr]
isEnabled_tr [in LblStr]
isInj_inl [in LblStr]
isInj_prod [in LblStr]
isInj_sum [in LblStr]
isInj_id [in LblStr]
isInj_nopt [in LblStr]
isInj_opt [in LblStr]
isInj_snd [in LblStr]
isInj_extr [in LblStr]
isInj_extl [in LblStr]
isLLab_stable [in LblStr]
isRcompo_prod [in LblStr]
isRcompo_sum [in LblStr]
isTDiag_Clock [in LblStr]
isTDiag_apply_inl [in LblStr]
isTDiag_outr [in LblStr]
isTDiag_outl [in LblStr]
isTDiag_union [in LblStr]
isTDiag_tr [in LblStr]
isTIdem_Clock [in LblStr]
isTIdem_apply_inl [in LblStr]
isTIdem_outr [in LblStr]
isTIdem_outl [in LblStr]
isTIdem_union [in LblStr]
isTIdem_tr [in LblStr]

L

Lcnd_sum_LL [in LblStr]
le_prd_l [in LblStr]
le_prd_r [in LblStr]
le_prd_elim [in LblStr]
le_prd_intro [in LblStr]
le_trans [in LblStr]
le_anti [in LblStr]
le_refl [in LblStr]
Lprd_sum_LL [in LblStr]
LSoptAssoc [in LblStr]
LSoptComm [in LblStr]
LSoptIdem [in LblStr]
LSoptPS [in LblStr]
LSprodAssoc [in LblStr]
LSprodComm [in LblStr]
LSprodIdem [in LblStr]
LSprodPS [in LblStr]
LSsumAssoc [in LblStr]
LSsumComm [in LblStr]
LSsumIdem [in LblStr]
LSsumPS [in LblStr]

M

mkCmd_LE [in LblStr]
M_BASIC_ELEMS.GA_PS [in LblStr]
M_BASIC_ELEMS.GA_Mono [in LblStr]
M_BASIC_ELEMS.Action_Mono [in LblStr]
M_BASIC_ELEMS.Guard_Mono [in LblStr]
M_BASIC_ELEMS.TrSum_Idem [in LblStr]
M_BASIC_ELEMS.TrSum_Diag [in LblStr]
M_BASIC_ELEMS.TrSum_Det [in LblStr]
M_BASIC_ELEMS.TrProd_Det_r [in LblStr]
M_BASIC_ELEMS.TrProd_Det_l [in LblStr]
M_BASIC_ELEMS.TrSum_TotalOrEmpty [in LblStr]
M_BASIC_ELEMS.TrProd_Mono [in LblStr]
M_BASIC_ELEMS.LS_le_LRLR [in LblStr]
M_BASIC_ELEMS.TrRecv_TotalOrEmpty [in LblStr]
M_BASIC_ELEMS.GuardPS [in LblStr]
M_BASIC_ELEMS.ActionPS [in LblStr]
M_BASIC_ELEMS.Action_idem [in LblStr]
M_BASIC_ELEMS.Action_assoc [in LblStr]
M_BASIC_ELEMS.Action_comm [in LblStr]
M_BASIC_ELEMS.action_eq [in LblStr]
M_BASIC_ELEMS.InvPS [in LblStr]
M_INVARIANT.isem_ok [in LblStr]
M_INVARIANT.ictrans_LE [in LblStr]
M_INVARIANT.isem_prod [in LblStr]
M_INVARIANT.isTIdem_IClock [in LblStr]
M_INVARIANT.isTDiag_IClock [in LblStr]
M_INVARIANT.isDet_IClock [in LblStr]
M_INVARIANT.INVARIANT_PS [in LblStr]
M_INVARIANT.INVARIANT_idem [in LblStr]
M_INVARIANT.INVARIANT_assoc [in LblStr]
M_INVARIANT.INVARIANT_comm [in LblStr]
M_ACTION.SRAction_PS [in LblStr]
M_ACTION.GuardedAction_PS [in LblStr]
M_ACTION.GuardedAction_idem [in LblStr]
M_ACTION.GuardedAction_assoc [in LblStr]
M_ACTION.GuardedAction_comm [in LblStr]
M_ACTION.CkLabel_eq [in LblStr]

N

NopRst_LE [in LblStr]
Nop_LE [in LblStr]
notIsLLab_stable [in LblStr]
not_false [in LblStr]
not_LLab [in LblStr]
not_in_EMPTY [in LblStr]

O

outl_par [in LblStr]
outr_par [in LblStr]

P

papp_prod [in LblStr]
papp_sum_L [in LblStr]
par_idem_det [in LblStr]
par_idem_tot [in LblStr]
par_sat [in LblStr]
par_alpha_inc [in LblStr]
par_com [in LblStr]
par_assoc_weak [in LblStr]
prd_mkCmd [in LblStr]
prj1_mono [in LblStr]
prj2_mono [in LblStr]
prod_compat [in LblStr]

R

ran_id [in LblStr]
ran_prod [in LblStr]
ran_sum [in LblStr]
rcompo_comp [in LblStr]
rcompo_id [in LblStr]
rcompo_snd [in LblStr]
rcompo_nopt [in LblStr]
rcompo_opt [in LblStr]
rcompo_extl [in LblStr]
rcompo_extr [in LblStr]
rcompo_outl [in LblStr]
rcompo_outr [in LblStr]
rcompo_inr [in LblStr]
rcompo_inl [in LblStr]
Rst_LE [in LblStr]

S

sat_UNIV [in LblStr]
sem_prod [in LblStr]
sem_ok [in LblStr]
sr_PS [in LblStr]
sr_idem [in LblStr]
sr_assoc [in LblStr]
sr_comm [in LblStr]
stable_prod [in LblStr]
stable_sum [in LblStr]
stable_comp [in LblStr]
stable_id [in LblStr]
stable_opt [in LblStr]
stable_snd [in LblStr]
stable_extl [in LblStr]
stable_inl [in LblStr]
stable_inter [in LblStr]
stable_EMPTY [in LblStr]
stable_UNIV [in LblStr]
stable_e_stable [in LblStr]
SUPERPOSITION.spsem_prod [in LblStr]
SUPERPOSITION.spsem_ok [in LblStr]
SUPERPOSITION2.spsem_prod [in LblStr]
SUPERPOSITION2.spsem_ok [in LblStr]
SUPERPOSITION2.tr_inl_psum [in LblStr]
sync_async [in LblStr]

T

tfr_sat_rl [in LblStr]
TIME_PS [in LblStr]
TIME_idem [in LblStr]
TIME_assoc [in LblStr]
TIME_comm [in LblStr]
tle_trans [in LblStr]
tle_anti [in LblStr]
tle_refl [in LblStr]
tmin_tt [in LblStr]
tr_sat [in LblStr]
tr_all [in LblStr]
tr_compat [in LblStr]
tr_inl_psum [in LblStr]

U

UNIV_prod [in LblStr]
UNIV_sum [in LblStr]

---

Axiom Index

T

tadd [in LblStr]
tadd_eq0 [in LblStr]
tadd_reg_l [in LblStr]
tadd_assoc [in LblStr]
tadd_n_0 [in LblStr]
teq_dec [in LblStr]
Time [in LblStr]
tmin [in LblStr]
tmin_l [in LblStr]
tmin_r [in LblStr]
tmin_intro [in LblStr]
tmin_assoc [in LblStr]
tmin_comm [in LblStr]

V

V [in LblStr]

Z

Zero [in LblStr]

---

Constructor Index

C

CCS.Neg [in LblStr]
CCS.Pos [in LblStr]
CCS.Tau [in LblStr]

I

inAlpha [in LblStr]
Inter_intro [in LblStr]
IProd_intro [in LblStr]
is_tle [in LblStr]
is_tr_eq [in LblStr]

L

Left [in LblStr]
LLab [in LblStr]
LR [in LblStr]
lsapplyPrf [in LblStr]

M

mkBisim [in LblStr]
mkLS [in LblStr]
mkLTS [in LblStr]
mkRefines [in LblStr]
mkTransfo [in LblStr]
mkTTrans [in LblStr]

N

ne_ex [in LblStr]

P

Prj1_intro [in LblStr]
Prj2_intro [in LblStr]

R

Right [in LblStr]
RLab [in LblStr]

T

tfr_ran_intro [in LblStr]

U

Union_r [in LblStr]
Union_l [in LblStr]

---

Projection Index

A

ah1 [in LblStr]
ah1b [in LblStr]
ah1c [in LblStr]
ah1d [in LblStr]
ah13 [in LblStr]
ah14 [in LblStr]
ah15 [in LblStr]
ah16 [in LblStr]
ah17 [in LblStr]
ah18 [in LblStr]
ah2 [in LblStr]
ah3 [in LblStr]
ah4 [in LblStr]
ah5 [in LblStr]
ah8 [in LblStr]
ah9 [in LblStr]
atl2 [in LblStr]
atl3 [in LblStr]
atl4 [in LblStr]

B

binit [in LblStr]
bmap [in LblStr]
btr12 [in LblStr]
btr21 [in LblStr]

E

eh1 [in LblStr]
eh2 [in LblStr]
eh3 [in LblStr]
estb_r [in LblStr]
estb_l [in LblStr]

I

Init [in LblStr]
isA [in LblStr]
isAssoc1 [in LblStr]
isAssoc2 [in LblStr]
isAssoc3 [in LblStr]
isAssoc4 [in LblStr]
isAssoc5 [in LblStr]
isC [in LblStr]
isComm1 [in LblStr]
isComm2 [in LblStr]
isI [in LblStr]
isStr1l [in LblStr]
isStr1r [in LblStr]
isStr2l1 [in LblStr]
isStr2l2 [in LblStr]
isStr2r1 [in LblStr]
isStr2r2 [in LblStr]

L

Label [in LblStr]
Lcnd [in LblStr]
Lerr [in LblStr]
Lprd [in LblStr]

M

M_BASIC_ELEMS.act_ok [in LblStr]
M_BASIC_ELEMS.act_nop [in LblStr]
M_BASIC_ELEMS.act_reset [in LblStr]
M_ACTION.CkOK [in LblStr]
M_ACTION.CkNop [in LblStr]
M_ACTION.CkRst [in LblStr]
M_ACTION.CkGuard [in LblStr]

R

rinit [in LblStr]
rmap [in LblStr]
rtr12 [in LblStr]
rtr21 [in LblStr]

S

State [in LblStr]
stb_pr [in LblStr]
stb_pl [in LblStr]
stb_er [in LblStr]
stb_el [in LblStr]

T

tfr_prd [in LblStr]
tfr_cnd [in LblStr]
tfr_img [in LblStr]
tfr_map [in LblStr]
tfr_dom [in LblStr]
Trans [in LblStr]

U

unit [in LblStr]
unit_r [in LblStr]
unit_l [in LblStr]
unit_def [in LblStr]

---

Inductive Index

A

alpha [in LblStr]

C

CCS.CCS_Lbl [in LblStr]

I

Inter [in LblStr]
IProd [in LblStr]

L

lsapply [in LblStr]

N

not_empty [in LblStr]

P

Prj1 [in LblStr]
Prj2 [in LblStr]
PTrans [in LblStr]

S

SumLabs [in LblStr]

T

tfr_ran [in LblStr]
tle [in LblStr]
trans_eq [in LblStr]
TTrans [in LblStr]

U

Union [in LblStr]

---

Section Index

M

M_BASIC_ELEMS.Transitions [in LblStr]

---

Instance Index

M

M_INVARIANT.uZero [in LblStr]

O

optUnit [in LblStr]

---

Definition Index

A

add_sr [in LblStr]
apply [in LblStr]
apply_inl [in LblStr]
apply_inr [in LblStr]
AsInstanceOfSuperposition2.actMax [in LblStr]
AsInstanceOfSuperposition2.Clk [in LblStr]
AsInstanceOfSuperposition2.CLK_Trans [in LblStr]
AsInstanceOfSuperposition2.Ctrl [in LblStr]
AsInstanceOfSuperposition2.GASRT_Trans [in LblStr]
AsInstanceOfSuperposition2.GAT_Trans [in LblStr]
AsInstanceOfSuperposition2.GA_SR [in LblStr]
AsInstanceOfSuperposition2.sem [in LblStr]
AsInstanceOfSuperposition2.std_sem [in LblStr]
AsInstanceOfSuperposition2.TA [in LblStr]

C

CCS.CCS_prod [in LblStr]
CCS.CCS_LS [in LblStr]
Clock [in LblStr]
Compl [in LblStr]
Compositionnel [in LblStr]
CSP.CSP_prod [in LblStr]
CSP.CSP_LS [in LblStr]
ctrans [in LblStr]

D

dist_par [in LblStr]

E

EMPTY [in LblStr]
emptyCmd [in LblStr]
Equiv [in LblStr]
extl [in LblStr]
Extl [in LblStr]
extr [in LblStr]
Extr [in LblStr]

G

getLLab [in LblStr]
getRLab [in LblStr]

H

hasRcompo [in LblStr]

I

Incl [in LblStr]
Interv [in LblStr]
isCompat [in LblStr]
isDet [in LblStr]
isDiag [in LblStr]
isEnabled [in LblStr]
isEnabledOrEmpty [in LblStr]
isIdem [in LblStr]
isIMono [in LblStr]
isInj [in LblStr]
isJoin [in LblStr]
isLLab [in LblStr]
isMono [in LblStr]
isRcompat [in LblStr]
isRcompo [in LblStr]
isRLab [in LblStr]
isSurj [in LblStr]
isTDiag [in LblStr]
isTIdem [in LblStr]
isTotal [in LblStr]

L

lbl_all [in LblStr]
LRel [in LblStr]
LSet [in LblStr]
LSopt [in LblStr]
LSprod [in LblStr]
LSsum [in LblStr]
LS_le [in LblStr]
LS_inj [in LblStr]
lts_outr [in LblStr]
lts_opt [in LblStr]
lts_outl [in LblStr]
lts_inr [in LblStr]
lts_inl [in LblStr]
lts1 [in LblStr]

M

mkCmd [in LblStr]
M_BASIC_ELEMS.GA_Trans [in LblStr]
M_BASIC_ELEMS.ClkAction_Trans [in LblStr]
M_BASIC_ELEMS.Action_Trans [in LblStr]
M_BASIC_ELEMS.Guard_Trans [in LblStr]
M_BASIC_ELEMS.Tr_Mono [in LblStr]
M_BASIC_ELEMS.TrRecv [in LblStr]
M_BASIC_ELEMS.TrSR [in LblStr]
M_BASIC_ELEMS.TrSum [in LblStr]
M_BASIC_ELEMS.TrProd [in LblStr]
M_BASIC_ELEMS.TrTotalOrEmpty [in LblStr]
M_BASIC_ELEMS.TrIdem [in LblStr]
M_BASIC_ELEMS.TrDiag [in LblStr]
M_BASIC_ELEMS.TrDet [in LblStr]
M_BASIC_ELEMS.Transition [in LblStr]
M_BASIC_ELEMS.GA [in LblStr]
M_BASIC_ELEMS.Guard [in LblStr]
M_BASIC_ELEMS.Action [in LblStr]
M_BASIC_ELEMS.INVARIANT [in LblStr]
M_BASIC_ELEMS.Invariant [in LblStr]
M_INVARIANT.std_isem [in LblStr]
M_INVARIANT.ittrans [in LblStr]
M_INVARIANT.ictrans [in LblStr]
M_INVARIANT.isem [in LblStr]
M_INVARIANT.IClock [in LblStr]
M_INVARIANT.ITA [in LblStr]
M_INVARIANT.INVARIANT [in LblStr]
M_ACTION.SRAction [in LblStr]
M_ACTION.GuardedAction [in LblStr]
M_ACTION.gaNop [in LblStr]
M_ACTION.gaRst [in LblStr]
M_ACTION.gaGuard [in LblStr]

N

notIdem [in LblStr]
notTotal [in LblStr]

P

papply [in LblStr]
Prd [in LblStr]
prjl [in LblStr]
prjr [in LblStr]
prod [in LblStr]
p_prod [in LblStr]
p_sum [in LblStr]

R

Restr [in LblStr]
Rprod [in LblStr]
Rsum [in LblStr]
r_id [in LblStr]

S

sem [in LblStr]
Sprod [in LblStr]
std_sem [in LblStr]
SUPERPOSITION.isMax_inl [in LblStr]
SUPERPOSITION.isMono [in LblStr]
SUPERPOSITION.isMono_extr [in LblStr]
SUPERPOSITION.isMono_inl [in LblStr]
SUPERPOSITION.spsem [in LblStr]
SUPERPOSITION.std_spsem [in LblStr]
SUPERPOSITION2.isMono_sr_inl [in LblStr]
SUPERPOSITION2.isMono_inl [in LblStr]
SUPERPOSITION2.isRecv_inl [in LblStr]
SUPERPOSITION2.spsem [in LblStr]
SUPERPOSITION2.std_spsem [in LblStr]

T

TA [in LblStr]
tfr_nopt [in LblStr]
tfr_opt [in LblStr]
tfr_nrcv [in LblStr]
tfr_rcv [in LblStr]
tfr_nsnd [in LblStr]
tfr_snd [in LblStr]
TIME [in LblStr]
Transfo [in LblStr]
tr_prod [in LblStr]
tr_sum [in LblStr]
tr_id [in LblStr]
tr_extr [in LblStr]
tr_extl [in LblStr]
tr_outr [in LblStr]
tr_outl [in LblStr]
tr_inr [in LblStr]
tr_inl [in LblStr]
tr_comp [in LblStr]
ttrans [in LblStr]

U

union [in LblStr]
UNIV [in LblStr]

---

Record Index

A

assoc_hyp [in LblStr]
Atl4 [in LblStr]

B

bisim [in LblStr]

E

e_stable [in LblStr]

I

isACI [in LblStr]
isAssoc [in LblStr]
isComm [in LblStr]
isStratified [in LblStr]

L

LblStr [in LblStr]
LTS [in LblStr]

M

M_BASIC_ELEMS.action [in LblStr]
M_ACTION.CkLabel [in LblStr]

R

refines [in LblStr]

S

stable [in LblStr]

T

transfo [in LblStr]

U

Unit [in LblStr]

---

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

(579 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

(31 entries)

Module 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

(8 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

(1 entry)

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

(241 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

(15 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

(26 entries)

Projection 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

(75 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

(15 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

(1 entry)

Instance 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)

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

(148 entries)

Record 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

(16 entries)

---

This page has been generated by coqdoc