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 (410 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 (11 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 (31 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 (12 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 (160 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 (65 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 (21 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 (10 entries)
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 (49 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 (11 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 (40 entries)

Global Index

A

AB [lemma, in Companion.ccs_rep_bisim]
accumulate [lemma, in Companion.companion_param]
Act [constructor, in Companion.ccs_rep_lang]
act [inductive, in Companion.ccs_rep_lang]
Act [constructor, in Companion.ccs_mu_syn]
act [inductive, in Companion.ccs_mu_syn]
ActRecv [constructor, in Companion.ccs_rep_lang]
ActRecv [constructor, in Companion.ccs_mu_syn]
ActSend [constructor, in Companion.ccs_rep_lang]
ActSend [constructor, in Companion.ccs_mu_syn]
ActTau [constructor, in Companion.ccs_rep_lang]
ActTau [constructor, in Companion.ccs_mu_syn]
act_proper_l [instance, in Companion.ccs_mu_bisim]
act_proper [instance, in Companion.ccs_mu_bisim]
act_proper_l [instance, in Companion.ccs_rep_bisim]
act_proper [instance, in Companion.ccs_rep_bisim]
asimpl [definition, in Companion.ccs_mu_syn]


B

bisim [abbreviation, in Companion.ccs_mu_bisim]
Bisim [abbreviation, in Companion.ccs_mu_bisim]
bisim [abbreviation, in Companion.ccs_rep_bisim]
Bisim [abbreviation, in Companion.ccs_rep_bisim]
bisim_equiv [instance, in Companion.ccs_mu_bisim]
bisim_upto [lemma, in Companion.ccs_mu_bisim]
bisim_trans [instance, in Companion.ccs_mu_bisim]
bisim_sym [instance, in Companion.ccs_mu_bisim]
bisim_refl [instance, in Companion.ccs_mu_bisim]
bisim_rewrite [instance, in Companion.ccs_mu_bisim]
bisim_left [lemma, in Companion.ccs_mu_bisim]
bisim_bisim [lemma, in Companion.ccs_mu_bisim]
bisim_unfold [lemma, in Companion.ccs_mu_bisim]
bisim_fold [lemma, in Companion.ccs_mu_bisim]
Bisim_mono [instance, in Companion.ccs_mu_bisim]
bisim_equiv [instance, in Companion.ccs_rep_bisim]
bisim_upto [lemma, in Companion.ccs_rep_bisim]
bisim_trans [instance, in Companion.ccs_rep_bisim]
bisim_sym [instance, in Companion.ccs_rep_bisim]
bisim_refl [instance, in Companion.ccs_rep_bisim]
bisim_rewrite [instance, in Companion.ccs_rep_bisim]
bisim_left [lemma, in Companion.ccs_rep_bisim]
bisim_bisim [lemma, in Companion.ccs_rep_bisim]
bisim_unfold [lemma, in Companion.ccs_rep_bisim]
bisim_fold [lemma, in Companion.ccs_rep_bisim]
bisim_coind [lemma, in Companion.ccs_rep_bisim]
Bisim_mono [instance, in Companion.ccs_rep_bisim]


C

C [inductive, in Companion.companion_sound]
CAct [constructor, in Companion.ccs_mu_bisim]
cAct [inductive, in Companion.ccs_mu_bisim]
CAct [constructor, in Companion.ccs_rep_bisim]
cAct [inductive, in Companion.ccs_rep_bisim]
cAct_step [lemma, in Companion.ccs_mu_bisim]
cAct_step [lemma, in Companion.ccs_rep_bisim]
ccs_rep_bisim [library]
ccs_rep_lang [library]
ccs_mu_sem [library]
ccs_mu_syn [library]
ccs_mu_bisim [library]
cexp [definition, in Companion.ccs_mu_sem]
CFix [constructor, in Companion.ccs_mu_bisim]
cFix [inductive, in Companion.ccs_mu_bisim]
cFix_symmetric [lemma, in Companion.ccs_mu_bisim]
cFix_mono [instance, in Companion.ccs_mu_bisim]
CNew [constructor, in Companion.ccs_mu_bisim]
cNew [inductive, in Companion.ccs_mu_bisim]
CNew [constructor, in Companion.ccs_rep_bisim]
cNew [inductive, in Companion.ccs_rep_bisim]
cNew_symmetric [lemma, in Companion.ccs_mu_bisim]
cNew_mono [instance, in Companion.ccs_mu_bisim]
cNew_symmetric [lemma, in Companion.ccs_rep_bisim]
cNew_mono [instance, in Companion.ccs_rep_bisim]
Companion [section, in Companion.companion]
companion [library]
companion_rel [library]
companion_param [library]
companion_sound [library]
companion_mu [library]
Companion.A [variable, in Companion.companion]
Companion.f [variable, in Companion.companion]
Companion.fP [variable, in Companion.companion]
Companion.UptoLemma [section, in Companion.companion]
Companion.UptoLemma.g [variable, in Companion.companion]
Companion.UptoLemma.gP [variable, in Companion.companion]
compatible [definition, in Companion.companion]
compat_below [lemma, in Companion.companion]
CPar [constructor, in Companion.ccs_mu_bisim]
cPar [inductive, in Companion.ccs_mu_bisim]
CPar [constructor, in Companion.ccs_rep_bisim]
cPar [inductive, in Companion.ccs_rep_bisim]
cPar_symmetric [lemma, in Companion.ccs_mu_bisim]
cPar_mono [instance, in Companion.ccs_mu_bisim]
cPar_symmetric [lemma, in Companion.ccs_rep_bisim]
cPar_mono [instance, in Companion.ccs_rep_bisim]
CRep [constructor, in Companion.ccs_rep_bisim]
cRep [inductive, in Companion.ccs_rep_bisim]
cRep_symmetric [lemma, in Companion.ccs_rep_bisim]
cRep_mono [instance, in Companion.ccs_rep_bisim]
CSubst [constructor, in Companion.ccs_mu_bisim]
cSubst [inductive, in Companion.ccs_mu_bisim]
cSubst_symmetric [lemma, in Companion.ccs_mu_bisim]
cSubst_mono [instance, in Companion.ccs_mu_bisim]
CSum [constructor, in Companion.ccs_mu_bisim]
cSum [inductive, in Companion.ccs_mu_bisim]
CSum [constructor, in Companion.ccs_rep_bisim]
cSum [inductive, in Companion.ccs_rep_bisim]
cSum_symmetric [lemma, in Companion.ccs_mu_bisim]
cSum_mono [instance, in Companion.ccs_mu_bisim]
cSum_symmetric [lemma, in Companion.ccs_rep_bisim]
cSum_mono [instance, in Companion.ccs_rep_bisim]
ctx [inductive, in Companion.ccs_rep_bisim]
C_sound [lemma, in Companion.companion_sound]
C_ctx [constructor, in Companion.companion_sound]
C_trans [constructor, in Companion.companion_sound]
C_sym [constructor, in Companion.companion_sound]
C_bisim [constructor, in Companion.companion_sound]
C_R [constructor, in Companion.companion_sound]


D

dual [definition, in Companion.ccs_rep_lang]
dual [definition, in Companion.ccs_mu_sem]


E

Equiv [section, in Companion.companion_rel]
Equiv.f [variable, in Companion.companion_rel]
Equiv.X [variable, in Companion.companion_rel]
Example [section, in Companion.ccs_rep_bisim]
Example.A [variable, in Companion.ccs_rep_bisim]
Example.ai [variable, in Companion.ccs_rep_bisim]
Example.ao [variable, in Companion.ccs_rep_bisim]
Example.A_def [variable, in Companion.ccs_rep_bisim]
Example.B [variable, in Companion.ccs_rep_bisim]
Example.B_def [variable, in Companion.ccs_rep_bisim]
exp [inductive, in Companion.ccs_rep_lang]
exp [inductive, in Companion.ccs_mu_syn]


F

Fbisim [definition, in Companion.ccs_mu_bisim]
Fbisim [definition, in Companion.ccs_rep_bisim]
Fbisim_mono [instance, in Companion.ccs_mu_bisim]
Fbisim_mono [instance, in Companion.ccs_rep_bisim]
ffstep_step [lemma, in Companion.ccs_mu_sem]
fill [definition, in Companion.ccs_rep_bisim]
fill_proper [lemma, in Companion.ccs_rep_bisim]
fin [library]
Fix [constructor, in Companion.ccs_mu_syn]
fix_proper [instance, in Companion.ccs_mu_bisim]
flip [definition, in Companion.companion_rel]
flip_symmetric [lemma, in Companion.companion_rel]
freflexive [definition, in Companion.companion_rel]
freflexive_sceil [lemma, in Companion.companion_rel]
Fsim [definition, in Companion.ccs_mu_bisim]
Fsim [definition, in Companion.ccs_rep_bisim]
Fsim_mono [instance, in Companion.ccs_mu_bisim]
Fsim_mono [instance, in Companion.ccs_rep_bisim]
Fstep [inductive, in Companion.ccs_rep_lang]
Fstep [inductive, in Companion.ccs_mu_sem]
fstep_step [lemma, in Companion.ccs_rep_lang]
Fstep_mono [instance, in Companion.ccs_rep_lang]
Fstep_restrict [constructor, in Companion.ccs_rep_lang]
Fstep_rep [constructor, in Companion.ccs_rep_lang]
Fstep_comm [constructor, in Companion.ccs_rep_lang]
Fstep_parr [constructor, in Companion.ccs_rep_lang]
Fstep_parl [constructor, in Companion.ccs_rep_lang]
Fstep_sumr [constructor, in Companion.ccs_rep_lang]
Fstep_suml [constructor, in Companion.ccs_rep_lang]
Fstep_act [constructor, in Companion.ccs_rep_lang]
fstep_step [lemma, in Companion.ccs_mu_sem]
Fstep_mono [instance, in Companion.ccs_mu_sem]
Fstep_fix [constructor, in Companion.ccs_mu_sem]
Fstep_restrict [constructor, in Companion.ccs_mu_sem]
Fstep_comm [constructor, in Companion.ccs_mu_sem]
Fstep_parr [constructor, in Companion.ccs_mu_sem]
Fstep_parl [constructor, in Companion.ccs_mu_sem]
Fstep_sumr [constructor, in Companion.ccs_mu_sem]
Fstep_suml [constructor, in Companion.ccs_mu_sem]
Fstep_act [constructor, in Companion.ccs_mu_sem]
fsymmetric [definition, in Companion.companion_rel]
fsymmetric_sceil [lemma, in Companion.companion_rel]
ftransitive [definition, in Companion.companion_rel]
ftransitive_sceil [lemma, in Companion.companion_rel]


G

GAct [constructor, in Companion.ccs_rep_bisim]
gctx [inductive, in Companion.ccs_rep_bisim]
GExp [constructor, in Companion.ccs_rep_bisim]
gfill [definition, in Companion.ccs_rep_bisim]
gfill_proper [lemma, in Companion.ccs_rep_bisim]
GNew [constructor, in Companion.ccs_rep_bisim]
GPar [constructor, in Companion.ccs_rep_bisim]
GRep [constructor, in Companion.ccs_rep_bisim]
GSum [constructor, in Companion.ccs_rep_bisim]
guard [definition, in Companion.ccs_rep_lang]
guard [definition, in Companion.ccs_mu_sem]


I

ids [definition, in Companion.ccs_mu_syn]
id_rcomp [lemma, in Companion.ccs_mu_syn]
id_inst [lemma, in Companion.ccs_mu_syn]
ind [lemma, in Companion.companion_mu]
ind_upto_char [lemma, in Companion.companion_mu]
ind_upto_above [lemma, in Companion.companion_mu]
ind_upto [lemma, in Companion.companion_mu]
inf_closed_mono [lemma, in Companion.companion]
inf_closed_le [lemma, in Companion.companion]
inf_closed [definition, in Companion.companion]
inst_id [lemma, in Companion.ccs_mu_syn]


L

l [definition, in Companion.companion_mu]
lts [definition, in Companion.ccs_rep_lang]
lts [definition, in Companion.ccs_mu_sem]
l_unfold [lemma, in Companion.companion_mu]
l_f [lemma, in Companion.companion_mu]
l_idem [lemma, in Companion.companion_mu]
l_dec [lemma, in Companion.companion_mu]
l_monotone [instance, in Companion.companion_mu]
l_kernel [instance, in Companion.companion_mu]


M

map_subst [lemma, in Companion.ccs_mu_syn]
mu [definition, in Companion.companion_mu]
mu_l [lemma, in Companion.companion_mu]
mu_fp [lemma, in Companion.companion_mu]
mu_tarski [lemma, in Companion.companion_mu]


N

New [constructor, in Companion.ccs_rep_lang]
New [constructor, in Companion.ccs_mu_syn]
new_proper [instance, in Companion.ccs_mu_bisim]
new_proper [instance, in Companion.ccs_rep_bisim]
nu [definition, in Companion.prelim]
Null [constructor, in Companion.ccs_rep_lang]
nu_t [lemma, in Companion.companion]
nu_coind_t [lemma, in Companion.companion_param]
nu_fp [lemma, in Companion.prelim]
nu_prefix [lemma, in Companion.prelim]
nu_postfix [lemma, in Companion.prelim]
nu_tarski [lemma, in Companion.prelim]


O

obisim [abbreviation, in Companion.ccs_mu_bisim]
OBisim [definition, in Companion.ccs_mu_bisim]
obisim_trans [instance, in Companion.ccs_mu_bisim]
obisim_sym [instance, in Companion.ccs_mu_bisim]
obisim_refl [instance, in Companion.ccs_mu_bisim]
obisim_coind [lemma, in Companion.ccs_mu_bisim]
observable [definition, in Companion.ccs_rep_lang]
observable [definition, in Companion.ccs_mu_sem]
ord_inv [lemma, in Companion.fin]


P

Par [constructor, in Companion.ccs_rep_lang]
Par [constructor, in Companion.ccs_mu_syn]
ParameterizedCoinduction [section, in Companion.companion_param]
ParameterizedCoinduction.A [variable, in Companion.companion_param]
ParameterizedCoinduction.f [variable, in Companion.companion_param]
ParameterizedCoinduction.fP [variable, in Companion.companion_param]
param_tower_ind_s [lemma, in Companion.companion_param]
param_tower_ind [lemma, in Companion.companion_param]
parC [lemma, in Companion.ccs_rep_bisim]
par_proper [instance, in Companion.ccs_mu_bisim]
par_proper [instance, in Companion.ccs_rep_bisim]
prelim [library]


R

rbind [definition, in Companion.ccs_mu_syn]
rbindA [lemma, in Companion.ccs_mu_syn]
rbind_rmap_comp [lemma, in Companion.ccs_mu_syn]
rbisim_fold_subrel [instance, in Companion.ccs_rep_bisim]
rbisim_subrel [instance, in Companion.ccs_rep_bisim]
rcomp [definition, in Companion.ccs_mu_syn]
rcompA [lemma, in Companion.ccs_mu_syn]
rcomp_id [lemma, in Companion.ccs_mu_syn]
ren [abbreviation, in Companion.ccs_mu_syn]
Rep [constructor, in Companion.ccs_rep_lang]
rep_proper [instance, in Companion.ccs_rep_bisim]
rmap [definition, in Companion.ccs_mu_syn]
rmap_rbind_comp [lemma, in Companion.ccs_mu_syn]
rmap_comp [lemma, in Companion.ccs_mu_syn]
r_bisim [lemma, in Companion.ccs_rep_bisim]


S

S [definition, in Companion.fin]
sceil [definition, in Companion.companion_rel]
sceil_pre [lemma, in Companion.companion_rel]
sceil_mono [instance, in Companion.companion_rel]
scons [definition, in Companion.fin]
sconsS [lemma, in Companion.fin]
scons_scomp [lemma, in Companion.ccs_mu_syn]
scons_simpl [definition, in Companion.fin]
scons_eq [lemma, in Companion.fin]
scons_eta [lemma, in Companion.fin]
scons0 [lemma, in Companion.fin]
shift_scons [lemma, in Companion.ccs_mu_syn]
sound [definition, in Companion.companion_sound]
Soundndess [section, in Companion.companion_sound]
Soundndess.A [variable, in Companion.companion_sound]
Soundndess.f [variable, in Companion.companion_sound]
Soundndess.fP [variable, in Companion.companion_sound]
sound_t [lemma, in Companion.companion_sound]
step [abbreviation, in Companion.ccs_rep_lang]
Step [abbreviation, in Companion.ccs_rep_lang]
step [abbreviation, in Companion.ccs_mu_sem]
Step [abbreviation, in Companion.ccs_mu_sem]
step_rep_ind [lemma, in Companion.ccs_rep_lang]
step_new_inv [lemma, in Companion.ccs_rep_lang]
step_rep_inv [lemma, in Companion.ccs_rep_lang]
step_par_inv [lemma, in Companion.ccs_rep_lang]
step_sum_inv [lemma, in Companion.ccs_rep_lang]
step_act_inv [lemma, in Companion.ccs_rep_lang]
step_new [lemma, in Companion.ccs_rep_lang]
step_rep [lemma, in Companion.ccs_rep_lang]
step_comm [lemma, in Companion.ccs_rep_lang]
step_parr [lemma, in Companion.ccs_rep_lang]
step_parl [lemma, in Companion.ccs_rep_lang]
step_sumr [lemma, in Companion.ccs_rep_lang]
step_suml [lemma, in Companion.ccs_rep_lang]
step_act [lemma, in Companion.ccs_rep_lang]
step_fold [lemma, in Companion.ccs_rep_lang]
step_unfold [lemma, in Companion.ccs_rep_lang]
step_subst_sim [lemma, in Companion.ccs_mu_bisim]
step_fix_inv [lemma, in Companion.ccs_mu_sem]
step_new_inv [lemma, in Companion.ccs_mu_sem]
step_par_inv [lemma, in Companion.ccs_mu_sem]
step_sum_inv [lemma, in Companion.ccs_mu_sem]
step_act_inv [lemma, in Companion.ccs_mu_sem]
step_fix [lemma, in Companion.ccs_mu_sem]
step_new [lemma, in Companion.ccs_mu_sem]
step_comm [lemma, in Companion.ccs_mu_sem]
step_parr [lemma, in Companion.ccs_mu_sem]
step_parl [lemma, in Companion.ccs_mu_sem]
step_sumr [lemma, in Companion.ccs_mu_sem]
step_suml [lemma, in Companion.ccs_mu_sem]
step_act [lemma, in Companion.ccs_mu_sem]
step_fold [lemma, in Companion.ccs_mu_sem]
step_unfold [lemma, in Companion.ccs_mu_sem]
subst_up [lemma, in Companion.ccs_mu_syn]
subst_extend [lemma, in Companion.ccs_mu_syn]
Sum [constructor, in Companion.ccs_rep_lang]
Sum [constructor, in Companion.ccs_mu_syn]
sum_proper [instance, in Companion.ccs_mu_bisim]
sum_proper [instance, in Companion.ccs_rep_bisim]
sup_closed [definition, in Companion.companion_mu]
symmetric [definition, in Companion.companion_rel]
symmetric_t_sceil [lemma, in Companion.companion_rel]


T

t [definition, in Companion.companion]
T [inductive, in Companion.companion]
t [abbreviation, in Companion.companion_param]
TAct [constructor, in Companion.ccs_rep_bisim]
Tarski [section, in Companion.prelim]
TarskiMu [section, in Companion.companion_mu]
TarskiMu.A [variable, in Companion.companion_mu]
TarskiMu.B [variable, in Companion.companion_mu]
TarskiMu.f [variable, in Companion.companion_mu]
TarskiMu.fP [variable, in Companion.companion_mu]
Tarski.A [variable, in Companion.prelim]
Tarski.f [variable, in Companion.prelim]
Tarski.fP [variable, in Companion.prelim]
TExp [constructor, in Companion.ccs_rep_bisim]
THole [constructor, in Companion.ccs_rep_bisim]
TNew [constructor, in Companion.ccs_rep_bisim]
TowerMu [section, in Companion.companion_mu]
TowerMu.A [variable, in Companion.companion_mu]
TowerMu.B [variable, in Companion.companion_mu]
TowerMu.f [variable, in Companion.companion_mu]
TowerMu.UptoLemma [section, in Companion.companion_mu]
TowerMu.UptoLemma.g [variable, in Companion.companion_mu]
TowerMu.UptoLemma.gP [variable, in Companion.companion_mu]
tower_ind [lemma, in Companion.companion]
TPar [constructor, in Companion.ccs_rep_bisim]
TRep [constructor, in Companion.ccs_rep_bisim]
TSum [constructor, in Companion.ccs_rep_bisim]
t_greatest_compatible [lemma, in Companion.companion]
t_compat [lemma, in Companion.companion]
t_fold [lemma, in Companion.companion]
t_f [lemma, in Companion.companion]
t_img [lemma, in Companion.companion]
t_idem [lemma, in Companion.companion]
t_inc [lemma, in Companion.companion]
t_monotone [instance, in Companion.companion]
t_closure [instance, in Companion.companion]
T_t [lemma, in Companion.companion]
T_lim [constructor, in Companion.companion]
T_step [constructor, in Companion.companion]
t_trans [lemma, in Companion.companion_rel]
t_sym [lemma, in Companion.companion_rel]
t_refl [lemma, in Companion.companion_rel]


U

unique_solutions [lemma, in Companion.ccs_rep_bisim]
up [definition, in Companion.ccs_mu_syn]
upE [lemma, in Companion.ccs_mu_syn]
upr [definition, in Companion.ccs_mu_syn]
upr_up [lemma, in Companion.ccs_mu_syn]
upto [lemma, in Companion.companion]
upto_char [lemma, in Companion.companion]
upto_below [lemma, in Companion.companion]
upto_inst [lemma, in Companion.ccs_mu_bisim]
upto_fix [lemma, in Companion.ccs_mu_bisim]
upto_fix' [lemma, in Companion.ccs_mu_bisim]
upto_beta [lemma, in Companion.ccs_mu_bisim]
upto_inst_w [lemma, in Companion.ccs_mu_bisim]
upto_inst' [lemma, in Companion.ccs_mu_bisim]
upto_new [lemma, in Companion.ccs_mu_bisim]
upto_new' [lemma, in Companion.ccs_mu_bisim]
upto_par [lemma, in Companion.ccs_mu_bisim]
upto_par' [lemma, in Companion.ccs_mu_bisim]
upto_sum [lemma, in Companion.ccs_mu_bisim]
upto_sum' [lemma, in Companion.ccs_mu_bisim]
upto_act [lemma, in Companion.ccs_mu_bisim]
upto_act_s [lemma, in Companion.ccs_mu_bisim]
upto_sound [lemma, in Companion.companion_sound]
upto_rep [lemma, in Companion.ccs_rep_bisim]
upto_rep' [lemma, in Companion.ccs_rep_bisim]
upto_new [lemma, in Companion.ccs_rep_bisim]
upto_new' [lemma, in Companion.ccs_rep_bisim]
upto_par [lemma, in Companion.ccs_rep_bisim]
upto_par' [lemma, in Companion.ccs_rep_bisim]
upto_sum [lemma, in Companion.ccs_rep_bisim]
upto_sum' [lemma, in Companion.ccs_rep_bisim]
upto_act [lemma, in Companion.ccs_rep_bisim]
upto_act_s [lemma, in Companion.ccs_rep_bisim]
up_comp [lemma, in Companion.ccs_mu_syn]
up_upr [lemma, in Companion.ccs_mu_syn]
up_ren [lemma, in Companion.ccs_mu_syn]
up_id [lemma, in Companion.ccs_mu_syn]


V

Var [constructor, in Companion.ccs_mu_syn]


other

○ _ (type_scope) [notation, in Companion.ccs_mu_bisim]
○ _ (type_scope) [notation, in Companion.ccs_rep_bisim]
_ ~~ _ [notation, in Companion.ccs_mu_bisim]
_ |- _ ~ _ [notation, in Companion.ccs_mu_bisim]
_ .[ _ /] [notation, in Companion.ccs_mu_syn]
_ .[ _ ] [notation, in Companion.ccs_mu_syn]
_ >> _ [notation, in Companion.ccs_mu_syn]
_ .: _ [notation, in Companion.fin]
_ ~~ _ [notation, in Companion.ccs_rep_bisim]
_ |- _ ~ _ [notation, in Companion.ccs_rep_bisim]
0 [notation, in Companion.fin]



Notation Index

other

○ _ (type_scope) [in Companion.ccs_mu_bisim]
○ _ (type_scope) [in Companion.ccs_rep_bisim]
_ ~~ _ [in Companion.ccs_mu_bisim]
_ |- _ ~ _ [in Companion.ccs_mu_bisim]
_ .[ _ /] [in Companion.ccs_mu_syn]
_ .[ _ ] [in Companion.ccs_mu_syn]
_ >> _ [in Companion.ccs_mu_syn]
_ .: _ [in Companion.fin]
_ ~~ _ [in Companion.ccs_rep_bisim]
_ |- _ ~ _ [in Companion.ccs_rep_bisim]
0 [in Companion.fin]



Variable Index

C

Companion.A [in Companion.companion]
Companion.f [in Companion.companion]
Companion.fP [in Companion.companion]
Companion.UptoLemma.g [in Companion.companion]
Companion.UptoLemma.gP [in Companion.companion]


E

Equiv.f [in Companion.companion_rel]
Equiv.X [in Companion.companion_rel]
Example.A [in Companion.ccs_rep_bisim]
Example.ai [in Companion.ccs_rep_bisim]
Example.ao [in Companion.ccs_rep_bisim]
Example.A_def [in Companion.ccs_rep_bisim]
Example.B [in Companion.ccs_rep_bisim]
Example.B_def [in Companion.ccs_rep_bisim]


P

ParameterizedCoinduction.A [in Companion.companion_param]
ParameterizedCoinduction.f [in Companion.companion_param]
ParameterizedCoinduction.fP [in Companion.companion_param]


S

Soundndess.A [in Companion.companion_sound]
Soundndess.f [in Companion.companion_sound]
Soundndess.fP [in Companion.companion_sound]


T

TarskiMu.A [in Companion.companion_mu]
TarskiMu.B [in Companion.companion_mu]
TarskiMu.f [in Companion.companion_mu]
TarskiMu.fP [in Companion.companion_mu]
Tarski.A [in Companion.prelim]
Tarski.f [in Companion.prelim]
Tarski.fP [in Companion.prelim]
TowerMu.A [in Companion.companion_mu]
TowerMu.B [in Companion.companion_mu]
TowerMu.f [in Companion.companion_mu]
TowerMu.UptoLemma.g [in Companion.companion_mu]
TowerMu.UptoLemma.gP [in Companion.companion_mu]



Library Index

C

ccs_rep_bisim
ccs_rep_lang
ccs_mu_sem
ccs_mu_syn
ccs_mu_bisim
companion
companion_rel
companion_param
companion_sound
companion_mu


F

fin


P

prelim



Lemma Index

A

AB [in Companion.ccs_rep_bisim]
accumulate [in Companion.companion_param]


B

bisim_upto [in Companion.ccs_mu_bisim]
bisim_left [in Companion.ccs_mu_bisim]
bisim_bisim [in Companion.ccs_mu_bisim]
bisim_unfold [in Companion.ccs_mu_bisim]
bisim_fold [in Companion.ccs_mu_bisim]
bisim_upto [in Companion.ccs_rep_bisim]
bisim_left [in Companion.ccs_rep_bisim]
bisim_bisim [in Companion.ccs_rep_bisim]
bisim_unfold [in Companion.ccs_rep_bisim]
bisim_fold [in Companion.ccs_rep_bisim]
bisim_coind [in Companion.ccs_rep_bisim]


C

cAct_step [in Companion.ccs_mu_bisim]
cAct_step [in Companion.ccs_rep_bisim]
cFix_symmetric [in Companion.ccs_mu_bisim]
cNew_symmetric [in Companion.ccs_mu_bisim]
cNew_symmetric [in Companion.ccs_rep_bisim]
compat_below [in Companion.companion]
cPar_symmetric [in Companion.ccs_mu_bisim]
cPar_symmetric [in Companion.ccs_rep_bisim]
cRep_symmetric [in Companion.ccs_rep_bisim]
cSubst_symmetric [in Companion.ccs_mu_bisim]
cSum_symmetric [in Companion.ccs_mu_bisim]
cSum_symmetric [in Companion.ccs_rep_bisim]
C_sound [in Companion.companion_sound]


F

ffstep_step [in Companion.ccs_mu_sem]
fill_proper [in Companion.ccs_rep_bisim]
flip_symmetric [in Companion.companion_rel]
freflexive_sceil [in Companion.companion_rel]
fstep_step [in Companion.ccs_rep_lang]
fstep_step [in Companion.ccs_mu_sem]
fsymmetric_sceil [in Companion.companion_rel]
ftransitive_sceil [in Companion.companion_rel]


G

gfill_proper [in Companion.ccs_rep_bisim]


I

id_rcomp [in Companion.ccs_mu_syn]
id_inst [in Companion.ccs_mu_syn]
ind [in Companion.companion_mu]
ind_upto_char [in Companion.companion_mu]
ind_upto_above [in Companion.companion_mu]
ind_upto [in Companion.companion_mu]
inf_closed_mono [in Companion.companion]
inf_closed_le [in Companion.companion]
inst_id [in Companion.ccs_mu_syn]


L

l_unfold [in Companion.companion_mu]
l_f [in Companion.companion_mu]
l_idem [in Companion.companion_mu]
l_dec [in Companion.companion_mu]


M

map_subst [in Companion.ccs_mu_syn]
mu_l [in Companion.companion_mu]
mu_fp [in Companion.companion_mu]
mu_tarski [in Companion.companion_mu]


N

nu_t [in Companion.companion]
nu_coind_t [in Companion.companion_param]
nu_fp [in Companion.prelim]
nu_prefix [in Companion.prelim]
nu_postfix [in Companion.prelim]
nu_tarski [in Companion.prelim]


O

obisim_coind [in Companion.ccs_mu_bisim]
ord_inv [in Companion.fin]


P

param_tower_ind_s [in Companion.companion_param]
param_tower_ind [in Companion.companion_param]
parC [in Companion.ccs_rep_bisim]


R

rbindA [in Companion.ccs_mu_syn]
rbind_rmap_comp [in Companion.ccs_mu_syn]
rcompA [in Companion.ccs_mu_syn]
rcomp_id [in Companion.ccs_mu_syn]
rmap_rbind_comp [in Companion.ccs_mu_syn]
rmap_comp [in Companion.ccs_mu_syn]
r_bisim [in Companion.ccs_rep_bisim]


S

sceil_pre [in Companion.companion_rel]
sconsS [in Companion.fin]
scons_scomp [in Companion.ccs_mu_syn]
scons_eq [in Companion.fin]
scons_eta [in Companion.fin]
scons0 [in Companion.fin]
shift_scons [in Companion.ccs_mu_syn]
sound_t [in Companion.companion_sound]
step_rep_ind [in Companion.ccs_rep_lang]
step_new_inv [in Companion.ccs_rep_lang]
step_rep_inv [in Companion.ccs_rep_lang]
step_par_inv [in Companion.ccs_rep_lang]
step_sum_inv [in Companion.ccs_rep_lang]
step_act_inv [in Companion.ccs_rep_lang]
step_new [in Companion.ccs_rep_lang]
step_rep [in Companion.ccs_rep_lang]
step_comm [in Companion.ccs_rep_lang]
step_parr [in Companion.ccs_rep_lang]
step_parl [in Companion.ccs_rep_lang]
step_sumr [in Companion.ccs_rep_lang]
step_suml [in Companion.ccs_rep_lang]
step_act [in Companion.ccs_rep_lang]
step_fold [in Companion.ccs_rep_lang]
step_unfold [in Companion.ccs_rep_lang]
step_subst_sim [in Companion.ccs_mu_bisim]
step_fix_inv [in Companion.ccs_mu_sem]
step_new_inv [in Companion.ccs_mu_sem]
step_par_inv [in Companion.ccs_mu_sem]
step_sum_inv [in Companion.ccs_mu_sem]
step_act_inv [in Companion.ccs_mu_sem]
step_fix [in Companion.ccs_mu_sem]
step_new [in Companion.ccs_mu_sem]
step_comm [in Companion.ccs_mu_sem]
step_parr [in Companion.ccs_mu_sem]
step_parl [in Companion.ccs_mu_sem]
step_sumr [in Companion.ccs_mu_sem]
step_suml [in Companion.ccs_mu_sem]
step_act [in Companion.ccs_mu_sem]
step_fold [in Companion.ccs_mu_sem]
step_unfold [in Companion.ccs_mu_sem]
subst_up [in Companion.ccs_mu_syn]
subst_extend [in Companion.ccs_mu_syn]
symmetric_t_sceil [in Companion.companion_rel]


T

tower_ind [in Companion.companion]
t_greatest_compatible [in Companion.companion]
t_compat [in Companion.companion]
t_fold [in Companion.companion]
t_f [in Companion.companion]
t_img [in Companion.companion]
t_idem [in Companion.companion]
t_inc [in Companion.companion]
T_t [in Companion.companion]
t_trans [in Companion.companion_rel]
t_sym [in Companion.companion_rel]
t_refl [in Companion.companion_rel]


U

unique_solutions [in Companion.ccs_rep_bisim]
upE [in Companion.ccs_mu_syn]
upr_up [in Companion.ccs_mu_syn]
upto [in Companion.companion]
upto_char [in Companion.companion]
upto_below [in Companion.companion]
upto_inst [in Companion.ccs_mu_bisim]
upto_fix [in Companion.ccs_mu_bisim]
upto_fix' [in Companion.ccs_mu_bisim]
upto_beta [in Companion.ccs_mu_bisim]
upto_inst_w [in Companion.ccs_mu_bisim]
upto_inst' [in Companion.ccs_mu_bisim]
upto_new [in Companion.ccs_mu_bisim]
upto_new' [in Companion.ccs_mu_bisim]
upto_par [in Companion.ccs_mu_bisim]
upto_par' [in Companion.ccs_mu_bisim]
upto_sum [in Companion.ccs_mu_bisim]
upto_sum' [in Companion.ccs_mu_bisim]
upto_act [in Companion.ccs_mu_bisim]
upto_act_s [in Companion.ccs_mu_bisim]
upto_sound [in Companion.companion_sound]
upto_rep [in Companion.ccs_rep_bisim]
upto_rep' [in Companion.ccs_rep_bisim]
upto_new [in Companion.ccs_rep_bisim]
upto_new' [in Companion.ccs_rep_bisim]
upto_par [in Companion.ccs_rep_bisim]
upto_par' [in Companion.ccs_rep_bisim]
upto_sum [in Companion.ccs_rep_bisim]
upto_sum' [in Companion.ccs_rep_bisim]
upto_act [in Companion.ccs_rep_bisim]
upto_act_s [in Companion.ccs_rep_bisim]
up_comp [in Companion.ccs_mu_syn]
up_upr [in Companion.ccs_mu_syn]
up_ren [in Companion.ccs_mu_syn]
up_id [in Companion.ccs_mu_syn]



Constructor Index

A

Act [in Companion.ccs_rep_lang]
Act [in Companion.ccs_mu_syn]
ActRecv [in Companion.ccs_rep_lang]
ActRecv [in Companion.ccs_mu_syn]
ActSend [in Companion.ccs_rep_lang]
ActSend [in Companion.ccs_mu_syn]
ActTau [in Companion.ccs_rep_lang]
ActTau [in Companion.ccs_mu_syn]


C

CAct [in Companion.ccs_mu_bisim]
CAct [in Companion.ccs_rep_bisim]
CFix [in Companion.ccs_mu_bisim]
CNew [in Companion.ccs_mu_bisim]
CNew [in Companion.ccs_rep_bisim]
CPar [in Companion.ccs_mu_bisim]
CPar [in Companion.ccs_rep_bisim]
CRep [in Companion.ccs_rep_bisim]
CSubst [in Companion.ccs_mu_bisim]
CSum [in Companion.ccs_mu_bisim]
CSum [in Companion.ccs_rep_bisim]
C_ctx [in Companion.companion_sound]
C_trans [in Companion.companion_sound]
C_sym [in Companion.companion_sound]
C_bisim [in Companion.companion_sound]
C_R [in Companion.companion_sound]


F

Fix [in Companion.ccs_mu_syn]
Fstep_restrict [in Companion.ccs_rep_lang]
Fstep_rep [in Companion.ccs_rep_lang]
Fstep_comm [in Companion.ccs_rep_lang]
Fstep_parr [in Companion.ccs_rep_lang]
Fstep_parl [in Companion.ccs_rep_lang]
Fstep_sumr [in Companion.ccs_rep_lang]
Fstep_suml [in Companion.ccs_rep_lang]
Fstep_act [in Companion.ccs_rep_lang]
Fstep_fix [in Companion.ccs_mu_sem]
Fstep_restrict [in Companion.ccs_mu_sem]
Fstep_comm [in Companion.ccs_mu_sem]
Fstep_parr [in Companion.ccs_mu_sem]
Fstep_parl [in Companion.ccs_mu_sem]
Fstep_sumr [in Companion.ccs_mu_sem]
Fstep_suml [in Companion.ccs_mu_sem]
Fstep_act [in Companion.ccs_mu_sem]


G

GAct [in Companion.ccs_rep_bisim]
GExp [in Companion.ccs_rep_bisim]
GNew [in Companion.ccs_rep_bisim]
GPar [in Companion.ccs_rep_bisim]
GRep [in Companion.ccs_rep_bisim]
GSum [in Companion.ccs_rep_bisim]


N

New [in Companion.ccs_rep_lang]
New [in Companion.ccs_mu_syn]
Null [in Companion.ccs_rep_lang]


P

Par [in Companion.ccs_rep_lang]
Par [in Companion.ccs_mu_syn]


R

Rep [in Companion.ccs_rep_lang]


S

Sum [in Companion.ccs_rep_lang]
Sum [in Companion.ccs_mu_syn]


T

TAct [in Companion.ccs_rep_bisim]
TExp [in Companion.ccs_rep_bisim]
THole [in Companion.ccs_rep_bisim]
TNew [in Companion.ccs_rep_bisim]
TPar [in Companion.ccs_rep_bisim]
TRep [in Companion.ccs_rep_bisim]
TSum [in Companion.ccs_rep_bisim]
T_lim [in Companion.companion]
T_step [in Companion.companion]


V

Var [in Companion.ccs_mu_syn]



Inductive Index

A

act [in Companion.ccs_rep_lang]
act [in Companion.ccs_mu_syn]


C

C [in Companion.companion_sound]
cAct [in Companion.ccs_mu_bisim]
cAct [in Companion.ccs_rep_bisim]
cFix [in Companion.ccs_mu_bisim]
cNew [in Companion.ccs_mu_bisim]
cNew [in Companion.ccs_rep_bisim]
cPar [in Companion.ccs_mu_bisim]
cPar [in Companion.ccs_rep_bisim]
cRep [in Companion.ccs_rep_bisim]
cSubst [in Companion.ccs_mu_bisim]
cSum [in Companion.ccs_mu_bisim]
cSum [in Companion.ccs_rep_bisim]
ctx [in Companion.ccs_rep_bisim]


E

exp [in Companion.ccs_rep_lang]
exp [in Companion.ccs_mu_syn]


F

Fstep [in Companion.ccs_rep_lang]
Fstep [in Companion.ccs_mu_sem]


G

gctx [in Companion.ccs_rep_bisim]


T

T [in Companion.companion]



Section Index

C

Companion [in Companion.companion]
Companion.UptoLemma [in Companion.companion]


E

Equiv [in Companion.companion_rel]
Example [in Companion.ccs_rep_bisim]


P

ParameterizedCoinduction [in Companion.companion_param]


S

Soundndess [in Companion.companion_sound]


T

Tarski [in Companion.prelim]
TarskiMu [in Companion.companion_mu]
TowerMu [in Companion.companion_mu]
TowerMu.UptoLemma [in Companion.companion_mu]



Instance Index

A

act_proper_l [in Companion.ccs_mu_bisim]
act_proper [in Companion.ccs_mu_bisim]
act_proper_l [in Companion.ccs_rep_bisim]
act_proper [in Companion.ccs_rep_bisim]


B

bisim_equiv [in Companion.ccs_mu_bisim]
bisim_trans [in Companion.ccs_mu_bisim]
bisim_sym [in Companion.ccs_mu_bisim]
bisim_refl [in Companion.ccs_mu_bisim]
bisim_rewrite [in Companion.ccs_mu_bisim]
Bisim_mono [in Companion.ccs_mu_bisim]
bisim_equiv [in Companion.ccs_rep_bisim]
bisim_trans [in Companion.ccs_rep_bisim]
bisim_sym [in Companion.ccs_rep_bisim]
bisim_refl [in Companion.ccs_rep_bisim]
bisim_rewrite [in Companion.ccs_rep_bisim]
Bisim_mono [in Companion.ccs_rep_bisim]


C

cFix_mono [in Companion.ccs_mu_bisim]
cNew_mono [in Companion.ccs_mu_bisim]
cNew_mono [in Companion.ccs_rep_bisim]
cPar_mono [in Companion.ccs_mu_bisim]
cPar_mono [in Companion.ccs_rep_bisim]
cRep_mono [in Companion.ccs_rep_bisim]
cSubst_mono [in Companion.ccs_mu_bisim]
cSum_mono [in Companion.ccs_mu_bisim]
cSum_mono [in Companion.ccs_rep_bisim]


F

Fbisim_mono [in Companion.ccs_mu_bisim]
Fbisim_mono [in Companion.ccs_rep_bisim]
fix_proper [in Companion.ccs_mu_bisim]
Fsim_mono [in Companion.ccs_mu_bisim]
Fsim_mono [in Companion.ccs_rep_bisim]
Fstep_mono [in Companion.ccs_rep_lang]
Fstep_mono [in Companion.ccs_mu_sem]


L

l_monotone [in Companion.companion_mu]
l_kernel [in Companion.companion_mu]


N

new_proper [in Companion.ccs_mu_bisim]
new_proper [in Companion.ccs_rep_bisim]


O

obisim_trans [in Companion.ccs_mu_bisim]
obisim_sym [in Companion.ccs_mu_bisim]
obisim_refl [in Companion.ccs_mu_bisim]


P

par_proper [in Companion.ccs_mu_bisim]
par_proper [in Companion.ccs_rep_bisim]


R

rbisim_fold_subrel [in Companion.ccs_rep_bisim]
rbisim_subrel [in Companion.ccs_rep_bisim]
rep_proper [in Companion.ccs_rep_bisim]


S

sceil_mono [in Companion.companion_rel]
sum_proper [in Companion.ccs_mu_bisim]
sum_proper [in Companion.ccs_rep_bisim]


T

t_monotone [in Companion.companion]
t_closure [in Companion.companion]



Abbreviation Index

B

bisim [in Companion.ccs_mu_bisim]
Bisim [in Companion.ccs_mu_bisim]
bisim [in Companion.ccs_rep_bisim]
Bisim [in Companion.ccs_rep_bisim]


O

obisim [in Companion.ccs_mu_bisim]


R

ren [in Companion.ccs_mu_syn]


S

step [in Companion.ccs_rep_lang]
Step [in Companion.ccs_rep_lang]
step [in Companion.ccs_mu_sem]
Step [in Companion.ccs_mu_sem]


T

t [in Companion.companion_param]



Definition Index

A

asimpl [in Companion.ccs_mu_syn]


C

cexp [in Companion.ccs_mu_sem]
compatible [in Companion.companion]


D

dual [in Companion.ccs_rep_lang]
dual [in Companion.ccs_mu_sem]


F

Fbisim [in Companion.ccs_mu_bisim]
Fbisim [in Companion.ccs_rep_bisim]
fill [in Companion.ccs_rep_bisim]
flip [in Companion.companion_rel]
freflexive [in Companion.companion_rel]
Fsim [in Companion.ccs_mu_bisim]
Fsim [in Companion.ccs_rep_bisim]
fsymmetric [in Companion.companion_rel]
ftransitive [in Companion.companion_rel]


G

gfill [in Companion.ccs_rep_bisim]
guard [in Companion.ccs_rep_lang]
guard [in Companion.ccs_mu_sem]


I

ids [in Companion.ccs_mu_syn]
inf_closed [in Companion.companion]


L

l [in Companion.companion_mu]
lts [in Companion.ccs_rep_lang]
lts [in Companion.ccs_mu_sem]


M

mu [in Companion.companion_mu]


N

nu [in Companion.prelim]


O

OBisim [in Companion.ccs_mu_bisim]
observable [in Companion.ccs_rep_lang]
observable [in Companion.ccs_mu_sem]


R

rbind [in Companion.ccs_mu_syn]
rcomp [in Companion.ccs_mu_syn]
rmap [in Companion.ccs_mu_syn]


S

S [in Companion.fin]
sceil [in Companion.companion_rel]
scons [in Companion.fin]
scons_simpl [in Companion.fin]
sound [in Companion.companion_sound]
sup_closed [in Companion.companion_mu]
symmetric [in Companion.companion_rel]


T

t [in Companion.companion]


U

up [in Companion.ccs_mu_syn]
upr [in Companion.ccs_mu_syn]



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 (410 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 (11 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 (31 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 (12 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 (160 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 (65 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 (21 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 (10 entries)
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 (49 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 (11 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 (40 entries)