| 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 | (292 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 | (2 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 | (7 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 | (115 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 | (95 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 | (12 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 | (29 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) |
| 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 | (20 entries) |
Global Index
A
alglaws [library]ASS_PAR [lemma, in PiCalc.alglaws]
ASS_SUM [lemma, in PiCalc.alglaws]
Aux1 [lemma, in PiCalc.basiclemmata]
Aux2 [lemma, in PiCalc.basiclemmata]
B
bang [constructor, in PiCalc.picalcth]bangpack [library]
BANG_S [lemma, in PiCalc.bangpack]
BANG_S_L6 [lemma, in PiCalc.bangpack]
BANG_TAU_AUX4 [lemma, in PiCalc.bangpack]
BANG_TAU_AUX3 [lemma, in PiCalc.bangpack]
BANG_TAU_AUX2 [lemma, in PiCalc.bangpack]
BANG_TAU_AUX1 [lemma, in PiCalc.bangpack]
BANG_BTR_AUX [lemma, in PiCalc.bangpack]
BANG_FTR_AUX [lemma, in PiCalc.bangpack]
BANG_TAU [lemma, in PiCalc.bangpack]
BANG_BTR [lemma, in PiCalc.bangpack]
BANG_OUT [lemma, in PiCalc.bangpack]
BANG_UNF [lemma, in PiCalc.alglaws]
basiclemmata [library]
bBANG [constructor, in PiCalc.picalcth]
Bfun [definition, in PiCalc.basiclemmata]
BisBANG_S_UPTO [lemma, in PiCalc.bangpack]
BisBANG_S_FTR2 [lemma, in PiCalc.bangpack]
BisBANG_S_bOUT [lemma, in PiCalc.bangpack]
BisBANG_S_IN [lemma, in PiCalc.bangpack]
BisBANG_S_FTR1 [lemma, in PiCalc.bangpack]
bisbang_s [constructor, in PiCalc.bangpack]
BisBANG_S [inductive, in PiCalc.bangpack]
BisimL6 [lemma, in PiCalc.basiclemmata]
BisNU_E_UPTO [lemma, in PiCalc.alglaws]
BisNU_E_FTR2 [lemma, in PiCalc.alglaws]
BisNU_E_bOUT [lemma, in PiCalc.alglaws]
BisNU_E_IN [lemma, in PiCalc.alglaws]
BisNU_E_FTR1 [lemma, in PiCalc.alglaws]
bisnu_e_ref [constructor, in PiCalc.alglaws]
bisnu_e [constructor, in PiCalc.alglaws]
BisNU_E [inductive, in PiCalc.alglaws]
BisPAR_A_UPTO [lemma, in PiCalc.alglaws]
BisPAR_A_FTR2 [lemma, in PiCalc.alglaws]
BisPAR_A_bOUT [lemma, in PiCalc.alglaws]
BisPAR_A_IN [lemma, in PiCalc.alglaws]
BisPAR_A_FTR1 [lemma, in PiCalc.alglaws]
bispar_a [constructor, in PiCalc.alglaws]
BisPAR_A [inductive, in PiCalc.alglaws]
bispar_c [constructor, in PiCalc.alglaws]
BisPAR_C [inductive, in PiCalc.alglaws]
bispar_s [constructor, in PiCalc.alglaws]
BisPAR_S [inductive, in PiCalc.alglaws]
bl6 [constructor, in PiCalc.basiclemmata]
BL6 [inductive, in PiCalc.basiclemmata]
bMATCH [constructor, in PiCalc.picalcth]
bMISMATCH [constructor, in PiCalc.picalcth]
bOut [constructor, in PiCalc.picalcth]
bPAR1 [constructor, in PiCalc.picalcth]
bPAR2 [constructor, in PiCalc.picalcth]
bRES [constructor, in PiCalc.picalcth]
bSUM1 [constructor, in PiCalc.picalcth]
bSUM2 [constructor, in PiCalc.picalcth]
btrans [inductive, in PiCalc.picalcth]
btrans_ftrans_ind [definition, in PiCalc.basiclemmata]
BTR_L3 [lemma, in PiCalc.basiclemmata]
BTR_L1 [lemma, in PiCalc.basiclemmata]
b_act_notin_ho [definition, in PiCalc.picalcth]
b_act_notin_bOut [constructor, in PiCalc.picalcth]
b_act_notin_In [constructor, in PiCalc.picalcth]
b_act_notin [inductive, in PiCalc.picalcth]
b_act_isin_bOut [constructor, in PiCalc.picalcth]
b_act_isin_In [constructor, in PiCalc.picalcth]
b_act_isin [inductive, in PiCalc.picalcth]
b_act [inductive, in PiCalc.picalcth]
b_act_sub_congr [lemma, in PiCalc.hoaspack]
b_act_spec [lemma, in PiCalc.hoaspack]
b_act_ext [axiom, in PiCalc.hoaspack]
b_act_exp [lemma, in PiCalc.hoaspack]
b_act_mono [axiom, in PiCalc.hoaspack]
C
CF_B_ACT_NOTIN [lemma, in PiCalc.bangpack]cf_tau3 [definition, in PiCalc.bangpack]
cf_tau2 [definition, in PiCalc.bangpack]
cf_tau1 [definition, in PiCalc.bangpack]
cf_b_act [definition, in PiCalc.bangpack]
cf_f_act [definition, in PiCalc.bangpack]
CLOSE1 [constructor, in PiCalc.picalcth]
CLOSE2 [constructor, in PiCalc.picalcth]
COMM_PAR [lemma, in PiCalc.alglaws]
COMM_SUM [lemma, in PiCalc.alglaws]
Completeness [lemma, in PiCalc.xadequacy]
COM1 [constructor, in PiCalc.picalcth]
COM2 [constructor, in PiCalc.picalcth]
cons [constructor, in PiCalc.picalcth]
Co_Ind [constructor, in PiCalc.picalcth]
E
empty [constructor, in PiCalc.picalcth]eq_congr.y [variable, in PiCalc.hoaspack]
eq_congr.x [variable, in PiCalc.hoaspack]
eq_congr [section, in PiCalc.hoaspack]
eta [section, in PiCalc.hoaspack]
ETA_EQ2 [lemma, in PiCalc.hoaspack]
ETA_EQ [lemma, in PiCalc.hoaspack]
expansions [section, in PiCalc.hoaspack]
F
fBANG [constructor, in PiCalc.picalcth]fMATCH [constructor, in PiCalc.picalcth]
fMISMATCH [constructor, in PiCalc.picalcth]
fPAR1 [constructor, in PiCalc.picalcth]
fPAR2 [constructor, in PiCalc.picalcth]
frepl1 [definition, in PiCalc.bangpack]
FREPL1_NOTIN [lemma, in PiCalc.bangpack]
frepl2 [definition, in PiCalc.bangpack]
frepl3 [definition, in PiCalc.bangpack]
frepl4 [definition, in PiCalc.bangpack]
fRES [constructor, in PiCalc.picalcth]
fSUM1 [constructor, in PiCalc.picalcth]
fSUM2 [constructor, in PiCalc.picalcth]
ftrans [inductive, in PiCalc.picalcth]
ftrans_btrans_ind [definition, in PiCalc.basiclemmata]
FTR_L3 [lemma, in PiCalc.basiclemmata]
FTR_L1 [lemma, in PiCalc.basiclemmata]
F_REPL4 [lemma, in PiCalc.bangpack]
F_REPL3 [lemma, in PiCalc.bangpack]
F_REPL2 [lemma, in PiCalc.bangpack]
F_REPL1 [lemma, in PiCalc.bangpack]
f_act_notin_ho [definition, in PiCalc.picalcth]
f_act_notin_Out [constructor, in PiCalc.picalcth]
f_act_notin_tau [constructor, in PiCalc.picalcth]
f_act_notin [inductive, in PiCalc.picalcth]
f_act_isin_Out2 [constructor, in PiCalc.picalcth]
f_act_isin_Out1 [constructor, in PiCalc.picalcth]
f_act_isin [inductive, in PiCalc.picalcth]
f_act [inductive, in PiCalc.picalcth]
f_act_sub_congr [lemma, in PiCalc.hoaspack]
f_act_spec [lemma, in PiCalc.hoaspack]
f_act_ext [axiom, in PiCalc.hoaspack]
f_act_exp [lemma, in PiCalc.hoaspack]
f_act_mono [axiom, in PiCalc.hoaspack]
H
hoaspack [library]ho_proc_sub_congr [lemma, in PiCalc.hoaspack]
ho_proc_ext [axiom, in PiCalc.hoaspack]
ho_proc_exp [axiom, in PiCalc.hoaspack]
ho2_proc_exp [axiom, in PiCalc.hoaspack]
I
IDEM_SUM [lemma, in PiCalc.alglaws]ID_PAR [lemma, in PiCalc.alglaws]
ID_SUM [lemma, in PiCalc.alglaws]
IN [constructor, in PiCalc.picalcth]
In [constructor, in PiCalc.picalcth]
Inclus [definition, in PiCalc.picalcth]
IN_S [lemma, in PiCalc.alglaws]
in_pref [constructor, in PiCalc.picalcth]
isin [inductive, in PiCalc.picalcth]
isin_to_notin [lemma, in PiCalc.picalcth]
isin_out3 [constructor, in PiCalc.picalcth]
isin_out2 [constructor, in PiCalc.picalcth]
isin_out1 [constructor, in PiCalc.picalcth]
isin_in2 [constructor, in PiCalc.picalcth]
isin_in1 [constructor, in PiCalc.picalcth]
isin_mismatch3 [constructor, in PiCalc.picalcth]
isin_mismatch2 [constructor, in PiCalc.picalcth]
isin_mismatch1 [constructor, in PiCalc.picalcth]
isin_match3 [constructor, in PiCalc.picalcth]
isin_match2 [constructor, in PiCalc.picalcth]
isin_match1 [constructor, in PiCalc.picalcth]
isin_nu [constructor, in PiCalc.picalcth]
isin_sum2 [constructor, in PiCalc.picalcth]
isin_sum1 [constructor, in PiCalc.picalcth]
isin_par2 [constructor, in PiCalc.picalcth]
isin_par1 [constructor, in PiCalc.picalcth]
isin_tau [constructor, in PiCalc.picalcth]
isin_bang [constructor, in PiCalc.picalcth]
L
LEM_name [lemma, in PiCalc.picalcth]LEM_OC [axiom, in PiCalc.picalcth]
L3 [lemma, in PiCalc.basiclemmata]
L3bis [lemma, in PiCalc.basiclemmata]
L6 [lemma, in PiCalc.basiclemmata]
L6_Light [lemma, in PiCalc.basiclemmata]
M
MATCH_S [lemma, in PiCalc.alglaws]match_ [constructor, in PiCalc.picalcth]
MATCH1 [lemma, in PiCalc.alglaws]
MATCH2 [lemma, in PiCalc.alglaws]
mismatch [constructor, in PiCalc.picalcth]
MISMATCH_S [lemma, in PiCalc.alglaws]
MISMATCH1 [lemma, in PiCalc.alglaws]
MISMATCH2 [lemma, in PiCalc.alglaws]
monotonicity [section, in PiCalc.hoaspack]
MPW_Lemma6 [section, in PiCalc.basiclemmata]
MPW_Lemma3 [section, in PiCalc.basiclemmata]
MPW_Lemma1 [section, in PiCalc.basiclemmata]
N
name [axiom, in PiCalc.picalcth]nil [constructor, in PiCalc.picalcth]
Nlist [inductive, in PiCalc.picalcth]
Nlist_notin_cons [constructor, in PiCalc.picalcth]
Nlist_notin_empty [constructor, in PiCalc.picalcth]
Nlist_notin [inductive, in PiCalc.picalcth]
notin [inductive, in PiCalc.picalcth]
notin_to_isin [lemma, in PiCalc.picalcth]
notin_out [constructor, in PiCalc.picalcth]
notin_in [constructor, in PiCalc.picalcth]
notin_mismatch [constructor, in PiCalc.picalcth]
notin_match [constructor, in PiCalc.picalcth]
notin_nu [constructor, in PiCalc.picalcth]
notin_sum [constructor, in PiCalc.picalcth]
notin_par [constructor, in PiCalc.picalcth]
notin_tau [constructor, in PiCalc.picalcth]
notin_bang [constructor, in PiCalc.picalcth]
notin_nil [constructor, in PiCalc.picalcth]
nu [constructor, in PiCalc.picalcth]
NU_PAR2 [lemma, in PiCalc.alglaws]
NU_PAR1 [lemma, in PiCalc.alglaws]
NU_P [lemma, in PiCalc.alglaws]
NU_EXTR [lemma, in PiCalc.alglaws]
NU_E_RW [lemma, in PiCalc.alglaws]
NU_FUN_RW [lemma, in PiCalc.alglaws]
NU_fun [definition, in PiCalc.alglaws]
NU_IN_PREF [lemma, in PiCalc.alglaws]
NU_OUT_PREF [lemma, in PiCalc.alglaws]
NU_TAU_PREF [lemma, in PiCalc.alglaws]
NU_SUM [lemma, in PiCalc.alglaws]
NU_COMM [lemma, in PiCalc.alglaws]
NU_NIL2 [lemma, in PiCalc.alglaws]
NU_NIL1 [lemma, in PiCalc.alglaws]
NU_NIL [lemma, in PiCalc.alglaws]
NU_S [lemma, in PiCalc.alglaws]
O
OPEN [constructor, in PiCalc.picalcth]Op_StBisim_monotone [lemma, in PiCalc.xadequacy]
op_s [constructor, in PiCalc.basiclemmata]
Op_S [inductive, in PiCalc.basiclemmata]
op_nu [constructor, in PiCalc.alglaws]
Op_NU [inductive, in PiCalc.alglaws]
op_par_c [constructor, in PiCalc.alglaws]
Op_PAR_C [inductive, in PiCalc.alglaws]
op_par_s [constructor, in PiCalc.alglaws]
Op_PAR_S [inductive, in PiCalc.alglaws]
op_sb [constructor, in PiCalc.picalcth]
Op_StBisim [inductive, in PiCalc.picalcth]
OUT [constructor, in PiCalc.picalcth]
Out [constructor, in PiCalc.picalcth]
OUT_S [lemma, in PiCalc.alglaws]
out_pref [constructor, in PiCalc.picalcth]
P
par [constructor, in PiCalc.picalcth]PAR_S2 [lemma, in PiCalc.alglaws]
PAR_A_RW [lemma, in PiCalc.alglaws]
PAR_C_RW [lemma, in PiCalc.alglaws]
PAR_C_fun [definition, in PiCalc.alglaws]
PAR_S [lemma, in PiCalc.alglaws]
PAR_S_RW [lemma, in PiCalc.alglaws]
PAR_S_fun [definition, in PiCalc.alglaws]
picalc [library]
picalcth [library]
picalc_xadeq [section, in PiCalc.xadequacy]
picalc_SLB [section, in PiCalc.picalcth]
picalc_LTS [section, in PiCalc.picalcth]
picalc_syntax [section, in PiCalc.picalcth]
PRE_BANG_BTR [lemma, in PiCalc.bangpack]
PRE_ETA_EQ [lemma, in PiCalc.hoaspack]
proc [inductive, in PiCalc.picalcth]
proc_sub_congr [lemma, in PiCalc.hoaspack]
proc_spec [lemma, in PiCalc.hoaspack]
proc_ext [axiom, in PiCalc.hoaspack]
proc_exp [lemma, in PiCalc.hoaspack]
proc_mono [axiom, in PiCalc.hoaspack]
R
REF [lemma, in PiCalc.alglaws]S
sb [constructor, in PiCalc.picalcth]SBPAR_C_TO_SB' [lemma, in PiCalc.alglaws]
sbpar_c [constructor, in PiCalc.alglaws]
SBPAR_C [inductive, in PiCalc.alglaws]
SBPAR_S_TO_SB' [lemma, in PiCalc.alglaws]
sbpar_s [constructor, in PiCalc.alglaws]
SBPAR_S [inductive, in PiCalc.alglaws]
sbupto [constructor, in PiCalc.alglaws]
SBUPTO [inductive, in PiCalc.alglaws]
SB_CF_TAU3 [lemma, in PiCalc.bangpack]
SB_CF_TAU2 [lemma, in PiCalc.bangpack]
SB_CF_TAU1 [lemma, in PiCalc.bangpack]
SB_CF_B_ACT [lemma, in PiCalc.bangpack]
SB_CF_F_ACT [lemma, in PiCalc.bangpack]
SB_R_SB [definition, in PiCalc.alglaws]
Sep_b_act [lemma, in PiCalc.picalcth]
Sep_f_act [lemma, in PiCalc.picalcth]
Sep_proc [lemma, in PiCalc.picalcth]
Soundness [lemma, in PiCalc.xadequacy]
StBisim [inductive, in PiCalc.picalcth]
StBisim' [inductive, in PiCalc.picalcth]
structural_congruence3 [section, in PiCalc.bangpack]
sum [constructor, in PiCalc.picalcth]
SUM_S [lemma, in PiCalc.alglaws]
SYM [lemma, in PiCalc.alglaws]
T
TAU [constructor, in PiCalc.picalcth]tau [constructor, in PiCalc.picalcth]
TAU_S [lemma, in PiCalc.alglaws]
tau_pref [constructor, in PiCalc.picalcth]
TRANS [lemma, in PiCalc.alglaws]
U
unsat [axiom, in PiCalc.picalcth]UpTo [definition, in PiCalc.alglaws]
UPTO_SB' [lemma, in PiCalc.alglaws]
X
xadequacy [library]Variable Index
E
eq_congr.y [in PiCalc.hoaspack]eq_congr.x [in PiCalc.hoaspack]
Library Index
A
alglawsB
bangpackbasiclemmata
H
hoaspackP
picalcpicalcth
X
xadequacyLemma Index
A
ASS_PAR [in PiCalc.alglaws]ASS_SUM [in PiCalc.alglaws]
Aux1 [in PiCalc.basiclemmata]
Aux2 [in PiCalc.basiclemmata]
B
BANG_S [in PiCalc.bangpack]BANG_S_L6 [in PiCalc.bangpack]
BANG_TAU_AUX4 [in PiCalc.bangpack]
BANG_TAU_AUX3 [in PiCalc.bangpack]
BANG_TAU_AUX2 [in PiCalc.bangpack]
BANG_TAU_AUX1 [in PiCalc.bangpack]
BANG_BTR_AUX [in PiCalc.bangpack]
BANG_FTR_AUX [in PiCalc.bangpack]
BANG_TAU [in PiCalc.bangpack]
BANG_BTR [in PiCalc.bangpack]
BANG_OUT [in PiCalc.bangpack]
BANG_UNF [in PiCalc.alglaws]
BisBANG_S_UPTO [in PiCalc.bangpack]
BisBANG_S_FTR2 [in PiCalc.bangpack]
BisBANG_S_bOUT [in PiCalc.bangpack]
BisBANG_S_IN [in PiCalc.bangpack]
BisBANG_S_FTR1 [in PiCalc.bangpack]
BisimL6 [in PiCalc.basiclemmata]
BisNU_E_UPTO [in PiCalc.alglaws]
BisNU_E_FTR2 [in PiCalc.alglaws]
BisNU_E_bOUT [in PiCalc.alglaws]
BisNU_E_IN [in PiCalc.alglaws]
BisNU_E_FTR1 [in PiCalc.alglaws]
BisPAR_A_UPTO [in PiCalc.alglaws]
BisPAR_A_FTR2 [in PiCalc.alglaws]
BisPAR_A_bOUT [in PiCalc.alglaws]
BisPAR_A_IN [in PiCalc.alglaws]
BisPAR_A_FTR1 [in PiCalc.alglaws]
BTR_L3 [in PiCalc.basiclemmata]
BTR_L1 [in PiCalc.basiclemmata]
b_act_sub_congr [in PiCalc.hoaspack]
b_act_spec [in PiCalc.hoaspack]
b_act_exp [in PiCalc.hoaspack]
C
CF_B_ACT_NOTIN [in PiCalc.bangpack]COMM_PAR [in PiCalc.alglaws]
COMM_SUM [in PiCalc.alglaws]
Completeness [in PiCalc.xadequacy]
E
ETA_EQ2 [in PiCalc.hoaspack]ETA_EQ [in PiCalc.hoaspack]
F
FREPL1_NOTIN [in PiCalc.bangpack]FTR_L3 [in PiCalc.basiclemmata]
FTR_L1 [in PiCalc.basiclemmata]
F_REPL4 [in PiCalc.bangpack]
F_REPL3 [in PiCalc.bangpack]
F_REPL2 [in PiCalc.bangpack]
F_REPL1 [in PiCalc.bangpack]
f_act_sub_congr [in PiCalc.hoaspack]
f_act_spec [in PiCalc.hoaspack]
f_act_exp [in PiCalc.hoaspack]
H
ho_proc_sub_congr [in PiCalc.hoaspack]I
IDEM_SUM [in PiCalc.alglaws]ID_PAR [in PiCalc.alglaws]
ID_SUM [in PiCalc.alglaws]
IN_S [in PiCalc.alglaws]
isin_to_notin [in PiCalc.picalcth]
L
LEM_name [in PiCalc.picalcth]L3 [in PiCalc.basiclemmata]
L3bis [in PiCalc.basiclemmata]
L6 [in PiCalc.basiclemmata]
L6_Light [in PiCalc.basiclemmata]
M
MATCH_S [in PiCalc.alglaws]MATCH1 [in PiCalc.alglaws]
MATCH2 [in PiCalc.alglaws]
MISMATCH_S [in PiCalc.alglaws]
MISMATCH1 [in PiCalc.alglaws]
MISMATCH2 [in PiCalc.alglaws]
N
notin_to_isin [in PiCalc.picalcth]NU_PAR2 [in PiCalc.alglaws]
NU_PAR1 [in PiCalc.alglaws]
NU_P [in PiCalc.alglaws]
NU_EXTR [in PiCalc.alglaws]
NU_E_RW [in PiCalc.alglaws]
NU_FUN_RW [in PiCalc.alglaws]
NU_IN_PREF [in PiCalc.alglaws]
NU_OUT_PREF [in PiCalc.alglaws]
NU_TAU_PREF [in PiCalc.alglaws]
NU_SUM [in PiCalc.alglaws]
NU_COMM [in PiCalc.alglaws]
NU_NIL2 [in PiCalc.alglaws]
NU_NIL1 [in PiCalc.alglaws]
NU_NIL [in PiCalc.alglaws]
NU_S [in PiCalc.alglaws]
O
Op_StBisim_monotone [in PiCalc.xadequacy]OUT_S [in PiCalc.alglaws]
P
PAR_S2 [in PiCalc.alglaws]PAR_A_RW [in PiCalc.alglaws]
PAR_C_RW [in PiCalc.alglaws]
PAR_S [in PiCalc.alglaws]
PAR_S_RW [in PiCalc.alglaws]
PRE_BANG_BTR [in PiCalc.bangpack]
PRE_ETA_EQ [in PiCalc.hoaspack]
proc_sub_congr [in PiCalc.hoaspack]
proc_spec [in PiCalc.hoaspack]
proc_exp [in PiCalc.hoaspack]
R
REF [in PiCalc.alglaws]S
SBPAR_C_TO_SB' [in PiCalc.alglaws]SBPAR_S_TO_SB' [in PiCalc.alglaws]
SB_CF_TAU3 [in PiCalc.bangpack]
SB_CF_TAU2 [in PiCalc.bangpack]
SB_CF_TAU1 [in PiCalc.bangpack]
SB_CF_B_ACT [in PiCalc.bangpack]
SB_CF_F_ACT [in PiCalc.bangpack]
Sep_b_act [in PiCalc.picalcth]
Sep_f_act [in PiCalc.picalcth]
Sep_proc [in PiCalc.picalcth]
Soundness [in PiCalc.xadequacy]
SUM_S [in PiCalc.alglaws]
SYM [in PiCalc.alglaws]
T
TAU_S [in PiCalc.alglaws]TRANS [in PiCalc.alglaws]
U
UPTO_SB' [in PiCalc.alglaws]Constructor Index
B
bang [in PiCalc.picalcth]bBANG [in PiCalc.picalcth]
bisbang_s [in PiCalc.bangpack]
bisnu_e_ref [in PiCalc.alglaws]
bisnu_e [in PiCalc.alglaws]
bispar_a [in PiCalc.alglaws]
bispar_c [in PiCalc.alglaws]
bispar_s [in PiCalc.alglaws]
bl6 [in PiCalc.basiclemmata]
bMATCH [in PiCalc.picalcth]
bMISMATCH [in PiCalc.picalcth]
bOut [in PiCalc.picalcth]
bPAR1 [in PiCalc.picalcth]
bPAR2 [in PiCalc.picalcth]
bRES [in PiCalc.picalcth]
bSUM1 [in PiCalc.picalcth]
bSUM2 [in PiCalc.picalcth]
b_act_notin_bOut [in PiCalc.picalcth]
b_act_notin_In [in PiCalc.picalcth]
b_act_isin_bOut [in PiCalc.picalcth]
b_act_isin_In [in PiCalc.picalcth]
C
CLOSE1 [in PiCalc.picalcth]CLOSE2 [in PiCalc.picalcth]
COM1 [in PiCalc.picalcth]
COM2 [in PiCalc.picalcth]
cons [in PiCalc.picalcth]
Co_Ind [in PiCalc.picalcth]
E
empty [in PiCalc.picalcth]F
fBANG [in PiCalc.picalcth]fMATCH [in PiCalc.picalcth]
fMISMATCH [in PiCalc.picalcth]
fPAR1 [in PiCalc.picalcth]
fPAR2 [in PiCalc.picalcth]
fRES [in PiCalc.picalcth]
fSUM1 [in PiCalc.picalcth]
fSUM2 [in PiCalc.picalcth]
f_act_notin_Out [in PiCalc.picalcth]
f_act_notin_tau [in PiCalc.picalcth]
f_act_isin_Out2 [in PiCalc.picalcth]
f_act_isin_Out1 [in PiCalc.picalcth]
I
IN [in PiCalc.picalcth]In [in PiCalc.picalcth]
in_pref [in PiCalc.picalcth]
isin_out3 [in PiCalc.picalcth]
isin_out2 [in PiCalc.picalcth]
isin_out1 [in PiCalc.picalcth]
isin_in2 [in PiCalc.picalcth]
isin_in1 [in PiCalc.picalcth]
isin_mismatch3 [in PiCalc.picalcth]
isin_mismatch2 [in PiCalc.picalcth]
isin_mismatch1 [in PiCalc.picalcth]
isin_match3 [in PiCalc.picalcth]
isin_match2 [in PiCalc.picalcth]
isin_match1 [in PiCalc.picalcth]
isin_nu [in PiCalc.picalcth]
isin_sum2 [in PiCalc.picalcth]
isin_sum1 [in PiCalc.picalcth]
isin_par2 [in PiCalc.picalcth]
isin_par1 [in PiCalc.picalcth]
isin_tau [in PiCalc.picalcth]
isin_bang [in PiCalc.picalcth]
M
match_ [in PiCalc.picalcth]mismatch [in PiCalc.picalcth]
N
nil [in PiCalc.picalcth]Nlist_notin_cons [in PiCalc.picalcth]
Nlist_notin_empty [in PiCalc.picalcth]
notin_out [in PiCalc.picalcth]
notin_in [in PiCalc.picalcth]
notin_mismatch [in PiCalc.picalcth]
notin_match [in PiCalc.picalcth]
notin_nu [in PiCalc.picalcth]
notin_sum [in PiCalc.picalcth]
notin_par [in PiCalc.picalcth]
notin_tau [in PiCalc.picalcth]
notin_bang [in PiCalc.picalcth]
notin_nil [in PiCalc.picalcth]
nu [in PiCalc.picalcth]
O
OPEN [in PiCalc.picalcth]op_s [in PiCalc.basiclemmata]
op_nu [in PiCalc.alglaws]
op_par_c [in PiCalc.alglaws]
op_par_s [in PiCalc.alglaws]
op_sb [in PiCalc.picalcth]
OUT [in PiCalc.picalcth]
Out [in PiCalc.picalcth]
out_pref [in PiCalc.picalcth]
P
par [in PiCalc.picalcth]S
sb [in PiCalc.picalcth]sbpar_c [in PiCalc.alglaws]
sbpar_s [in PiCalc.alglaws]
sbupto [in PiCalc.alglaws]
sum [in PiCalc.picalcth]
T
TAU [in PiCalc.picalcth]tau [in PiCalc.picalcth]
tau_pref [in PiCalc.picalcth]
Axiom Index
B
b_act_ext [in PiCalc.hoaspack]b_act_mono [in PiCalc.hoaspack]
F
f_act_ext [in PiCalc.hoaspack]f_act_mono [in PiCalc.hoaspack]
H
ho_proc_ext [in PiCalc.hoaspack]ho_proc_exp [in PiCalc.hoaspack]
ho2_proc_exp [in PiCalc.hoaspack]
L
LEM_OC [in PiCalc.picalcth]N
name [in PiCalc.picalcth]P
proc_ext [in PiCalc.hoaspack]proc_mono [in PiCalc.hoaspack]
U
unsat [in PiCalc.picalcth]Inductive Index
B
BisBANG_S [in PiCalc.bangpack]BisNU_E [in PiCalc.alglaws]
BisPAR_A [in PiCalc.alglaws]
BisPAR_C [in PiCalc.alglaws]
BisPAR_S [in PiCalc.alglaws]
BL6 [in PiCalc.basiclemmata]
btrans [in PiCalc.picalcth]
b_act_notin [in PiCalc.picalcth]
b_act_isin [in PiCalc.picalcth]
b_act [in PiCalc.picalcth]
F
ftrans [in PiCalc.picalcth]f_act_notin [in PiCalc.picalcth]
f_act_isin [in PiCalc.picalcth]
f_act [in PiCalc.picalcth]
I
isin [in PiCalc.picalcth]N
Nlist [in PiCalc.picalcth]Nlist_notin [in PiCalc.picalcth]
notin [in PiCalc.picalcth]
O
Op_S [in PiCalc.basiclemmata]Op_NU [in PiCalc.alglaws]
Op_PAR_C [in PiCalc.alglaws]
Op_PAR_S [in PiCalc.alglaws]
Op_StBisim [in PiCalc.picalcth]
P
proc [in PiCalc.picalcth]S
SBPAR_C [in PiCalc.alglaws]SBPAR_S [in PiCalc.alglaws]
SBUPTO [in PiCalc.alglaws]
StBisim [in PiCalc.picalcth]
StBisim' [in PiCalc.picalcth]
Section Index
E
eq_congr [in PiCalc.hoaspack]eta [in PiCalc.hoaspack]
expansions [in PiCalc.hoaspack]
M
monotonicity [in PiCalc.hoaspack]MPW_Lemma6 [in PiCalc.basiclemmata]
MPW_Lemma3 [in PiCalc.basiclemmata]
MPW_Lemma1 [in PiCalc.basiclemmata]
P
picalc_xadeq [in PiCalc.xadequacy]picalc_SLB [in PiCalc.picalcth]
picalc_LTS [in PiCalc.picalcth]
picalc_syntax [in PiCalc.picalcth]
S
structural_congruence3 [in PiCalc.bangpack]Definition Index
B
Bfun [in PiCalc.basiclemmata]btrans_ftrans_ind [in PiCalc.basiclemmata]
b_act_notin_ho [in PiCalc.picalcth]
C
cf_tau3 [in PiCalc.bangpack]cf_tau2 [in PiCalc.bangpack]
cf_tau1 [in PiCalc.bangpack]
cf_b_act [in PiCalc.bangpack]
cf_f_act [in PiCalc.bangpack]
F
frepl1 [in PiCalc.bangpack]frepl2 [in PiCalc.bangpack]
frepl3 [in PiCalc.bangpack]
frepl4 [in PiCalc.bangpack]
ftrans_btrans_ind [in PiCalc.basiclemmata]
f_act_notin_ho [in PiCalc.picalcth]
I
Inclus [in PiCalc.picalcth]N
NU_fun [in PiCalc.alglaws]P
PAR_C_fun [in PiCalc.alglaws]PAR_S_fun [in PiCalc.alglaws]
S
SB_R_SB [in PiCalc.alglaws]U
UpTo [in PiCalc.alglaws]| 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 | (292 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 | (2 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 | (7 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 | (115 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 | (95 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 | (12 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 | (29 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) |
| 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 | (20 entries) |