| 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_bisimccs_rep_lang
ccs_mu_sem
ccs_mu_syn
ccs_mu_bisim
companion
companion_rel
companion_param
companion_sound
companion_mu
F
finP
prelimLemma 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) |