| 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 | (408 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 | (9 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 | (7 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 | (17 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 | (6 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 | (193 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 | (3 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 | (29 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 | (7 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 | (19 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 | (36 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 | (12 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 | (34 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 | (33 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 | (3 entries) |
Global Index
A
a [constructor, in cawu.divergence]A [definition, in cawu.ccs]
accumulate [lemma, in cawu.coinduction]
acd [module, in cawu.ccs]
acd.a [constructor, in cawu.ccs]
acd.c [constructor, in cawu.ccs]
acd.d [constructor, in cawu.ccs]
acd.N [definition, in cawu.ccs]
acd.N' [inductive, in cawu.ccs]
antisym [lemma, in cawu.lattice]
antisym' [lemma, in cawu.lattice]
app_weq [instance, in cawu.lattice]
app_leq [instance, in cawu.lattice]
B
b [constructor, in cawu.divergence]B [abbreviation, in cawu.coinduction]
B [abbreviation, in cawu.coinduction]
b [abbreviation, in cawu.coinduction]
B [definition, in cawu.coinduction]
B [definition, in cawu.ccs]
bAB [lemma, in cawu.ccs]
bCD [lemma, in cawu.ccs]
Bfb [lemma, in cawu.coinduction]
binary_proper [lemma, in cawu.rel]
binary_sym [lemma, in cawu.rel]
binary_ctx [definition, in cawu.rel]
body [projection, in cawu.lattice]
bot [projection, in cawu.lattice]
by_Symmetry [lemma, in cawu.coinduction]
by_symmetry [lemma, in cawu.coinduction]
b_T [lemma, in cawu.coinduction]
B_spec [lemma, in cawu.coinduction]
b_t [lemma, in cawu.coinduction]
b' [abbreviation, in cawu.coinduction]
C
c [constructor, in cawu.divergence]C [definition, in cawu.ccs]
Cancel [lemma, in cawu.coinduction]
cap [projection, in cawu.lattice]
capA [lemma, in cawu.lattice]
capbx [lemma, in cawu.lattice]
capC [lemma, in cawu.lattice]
capI [lemma, in cawu.lattice]
captx [lemma, in cawu.lattice]
capxb [lemma, in cawu.lattice]
capxt [lemma, in cawu.lattice]
cap_weq [instance, in cawu.lattice]
cap_leq [instance, in cawu.lattice]
cap_r [lemma, in cawu.lattice]
cap_l [lemma, in cawu.lattice]
cap_spec [projection, in cawu.lattice]
CCS [module, in cawu.ccs]
ccs [library]
CCSacd [module, in cawu.ccs]
CCS.B [abbreviation, in cawu.ccs]
CCS.b [abbreviation, in cawu.ccs]
CCS.converse_t [lemma, in cawu.ccs]
CCS.Equivalence_bisim [lemma, in cawu.ccs]
CCS.Equivalence_t [instance, in cawu.ccs]
CCS.Equivalence_T [instance, in cawu.ccs]
CCS.fresh [definition, in cawu.ccs]
CCS.id_S [definition, in cawu.ccs]
CCS.inp [constructor, in cawu.ccs]
CCS.label [inductive, in cawu.ccs]
CCS.new [constructor, in cawu.ccs]
CCS.newt_t [instance, in cawu.ccs]
CCS.new_t [lemma, in cawu.ccs]
CCS.nil [constructor, in cawu.ccs]
CCS.out [constructor, in cawu.ccs]
CCS.par [constructor, in cawu.ccs]
CCS.parA [lemma, in cawu.ccs]
CCS.parC [lemma, in cawu.ccs]
CCS.part_t [instance, in cawu.ccs]
CCS.par_t [lemma, in cawu.ccs]
CCS.par0p [lemma, in cawu.ccs]
CCS.pls [constructor, in cawu.ccs]
CCS.plst_t [instance, in cawu.ccs]
CCS.pls_t [lemma, in cawu.ccs]
CCS.prf [constructor, in cawu.ccs]
CCS.prft_t [instance, in cawu.ccs]
CCS.prf_t [lemma, in cawu.ccs]
CCS.refl_t [lemma, in cawu.ccs]
CCS.rep [constructor, in cawu.ccs]
CCS.rept_t [instance, in cawu.ccs]
CCS.rep_t [lemma, in cawu.ccs]
CCS.rep_trans' [lemma, in cawu.ccs]
CCS.rep_trans [lemma, in cawu.ccs]
CCS.s [definition, in cawu.ccs]
CCS.S [inductive, in cawu.ccs]
CCS.Sd [lemma, in cawu.ccs]
CCS.square_t [lemma, in cawu.ccs]
CCS.t [abbreviation, in cawu.ccs]
CCS.T [abbreviation, in cawu.ccs]
CCS.tau [constructor, in cawu.ccs]
CCS.trans [inductive, in cawu.ccs]
CCS.t_rep [constructor, in cawu.ccs]
CCS.t_new [constructor, in cawu.ccs]
CCS.t_par_rl [constructor, in cawu.ccs]
CCS.t_par_lr [constructor, in cawu.ccs]
CCS.t_par_r [constructor, in cawu.ccs]
CCS.t_par_l [constructor, in cawu.ccs]
CCS.t_pls_r [constructor, in cawu.ccs]
CCS.t_pls_l [constructor, in cawu.ccs]
CCS.t_prf [constructor, in cawu.ccs]
CCS.unfold_rep [lemma, in cawu.ccs]
_ ~ _ [notation, in cawu.ccs]
Coinduction [lemma, in cawu.coinduction]
coinduction [lemma, in cawu.coinduction]
coinduction [library]
comp [definition, in cawu.lattice]
compA [lemma, in cawu.lattice]
companion_gfp [lemma, in cawu.coinduction]
compat [abbreviation, in cawu.coinduction]
compat [abbreviation, in cawu.coinduction]
compat_invol [lemma, in cawu.coinduction]
compat_if_fi [lemma, in cawu.coinduction]
compat_constid [lemma, in cawu.coinduction]
compat_csquare [lemma, in cawu.coinduction]
compat_t [lemma, in cawu.coinduction]
compat_sup [lemma, in cawu.coinduction]
compat_const [lemma, in cawu.coinduction]
compat_b [lemma, in cawu.coinduction]
compat_comp [lemma, in cawu.coinduction]
compat_id [lemma, in cawu.coinduction]
compIx [lemma, in cawu.lattice]
CompleteLattice [record, in cawu.lattice]
CompleteLattice_mon [instance, in cawu.lattice]
CompleteLattice_fun [instance, in cawu.lattice]
CompleteLattice_Prop [instance, in cawu.lattice]
compxI [lemma, in cawu.lattice]
comp_weq [instance, in cawu.lattice]
comp_leq [instance, in cawu.lattice]
const [definition, in cawu.lattice]
converse [definition, in cawu.rel]
csquare [definition, in cawu.coinduction]
cup [projection, in cawu.lattice]
cupA [lemma, in cawu.lattice]
cupbx [lemma, in cawu.lattice]
cupC [lemma, in cawu.lattice]
cupI [lemma, in cawu.lattice]
cuptx [lemma, in cawu.lattice]
cupxb [lemma, in cawu.lattice]
cupxt [lemma, in cawu.lattice]
cup_weq [instance, in cawu.lattice]
cup_leq [instance, in cawu.lattice]
cup_r [lemma, in cawu.lattice]
cup_l [lemma, in cawu.lattice]
cup_spec [projection, in cawu.lattice]
D
D [abbreviation, in cawu.divergence]d [constructor, in cawu.divergence]
D [definition, in cawu.ccs]
dA [lemma, in cawu.ccs]
dB [lemma, in cawu.ccs]
dC [lemma, in cawu.ccs]
dD [lemma, in cawu.ccs]
divergence [library]
diverges [abbreviation, in cawu.divergence]
done [lemma, in cawu.divergence]
Dual [definition, in cawu.lattice]
D' [abbreviation, in cawu.divergence]
E
e [constructor, in cawu.divergence]edge [definition, in cawu.divergence]
eleq_infx_all [lemma, in cawu.lattice]
eleq_infx_id [lemma, in cawu.lattice]
eleq_infx [lemma, in cawu.lattice]
eleq_xsup_all [lemma, in cawu.lattice]
eleq_xsup_id [lemma, in cawu.lattice]
eleq_xsup [lemma, in cawu.lattice]
enhanced_gfp [lemma, in cawu.coinduction]
Equivalence_weq [instance, in cawu.lattice]
Equivalence_gfp [lemma, in cawu.rel]
Equivalence_t [lemma, in cawu.rel]
Equivalence_T [lemma, in cawu.rel]
F
f [constructor, in cawu.divergence]from_below [lemma, in cawu.lattice]
from_above [lemma, in cawu.lattice]
fTf_Tf [lemma, in cawu.coinduction]
ftT_T [lemma, in cawu.coinduction]
fT_T [lemma, in cawu.coinduction]
ft_t [lemma, in cawu.coinduction]
f_Tf [lemma, in cawu.coinduction]
G
gfp [definition, in cawu.coinduction]gfp_T [lemma, in cawu.coinduction]
gfp_weq [instance, in cawu.coinduction]
gfp_leq [instance, in cawu.coinduction]
gfp_t [lemma, in cawu.coinduction]
gfp_fp [lemma, in cawu.coinduction]
gfp_pfp [lemma, in cawu.coinduction]
H
Hbody [projection, in cawu.lattice]Hbody' [instance, in cawu.lattice]
I
id [definition, in cawu.lattice]id_T [lemma, in cawu.coinduction]
id_t [lemma, in cawu.coinduction]
In [definition, in cawu.divergence]
inf [section, in cawu.lattice]
inf [projection, in cawu.lattice]
inf_all_spec [lemma, in cawu.lattice]
inf_id_spec [lemma, in cawu.lattice]
inf_weq [instance, in cawu.lattice]
inf_leq [instance, in cawu.lattice]
inf_all [abbreviation, in cawu.lattice]
inf_spec [projection, in cawu.lattice]
init [lemma, in cawu.divergence]
invol [projection, in cawu.coinduction]
invol [constructor, in cawu.coinduction]
Involution [record, in cawu.coinduction]
Involution [inductive, in cawu.coinduction]
Involution_converse [instance, in cawu.rel]
invol_t [lemma, in cawu.coinduction]
invol' [lemma, in cawu.coinduction]
In_leq [lemma, in cawu.divergence]
In_single [lemma, in cawu.divergence]
In_cons [lemma, in cawu.divergence]
In_nil [lemma, in cawu.divergence]
in_binary_ctx [lemma, in cawu.rel]
in_unary_ctx [lemma, in cawu.rel]
in_pair3 [lemma, in cawu.rel]
in_pair2 [lemma, in cawu.rel]
in_pair1 [lemma, in cawu.rel]
in_pair0 [lemma, in cawu.rel]
J
jump [lemma, in cawu.divergence]L
l [section, in cawu.divergence]lattice [library]
leq [projection, in cawu.lattice]
leq_f_tf [lemma, in cawu.coinduction]
leq_f_ft [lemma, in cawu.coinduction]
leq_t [lemma, in cawu.coinduction]
leq_gfp [lemma, in cawu.coinduction]
leq_capx [lemma, in cawu.lattice]
leq_infx_all [lemma, in cawu.lattice]
leq_infx_id [lemma, in cawu.lattice]
leq_infx [lemma, in cawu.lattice]
leq_xcup [lemma, in cawu.lattice]
leq_xsup_all [lemma, in cawu.lattice]
leq_xsup_id [lemma, in cawu.lattice]
leq_xsup [lemma, in cawu.lattice]
leq_xt [projection, in cawu.lattice]
leq_bx [projection, in cawu.lattice]
leq_binary_ctx [lemma, in cawu.rel]
leq_unary_ctx [lemma, in cawu.rel]
leq_pair [lemma, in cawu.rel]
l.A [variable, in cawu.divergence]
M
mbot_o [lemma, in cawu.lattice]mcap_o [lemma, in cawu.lattice]
mcup_o [lemma, in cawu.lattice]
minf_o [lemma, in cawu.lattice]
mon [record, in cawu.lattice]
mon [section, in cawu.lattice]
_ o _ [notation, in cawu.lattice]
msup_o [lemma, in cawu.lattice]
mtop_o [lemma, in cawu.lattice]
N
N [module, in cawu.ccs]N.N [axiom, in cawu.ccs]
O
op_leq_weq_2 [lemma, in cawu.lattice]op_leq_weq_1 [lemma, in cawu.lattice]
o_mcap [lemma, in cawu.lattice]
o_minf [lemma, in cawu.lattice]
o_mcup [lemma, in cawu.lattice]
o_msup [lemma, in cawu.lattice]
P
paco [module, in cawu.coinduction]paco.G [definition, in cawu.coinduction]
paco.g [definition, in cawu.coinduction]
paco.G_upto [lemma, in cawu.coinduction]
paco.G_bt [lemma, in cawu.coinduction]
paco.G' [abbreviation, in cawu.coinduction]
paco.s [section, in cawu.coinduction]
paco.s.b [variable, in cawu.coinduction]
paco.t [abbreviation, in cawu.coinduction]
pair [definition, in cawu.rel]
PartialOrder_weq_leq [instance, in cawu.lattice]
play [lemma, in cawu.divergence]
PreOrder_leq [projection, in cawu.lattice]
proof_system.b [variable, in cawu.coinduction]
proof_system [section, in cawu.coinduction]
R
rel [library]rel_gfp_t [instance, in cawu.rel]
rel_gfp_T [instance, in cawu.rel]
respectful [module, in cawu.coinduction]
respectful.B [abbreviation, in cawu.coinduction]
respectful.bt_b't [lemma, in cawu.coinduction]
respectful.b_b't [lemma, in cawu.coinduction]
respectful.B' [abbreviation, in cawu.coinduction]
respectful.b' [abbreviation, in cawu.coinduction]
respectful.B'S_BS [lemma, in cawu.coinduction]
respectful.B'T'_BT [lemma, in cawu.coinduction]
respectful.s [section, in cawu.coinduction]
respectful.s.b [variable, in cawu.coinduction]
respectful.t [abbreviation, in cawu.coinduction]
respectful.T [abbreviation, in cawu.coinduction]
respectful.t_t' [lemma, in cawu.coinduction]
respectful.T' [abbreviation, in cawu.coinduction]
respectful.t' [abbreviation, in cawu.coinduction]
respectful.T'_T [lemma, in cawu.coinduction]
rule_coind [lemma, in cawu.coinduction]
rule_upto [lemma, in cawu.coinduction]
rule_done [lemma, in cawu.coinduction]
rule_init [lemma, in cawu.coinduction]
S
S [inductive, in cawu.divergence]s [section, in cawu.rel]
save [lemma, in cawu.divergence]
square [definition, in cawu.rel]
stagnate_t [lemma, in cawu.coinduction]
step [definition, in cawu.divergence]
streams [module, in cawu.streams]
streams [library]
streams.b [definition, in cawu.streams]
streams.c [definition, in cawu.streams]
streams.cons [constructor, in cawu.streams]
streams.converse_t [lemma, in cawu.streams]
streams.c_mult [lemma, in cawu.streams]
streams.c_plus [lemma, in cawu.streams]
streams.Equivalence_bisim [lemma, in cawu.streams]
streams.Equivalence_t [instance, in cawu.streams]
streams.eq_t [lemma, in cawu.streams]
streams.expand [lemma, in cawu.streams]
streams.hd [definition, in cawu.streams]
streams.hd_mult [variable, in cawu.streams]
streams.hd_shuf [variable, in cawu.streams]
streams.hd_bisim [instance, in cawu.streams]
streams.mult [axiom, in cawu.streams]
streams.multA [lemma, in cawu.streams]
streams.multC [lemma, in cawu.streams]
streams.multC_X [lemma, in cawu.streams]
streams.multC_11 [lemma, in cawu.streams]
streams.multC_n [lemma, in cawu.streams]
streams.multt_t [instance, in cawu.streams]
streams.mult_plus_x [lemma, in cawu.streams]
streams.mult_t [lemma, in cawu.streams]
streams.mult_x_plus [lemma, in cawu.streams]
streams.mult_x1 [lemma, in cawu.streams]
streams.mult_1x [lemma, in cawu.streams]
streams.mult_x0 [lemma, in cawu.streams]
streams.mult_0x [lemma, in cawu.streams]
streams.plus [definition, in cawu.streams]
streams.plusA [lemma, in cawu.streams]
streams.plusC [lemma, in cawu.streams]
streams.plust_t [instance, in cawu.streams]
streams.plus_t [lemma, in cawu.streams]
streams.plus_0x [lemma, in cawu.streams]
streams.S [inductive, in cawu.streams]
streams.shuf [axiom, in cawu.streams]
streams.shufA [lemma, in cawu.streams]
streams.shufC [lemma, in cawu.streams]
streams.shuft_t [instance, in cawu.streams]
streams.shuf_t [lemma, in cawu.streams]
streams.shuf_plus_x [lemma, in cawu.streams]
streams.shuf_x_plus [lemma, in cawu.streams]
streams.shuf_1x [lemma, in cawu.streams]
streams.shuf_0x [lemma, in cawu.streams]
streams.square_t [lemma, in cawu.streams]
streams.t [abbreviation, in cawu.streams]
streams.T [abbreviation, in cawu.streams]
streams.tl [definition, in cawu.streams]
streams.tl_mult [variable, in cawu.streams]
streams.tl_shuf [variable, in cawu.streams]
streams.tl_bisim [instance, in cawu.streams]
streams.X [definition, in cawu.streams]
_ * _ [notation, in cawu.streams]
_ @ _ [notation, in cawu.streams]
_ + _ [notation, in cawu.streams]
_ ~ _ [notation, in cawu.streams]
sup [section, in cawu.lattice]
sup [projection, in cawu.lattice]
sup_all_spec [lemma, in cawu.lattice]
sup_id_spec [lemma, in cawu.lattice]
sup_weq [instance, in cawu.lattice]
sup_leq [instance, in cawu.lattice]
sup_all [abbreviation, in cawu.lattice]
sup_spec [projection, in cawu.lattice]
Switch [lemma, in cawu.coinduction]
switch [lemma, in cawu.coinduction]
symmetry [section, in cawu.coinduction]
symmetry.s [variable, in cawu.coinduction]
s.A [variable, in cawu.rel]
s.b [variable, in cawu.rel]
s.converse_t [variable, in cawu.rel]
s.eq_t [variable, in cawu.rel]
s.square_t [variable, in cawu.rel]
s1 [section, in cawu.coinduction]
s1.b [variable, in cawu.coinduction]
s2 [section, in cawu.coinduction]
s2.b [variable, in cawu.coinduction]
s3 [section, in cawu.coinduction]
s3.b [variable, in cawu.coinduction]
T
t [abbreviation, in cawu.coinduction]T [abbreviation, in cawu.coinduction]
t [abbreviation, in cawu.coinduction]
T [abbreviation, in cawu.coinduction]
t [abbreviation, in cawu.coinduction]
T [abbreviation, in cawu.coinduction]
t [abbreviation, in cawu.coinduction]
t [definition, in cawu.coinduction]
Tf_T [lemma, in cawu.coinduction]
top [projection, in cawu.lattice]
TT_T [lemma, in cawu.coinduction]
tt_t [lemma, in cawu.coinduction]
t_T [lemma, in cawu.coinduction]
T_idem [lemma, in cawu.coinduction]
t_gfp [lemma, in cawu.coinduction]
t_idem [lemma, in cawu.coinduction]
t' [abbreviation, in cawu.coinduction]
U
unary_proper [lemma, in cawu.rel]unary_sym [lemma, in cawu.rel]
unary_ctx [definition, in cawu.rel]
W
weq [projection, in cawu.lattice]weq_spec [projection, in cawu.lattice]
X
xaccumulate [definition, in cawu.coinduction]other
_ o _ [notation, in cawu.lattice]_ <= _ [notation, in cawu.lattice]
_ == _ [notation, in cawu.lattice]
Notation Index
C
_ ~ _ [in cawu.ccs]M
_ o _ [in cawu.lattice]S
_ * _ [in cawu.streams]_ @ _ [in cawu.streams]
_ + _ [in cawu.streams]
_ ~ _ [in cawu.streams]
other
_ o _ [in cawu.lattice]_ <= _ [in cawu.lattice]
_ == _ [in cawu.lattice]
Module Index
A
acd [in cawu.ccs]C
CCS [in cawu.ccs]CCSacd [in cawu.ccs]
N
N [in cawu.ccs]P
paco [in cawu.coinduction]R
respectful [in cawu.coinduction]S
streams [in cawu.streams]Variable Index
L
l.A [in cawu.divergence]P
paco.s.b [in cawu.coinduction]proof_system.b [in cawu.coinduction]
R
respectful.s.b [in cawu.coinduction]S
streams.hd_mult [in cawu.streams]streams.hd_shuf [in cawu.streams]
streams.tl_mult [in cawu.streams]
streams.tl_shuf [in cawu.streams]
symmetry.s [in cawu.coinduction]
s.A [in cawu.rel]
s.b [in cawu.rel]
s.converse_t [in cawu.rel]
s.eq_t [in cawu.rel]
s.square_t [in cawu.rel]
s1.b [in cawu.coinduction]
s2.b [in cawu.coinduction]
s3.b [in cawu.coinduction]
Library Index
C
ccscoinduction
D
divergenceL
latticeR
relS
streamsLemma Index
A
accumulate [in cawu.coinduction]antisym [in cawu.lattice]
antisym' [in cawu.lattice]
B
bAB [in cawu.ccs]bCD [in cawu.ccs]
Bfb [in cawu.coinduction]
binary_proper [in cawu.rel]
binary_sym [in cawu.rel]
by_Symmetry [in cawu.coinduction]
by_symmetry [in cawu.coinduction]
b_T [in cawu.coinduction]
B_spec [in cawu.coinduction]
b_t [in cawu.coinduction]
C
Cancel [in cawu.coinduction]capA [in cawu.lattice]
capbx [in cawu.lattice]
capC [in cawu.lattice]
capI [in cawu.lattice]
captx [in cawu.lattice]
capxb [in cawu.lattice]
capxt [in cawu.lattice]
cap_r [in cawu.lattice]
cap_l [in cawu.lattice]
CCS.converse_t [in cawu.ccs]
CCS.Equivalence_bisim [in cawu.ccs]
CCS.new_t [in cawu.ccs]
CCS.parA [in cawu.ccs]
CCS.parC [in cawu.ccs]
CCS.par_t [in cawu.ccs]
CCS.par0p [in cawu.ccs]
CCS.pls_t [in cawu.ccs]
CCS.prf_t [in cawu.ccs]
CCS.refl_t [in cawu.ccs]
CCS.rep_t [in cawu.ccs]
CCS.rep_trans' [in cawu.ccs]
CCS.rep_trans [in cawu.ccs]
CCS.Sd [in cawu.ccs]
CCS.square_t [in cawu.ccs]
CCS.unfold_rep [in cawu.ccs]
Coinduction [in cawu.coinduction]
coinduction [in cawu.coinduction]
compA [in cawu.lattice]
companion_gfp [in cawu.coinduction]
compat_invol [in cawu.coinduction]
compat_if_fi [in cawu.coinduction]
compat_constid [in cawu.coinduction]
compat_csquare [in cawu.coinduction]
compat_t [in cawu.coinduction]
compat_sup [in cawu.coinduction]
compat_const [in cawu.coinduction]
compat_b [in cawu.coinduction]
compat_comp [in cawu.coinduction]
compat_id [in cawu.coinduction]
compIx [in cawu.lattice]
compxI [in cawu.lattice]
cupA [in cawu.lattice]
cupbx [in cawu.lattice]
cupC [in cawu.lattice]
cupI [in cawu.lattice]
cuptx [in cawu.lattice]
cupxb [in cawu.lattice]
cupxt [in cawu.lattice]
cup_r [in cawu.lattice]
cup_l [in cawu.lattice]
D
dA [in cawu.ccs]dB [in cawu.ccs]
dC [in cawu.ccs]
dD [in cawu.ccs]
done [in cawu.divergence]
E
eleq_infx_all [in cawu.lattice]eleq_infx_id [in cawu.lattice]
eleq_infx [in cawu.lattice]
eleq_xsup_all [in cawu.lattice]
eleq_xsup_id [in cawu.lattice]
eleq_xsup [in cawu.lattice]
enhanced_gfp [in cawu.coinduction]
Equivalence_gfp [in cawu.rel]
Equivalence_t [in cawu.rel]
Equivalence_T [in cawu.rel]
F
from_below [in cawu.lattice]from_above [in cawu.lattice]
fTf_Tf [in cawu.coinduction]
ftT_T [in cawu.coinduction]
fT_T [in cawu.coinduction]
ft_t [in cawu.coinduction]
f_Tf [in cawu.coinduction]
G
gfp_T [in cawu.coinduction]gfp_t [in cawu.coinduction]
gfp_fp [in cawu.coinduction]
gfp_pfp [in cawu.coinduction]
I
id_T [in cawu.coinduction]id_t [in cawu.coinduction]
inf_all_spec [in cawu.lattice]
inf_id_spec [in cawu.lattice]
init [in cawu.divergence]
invol_t [in cawu.coinduction]
invol' [in cawu.coinduction]
In_leq [in cawu.divergence]
In_single [in cawu.divergence]
In_cons [in cawu.divergence]
In_nil [in cawu.divergence]
in_binary_ctx [in cawu.rel]
in_unary_ctx [in cawu.rel]
in_pair3 [in cawu.rel]
in_pair2 [in cawu.rel]
in_pair1 [in cawu.rel]
in_pair0 [in cawu.rel]
J
jump [in cawu.divergence]L
leq_f_tf [in cawu.coinduction]leq_f_ft [in cawu.coinduction]
leq_t [in cawu.coinduction]
leq_gfp [in cawu.coinduction]
leq_capx [in cawu.lattice]
leq_infx_all [in cawu.lattice]
leq_infx_id [in cawu.lattice]
leq_infx [in cawu.lattice]
leq_xcup [in cawu.lattice]
leq_xsup_all [in cawu.lattice]
leq_xsup_id [in cawu.lattice]
leq_xsup [in cawu.lattice]
leq_binary_ctx [in cawu.rel]
leq_unary_ctx [in cawu.rel]
leq_pair [in cawu.rel]
M
mbot_o [in cawu.lattice]mcap_o [in cawu.lattice]
mcup_o [in cawu.lattice]
minf_o [in cawu.lattice]
msup_o [in cawu.lattice]
mtop_o [in cawu.lattice]
O
op_leq_weq_2 [in cawu.lattice]op_leq_weq_1 [in cawu.lattice]
o_mcap [in cawu.lattice]
o_minf [in cawu.lattice]
o_mcup [in cawu.lattice]
o_msup [in cawu.lattice]
P
paco.G_upto [in cawu.coinduction]paco.G_bt [in cawu.coinduction]
play [in cawu.divergence]
R
respectful.bt_b't [in cawu.coinduction]respectful.b_b't [in cawu.coinduction]
respectful.B'S_BS [in cawu.coinduction]
respectful.B'T'_BT [in cawu.coinduction]
respectful.t_t' [in cawu.coinduction]
respectful.T'_T [in cawu.coinduction]
rule_coind [in cawu.coinduction]
rule_upto [in cawu.coinduction]
rule_done [in cawu.coinduction]
rule_init [in cawu.coinduction]
S
save [in cawu.divergence]stagnate_t [in cawu.coinduction]
streams.converse_t [in cawu.streams]
streams.c_mult [in cawu.streams]
streams.c_plus [in cawu.streams]
streams.Equivalence_bisim [in cawu.streams]
streams.eq_t [in cawu.streams]
streams.expand [in cawu.streams]
streams.multA [in cawu.streams]
streams.multC [in cawu.streams]
streams.multC_X [in cawu.streams]
streams.multC_11 [in cawu.streams]
streams.multC_n [in cawu.streams]
streams.mult_plus_x [in cawu.streams]
streams.mult_t [in cawu.streams]
streams.mult_x_plus [in cawu.streams]
streams.mult_x1 [in cawu.streams]
streams.mult_1x [in cawu.streams]
streams.mult_x0 [in cawu.streams]
streams.mult_0x [in cawu.streams]
streams.plusA [in cawu.streams]
streams.plusC [in cawu.streams]
streams.plus_t [in cawu.streams]
streams.plus_0x [in cawu.streams]
streams.shufA [in cawu.streams]
streams.shufC [in cawu.streams]
streams.shuf_t [in cawu.streams]
streams.shuf_plus_x [in cawu.streams]
streams.shuf_x_plus [in cawu.streams]
streams.shuf_1x [in cawu.streams]
streams.shuf_0x [in cawu.streams]
streams.square_t [in cawu.streams]
sup_all_spec [in cawu.lattice]
sup_id_spec [in cawu.lattice]
Switch [in cawu.coinduction]
switch [in cawu.coinduction]
T
Tf_T [in cawu.coinduction]TT_T [in cawu.coinduction]
tt_t [in cawu.coinduction]
t_T [in cawu.coinduction]
T_idem [in cawu.coinduction]
t_gfp [in cawu.coinduction]
t_idem [in cawu.coinduction]
U
unary_proper [in cawu.rel]unary_sym [in cawu.rel]
Axiom Index
N
N.N [in cawu.ccs]S
streams.mult [in cawu.streams]streams.shuf [in cawu.streams]
Constructor Index
A
a [in cawu.divergence]acd.a [in cawu.ccs]
acd.c [in cawu.ccs]
acd.d [in cawu.ccs]
B
b [in cawu.divergence]C
c [in cawu.divergence]CCS.inp [in cawu.ccs]
CCS.new [in cawu.ccs]
CCS.nil [in cawu.ccs]
CCS.out [in cawu.ccs]
CCS.par [in cawu.ccs]
CCS.pls [in cawu.ccs]
CCS.prf [in cawu.ccs]
CCS.rep [in cawu.ccs]
CCS.tau [in cawu.ccs]
CCS.t_rep [in cawu.ccs]
CCS.t_new [in cawu.ccs]
CCS.t_par_rl [in cawu.ccs]
CCS.t_par_lr [in cawu.ccs]
CCS.t_par_r [in cawu.ccs]
CCS.t_par_l [in cawu.ccs]
CCS.t_pls_r [in cawu.ccs]
CCS.t_pls_l [in cawu.ccs]
CCS.t_prf [in cawu.ccs]
D
d [in cawu.divergence]E
e [in cawu.divergence]F
f [in cawu.divergence]I
invol [in cawu.coinduction]S
streams.cons [in cawu.streams]Inductive Index
A
acd.N' [in cawu.ccs]C
CCS.label [in cawu.ccs]CCS.S [in cawu.ccs]
CCS.trans [in cawu.ccs]
I
Involution [in cawu.coinduction]S
S [in cawu.divergence]streams.S [in cawu.streams]
Projection Index
B
body [in cawu.lattice]bot [in cawu.lattice]
C
cap [in cawu.lattice]cap_spec [in cawu.lattice]
cup [in cawu.lattice]
cup_spec [in cawu.lattice]
H
Hbody [in cawu.lattice]I
inf [in cawu.lattice]inf_spec [in cawu.lattice]
invol [in cawu.coinduction]
L
leq [in cawu.lattice]leq_xt [in cawu.lattice]
leq_bx [in cawu.lattice]
P
PreOrder_leq [in cawu.lattice]S
sup [in cawu.lattice]sup_spec [in cawu.lattice]
T
top [in cawu.lattice]W
weq [in cawu.lattice]weq_spec [in cawu.lattice]
Instance Index
A
app_weq [in cawu.lattice]app_leq [in cawu.lattice]
C
cap_weq [in cawu.lattice]cap_leq [in cawu.lattice]
CCS.Equivalence_t [in cawu.ccs]
CCS.Equivalence_T [in cawu.ccs]
CCS.newt_t [in cawu.ccs]
CCS.part_t [in cawu.ccs]
CCS.plst_t [in cawu.ccs]
CCS.prft_t [in cawu.ccs]
CCS.rept_t [in cawu.ccs]
CompleteLattice_mon [in cawu.lattice]
CompleteLattice_fun [in cawu.lattice]
CompleteLattice_Prop [in cawu.lattice]
comp_weq [in cawu.lattice]
comp_leq [in cawu.lattice]
cup_weq [in cawu.lattice]
cup_leq [in cawu.lattice]
E
Equivalence_weq [in cawu.lattice]G
gfp_weq [in cawu.coinduction]gfp_leq [in cawu.coinduction]
H
Hbody' [in cawu.lattice]I
inf_weq [in cawu.lattice]inf_leq [in cawu.lattice]
Involution_converse [in cawu.rel]
P
PartialOrder_weq_leq [in cawu.lattice]R
rel_gfp_t [in cawu.rel]rel_gfp_T [in cawu.rel]
S
streams.Equivalence_t [in cawu.streams]streams.hd_bisim [in cawu.streams]
streams.multt_t [in cawu.streams]
streams.plust_t [in cawu.streams]
streams.shuft_t [in cawu.streams]
streams.tl_bisim [in cawu.streams]
sup_weq [in cawu.lattice]
sup_leq [in cawu.lattice]
Section Index
I
inf [in cawu.lattice]L
l [in cawu.divergence]M
mon [in cawu.lattice]P
paco.s [in cawu.coinduction]proof_system [in cawu.coinduction]
R
respectful.s [in cawu.coinduction]S
s [in cawu.rel]sup [in cawu.lattice]
symmetry [in cawu.coinduction]
s1 [in cawu.coinduction]
s2 [in cawu.coinduction]
s3 [in cawu.coinduction]
Abbreviation Index
B
B [in cawu.coinduction]B [in cawu.coinduction]
b [in cawu.coinduction]
b' [in cawu.coinduction]
C
CCS.B [in cawu.ccs]CCS.b [in cawu.ccs]
CCS.t [in cawu.ccs]
CCS.T [in cawu.ccs]
compat [in cawu.coinduction]
compat [in cawu.coinduction]
D
D [in cawu.divergence]diverges [in cawu.divergence]
D' [in cawu.divergence]
I
inf_all [in cawu.lattice]P
paco.G' [in cawu.coinduction]paco.t [in cawu.coinduction]
R
respectful.B [in cawu.coinduction]respectful.B' [in cawu.coinduction]
respectful.b' [in cawu.coinduction]
respectful.t [in cawu.coinduction]
respectful.T [in cawu.coinduction]
respectful.T' [in cawu.coinduction]
respectful.t' [in cawu.coinduction]
S
streams.t [in cawu.streams]streams.T [in cawu.streams]
sup_all [in cawu.lattice]
T
t [in cawu.coinduction]T [in cawu.coinduction]
t [in cawu.coinduction]
T [in cawu.coinduction]
t [in cawu.coinduction]
T [in cawu.coinduction]
t [in cawu.coinduction]
t' [in cawu.coinduction]
Definition Index
A
A [in cawu.ccs]acd.N [in cawu.ccs]
B
B [in cawu.coinduction]B [in cawu.ccs]
binary_ctx [in cawu.rel]
C
C [in cawu.ccs]CCS.fresh [in cawu.ccs]
CCS.id_S [in cawu.ccs]
CCS.s [in cawu.ccs]
comp [in cawu.lattice]
const [in cawu.lattice]
converse [in cawu.rel]
csquare [in cawu.coinduction]
D
D [in cawu.ccs]Dual [in cawu.lattice]
E
edge [in cawu.divergence]G
gfp [in cawu.coinduction]I
id [in cawu.lattice]In [in cawu.divergence]
P
paco.G [in cawu.coinduction]paco.g [in cawu.coinduction]
pair [in cawu.rel]
S
square [in cawu.rel]step [in cawu.divergence]
streams.b [in cawu.streams]
streams.c [in cawu.streams]
streams.hd [in cawu.streams]
streams.plus [in cawu.streams]
streams.tl [in cawu.streams]
streams.X [in cawu.streams]
T
t [in cawu.coinduction]U
unary_ctx [in cawu.rel]X
xaccumulate [in cawu.coinduction]Record Index
C
CompleteLattice [in cawu.lattice]I
Involution [in cawu.coinduction]M
mon [in cawu.lattice]| 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 | (408 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 | (9 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 | (7 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 | (17 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 | (6 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 | (193 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 | (3 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 | (29 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 | (7 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 | (19 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 | (36 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 | (12 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 | (34 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 | (33 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 | (3 entries) |
This page has been generated by coqdoc