| 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 | (1466 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 | (2 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 | (7 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 | (1 entry) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (673 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 | (41 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 | (405 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 | (75 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (69 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 | (134 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 | (34 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 | (1 entry) |
| 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 | (14 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 | (10 entries) |
Global Index
A
admit [definition, in SfLib]ai_later [constructor, in SfLib]
ai_here [constructor, in SfLib]
Algebraic [section, in CCSSeqSemaphore]
all [constructor, in CharacteristicLogics]
andb_true [lemma, in SfLib]
andb_true_elim2 [lemma, in SfLib]
andb_true_elim1 [lemma, in SfLib]
appears_in [inductive, in SfLib]
app_inv [lemma, in Util]
app_split3 [lemma, in Util]
B
beq_id_sym [lemma, in SfLib]beq_id_false_not_eq [lemma, in SfLib]
beq_id_eq [lemma, in SfLib]
beq_id_refl [lemma, in SfLib]
beq_id [definition, in SfLib]
beq_nat_sym [lemma, in SfLib]
BisimTheory [library]
Bisimulation [section, in BisimTheory]
Bisimulation.lts [variable, in BisimTheory]
ble_nat_false [lemma, in SfLib]
ble_nat_true [lemma, in SfLib]
ble_nat [definition, in SfLib]
bn [definition, in CCSSeqSemaphore]
bnl [definition, in Labels]
bot [constructor, in CharacteristicLogics]
botA [definition, in CharacteristicLogics]
botA_correct [lemma, in CharacteristicLogics]
boxer [constructor, in LibTactics]
Boxer [inductive, in LibTactics]
C
CCSSeqSemaphore [library]CharacteristicLogics [library]
combine_app [lemma, in Util]
combine_nil2 [lemma, in Util]
Congruence [section, in CCSSeqSemaphore]
conj [constructor, in CharacteristicLogics]
contrasimilar [definition, in BisimTheory]
contrasimulation [definition, in BisimTheory]
ContrasimulationAlgebraic [section, in CCSSeqSemaphore]
ContrasimulationCongruence [section, in CCSSeqSemaphore]
contrasimulation_symm_weak_bisimulation [lemma, in BisimTheory]
contrasimulation_id [lemma, in BisimTheory]
contrasimulation_flip [lemma, in BisimTheory]
contrasimulation_lstep [lemma, in BisimTheory]
contrasimulation_tstep [lemma, in BisimTheory]
contrasimulation_step_star [lemma, in BisimTheory]
converges [definition, in CCSSeqSemaphore]
converges_term_impl [lemma, in CCSSeqSemaphore]
converges_step_star [lemma, in CCSSeqSemaphore]
converges_nil [lemma, in CCSSeqSemaphore]
converges_converges'_equiv [lemma, in CCSSeqSemaphore]
converges' [definition, in CCSSeqSemaphore]
count_occ_nIn [lemma, in Util]
coupled_simulation_flipping_id [lemma, in BisimTheory]
coupled_similar_equiv [lemma, in BisimTheory]
coupled_similar [definition, in BisimTheory]
coupled_similar' [definition, in BisimTheory]
coupled_simulation_flipping [definition, in BisimTheory]
csim_hml [lemma, in CharacteristicLogics]
csim_hmlE [lemma, in CharacteristicLogics]
csim_hmlA [lemma, in CharacteristicLogics]
csim_trace_equivalent [lemma, in BisimTheory]
csim_stable_bisim [lemma, in BisimTheory]
csim_symm [lemma, in BisimTheory]
csim_trans [lemma, in BisimTheory]
csim_pcsim2 [lemma, in BisimTheory]
csim_pcsim1 [lemma, in BisimTheory]
csim_refl [lemma, in BisimTheory]
csim_seq_par_simpl [lemma, in CCSSeqSemaphore]
csim_seq_par [lemma, in CCSSeqSemaphore]
csim_rep [lemma, in CCSSeqSemaphore]
csim_res_list [lemma, in CCSSeqSemaphore]
csim_internal_sum [lemma, in CCSSeqSemaphore]
csim_stable_sum [lemma, in CCSSeqSemaphore]
csim_res [lemma, in CCSSeqSemaphore]
csim_out [lemma, in CCSSeqSemaphore]
csim_in [lemma, in CCSSeqSemaphore]
csim_act [lemma, in CCSSeqSemaphore]
csim_par [lemma, in CCSSeqSemaphore]
csim_parR [lemma, in CCSSeqSemaphore]
csim_parL [lemma, in CCSSeqSemaphore]
csim_seq [lemma, in CCSSeqSemaphore]
csim_seq2 [lemma, in CCSSeqSemaphore]
csim_seq1 [lemma, in CCSSeqSemaphore]
csim_intro_tau [lemma, in CCSSeqSemaphore]
csim_sum_comm [lemma, in CCSSeqSemaphore]
csim_par_assoc [lemma, in CCSSeqSemaphore]
csim_seq_assoc [lemma, in CCSSeqSemaphore]
csim_par_nil2 [lemma, in CCSSeqSemaphore]
csim_par_nil1 [lemma, in CCSSeqSemaphore]
csim_par_swap [lemma, in CCSSeqSemaphore]
cssim_csim [lemma, in BisimTheory]
cssim_coupled_simulation_flipping [lemma, in BisimTheory]
cssim_pcssim2 [lemma, in BisimTheory]
cssim_pcssim1 [lemma, in BisimTheory]
cssim_refl [lemma, in BisimTheory]
cssim_symm [lemma, in BisimTheory]
D
deterministic_lts [definition, in LabeledTransitionSystems]deterministic_internal_choice [definition, in BisimTheory]
det_internal_choice_csim_wbisim [lemma, in BisimTheory]
det_internal_choice_pcsim_wbisim [lemma, in BisimTheory]
det_internal_choice_pcsim_symm [lemma, in BisimTheory]
disj [constructor, in CharacteristicLogics]
dup_lemma [lemma, in LibTactics]
E
ebisim_trans_false.ebisim_trans_false [lemma, in Examples]ebisim_trans_false.ebisimPR_false [lemma, in Examples]
ebisim_trans_false.step_star_s2_out [lemma, in Examples]
ebisim_trans_false.esimRQ [lemma, in Examples]
ebisim_trans_false.esimPQ [lemma, in Examples]
ebisim_trans_false.nat_div2 [lemma, in Examples]
ebisim_trans_false.step_star_s2_inv [lemma, in Examples]
ebisim_trans_false.step_star_s2_tau [lemma, in Examples]
ebisim_trans_false.step_star_s1_inv [lemma, in Examples]
ebisim_trans_false.step_star_s1_tau [lemma, in Examples]
ebisim_trans_false.step_star_s0_inv [lemma, in Examples]
ebisim_trans_false.Lemmas [section, in Examples]
ebisim_trans_false.lts [definition, in Examples]
ebisim_trans_false.s_s1' [constructor, in Examples]
ebisim_trans_false.s_s1 [constructor, in Examples]
ebisim_trans_false.s_sR [constructor, in Examples]
ebisim_trans_false.s_sL [constructor, in Examples]
ebisim_trans_false.lstep [inductive, in Examples]
ebisim_trans_false.s_t1' [constructor, in Examples]
ebisim_trans_false.s_t1 [constructor, in Examples]
ebisim_trans_false.s_t2 [constructor, in Examples]
ebisim_trans_false.tstep [inductive, in Examples]
ebisim_trans_false.s0 [constructor, in Examples]
ebisim_trans_false.s1' [constructor, in Examples]
ebisim_trans_false.s2 [constructor, in Examples]
ebisim_trans_false.s1 [constructor, in Examples]
ebisim_trans_false.state [inductive, in Examples]
ebisim_trans_false [module, in Examples]
ebisim_csim [lemma, in BisimTheory]
ebisim_symm [lemma, in BisimTheory]
ebisim_eventual_simulation2 [lemma, in BisimTheory]
ebisim_eventual_simulation1 [lemma, in BisimTheory]
ebisim_one_way_termination_sensitive2 [lemma, in BisimTheory]
ebisim_one_way_termination_sensitive1 [lemma, in BisimTheory]
ebisim_refl [lemma, in BisimTheory]
empty [definition, in SfLib]
empty_relation [inductive, in SfLib]
equatesLemma [section, in LibTactics]
equatesLemma.A0 [variable, in LibTactics]
equatesLemma.A1 [variable, in LibTactics]
equatesLemma.A2 [variable, in LibTactics]
equatesLemma.A3 [variable, in LibTactics]
equatesLemma.A4 [variable, in LibTactics]
equatesLemma.A5 [variable, in LibTactics]
equatesLemma.A6 [variable, in LibTactics]
equates_6 [lemma, in LibTactics]
equates_5 [lemma, in LibTactics]
equates_4 [lemma, in LibTactics]
equates_3 [lemma, in LibTactics]
equates_2 [lemma, in LibTactics]
equates_1 [lemma, in LibTactics]
equates_0 [lemma, in LibTactics]
eq' [definition, in LibTactics]
esim_trans [lemma, in BisimTheory]
esim_par_simulation [lemma, in BisimTheory]
esim_weak_simulation [lemma, in BisimTheory]
esim_one_way_termination_sensitive [lemma, in BisimTheory]
esim_ebisim2 [lemma, in BisimTheory]
esim_ebisim1 [lemma, in BisimTheory]
esim_refl [lemma, in BisimTheory]
esim_seq_par_simpl [lemma, in CCSSeqSemaphore]
esim_seq_par [lemma, in CCSSeqSemaphore]
esim_rep [lemma, in CCSSeqSemaphore]
esim_act [lemma, in CCSSeqSemaphore]
esim_internal_sum [lemma, in CCSSeqSemaphore]
esim_stable_sum [lemma, in CCSSeqSemaphore]
esim_res_list [lemma, in CCSSeqSemaphore]
esim_res [lemma, in CCSSeqSemaphore]
esim_par [lemma, in CCSSeqSemaphore]
esim_parR [lemma, in CCSSeqSemaphore]
esim_parL [lemma, in CCSSeqSemaphore]
esim_seq [lemma, in CCSSeqSemaphore]
esim_seq2 [lemma, in CCSSeqSemaphore]
esim_seq1 [lemma, in CCSSeqSemaphore]
esim_list_same_split [lemma, in CCSSeqSemaphore]
esim_list_single [lemma, in CCSSeqSemaphore]
esim_list_nil [lemma, in CCSSeqSemaphore]
esim_list_app [lemma, in CCSSeqSemaphore]
esim_list_cons [lemma, in CCSSeqSemaphore]
esim_list [definition, in CCSSeqSemaphore]
ev [inductive, in SfLib]
eventually_bisimilar [definition, in BisimTheory]
eventually_similar [definition, in BisimTheory]
EventualSimulationCompositionality [section, in CCSSeqSemaphore]
eventual_simulation_lstep [lemma, in BisimTheory]
eventual_simulation_tstep [lemma, in BisimTheory]
eventual_simulation_step_star [lemma, in BisimTheory]
eventual_simulation [definition, in BisimTheory]
ev_not_ev_S [lemma, in SfLib]
ev_SS [constructor, in SfLib]
ev_0 [constructor, in SfLib]
ExampleA [module, in Examples]
ExampleA.csim_false [lemma, in Examples]
ExampleA.cssim_false [lemma, in Examples]
ExampleA.label [definition, in Examples]
ExampleA.Lemmas [section, in Examples]
ExampleA.lstep [inductive, in Examples]
ExampleA.lstep_gi [constructor, in Examples]
ExampleA.lstep_fh [constructor, in Examples]
ExampleA.lstep_eg [constructor, in Examples]
ExampleA.lstep_ef [constructor, in Examples]
ExampleA.lstep_bd [constructor, in Examples]
ExampleA.lstep_bc [constructor, in Examples]
ExampleA.lstep_ab [constructor, in Examples]
ExampleA.lts [definition, in Examples]
ExampleA.pbisim_false2 [lemma, in Examples]
ExampleA.pbisim_false1 [lemma, in Examples]
ExampleA.Sa [constructor, in Examples]
ExampleA.Sb [constructor, in Examples]
ExampleA.Sc [constructor, in Examples]
ExampleA.Sd [constructor, in Examples]
ExampleA.Se [constructor, in Examples]
ExampleA.Sf [constructor, in Examples]
ExampleA.Sg [constructor, in Examples]
ExampleA.Sh [constructor, in Examples]
ExampleA.Si [constructor, in Examples]
ExampleA.state [inductive, in Examples]
ExampleA.tstep [inductive, in Examples]
ExampleA.wbisim_false [lemma, in Examples]
ExampleB [module, in Examples]
ExampleB_Full.csim_true [lemma, in Examples]
ExampleB_Full.pbisim_false1 [lemma, in Examples]
ExampleB_Full.pbisim_true2 [lemma, in Examples]
ExampleB_Full.Rp_ex [constructor, in Examples]
ExampleB_Full.Rp_dw [constructor, in Examples]
ExampleB_Full.Rp_cx [constructor, in Examples]
ExampleB_Full.Rp_bw [constructor, in Examples]
ExampleB_Full.Rp_zz [constructor, in Examples]
ExampleB_Full.Rp_yy [constructor, in Examples]
ExampleB_Full.Rp_xx [constructor, in Examples]
ExampleB_Full.Rp_ww [constructor, in Examples]
ExampleB_Full.Rp_init [constructor, in Examples]
ExampleB_Full.Rp [inductive, in Examples]
ExampleB_Full.cssim_false [lemma, in Examples]
ExampleB_Full.wbisim_false [lemma, in Examples]
ExampleB_Full.Lemmas [section, in Examples]
ExampleB_Full.lts [definition, in Examples]
ExampleB_Full.is_halted [definition, in Examples]
ExampleB_Full.tstep_Qqz [constructor, in Examples]
ExampleB_Full.tstep_Qpy [constructor, in Examples]
ExampleB_Full.tstep_Qoz [constructor, in Examples]
ExampleB_Full.tstep_Qny [constructor, in Examples]
ExampleB_Full.tstep_Qmz [constructor, in Examples]
ExampleB_Full.tstep_Qly [constructor, in Examples]
ExampleB_Full.tstep_Qkx [constructor, in Examples]
ExampleB_Full.tstep_Qjx [constructor, in Examples]
ExampleB_Full.tstep_Qiw [constructor, in Examples]
ExampleB_Full.tstep_Qhw [constructor, in Examples]
ExampleB_Full.tstep_Qgx [constructor, in Examples]
ExampleB_Full.tstep_Qfw [constructor, in Examples]
ExampleB_Full.tstep_Qem [constructor, in Examples]
ExampleB_Full.tstep_Qel [constructor, in Examples]
ExampleB_Full.tstep_Qdk [constructor, in Examples]
ExampleB_Full.tstep_Qdj [constructor, in Examples]
ExampleB_Full.tstep_Qci [constructor, in Examples]
ExampleB_Full.tstep_Qch [constructor, in Examples]
ExampleB_Full.tstep_Qbg [constructor, in Examples]
ExampleB_Full.tstep_Qbf [constructor, in Examples]
ExampleB_Full.tstep_Qad [constructor, in Examples]
ExampleB_Full.tstep_Qac [constructor, in Examples]
ExampleB_Full.tstep_Qab [constructor, in Examples]
ExampleB_Full.tstep_Pex [constructor, in Examples]
ExampleB_Full.tstep_Pdw [constructor, in Examples]
ExampleB_Full.tstep_Pce [constructor, in Examples]
ExampleB_Full.tstep_Pbd [constructor, in Examples]
ExampleB_Full.tstep_Pac [constructor, in Examples]
ExampleB_Full.tstep_Pab [constructor, in Examples]
ExampleB_Full.tstep [inductive, in Examples]
ExampleB_Full.lstep_Qjq [constructor, in Examples]
ExampleB_Full.lstep_Qhp [constructor, in Examples]
ExampleB_Full.lstep_Qgo [constructor, in Examples]
ExampleB_Full.lstep_Qfn [constructor, in Examples]
ExampleB_Full.lstep_Qbe [constructor, in Examples]
ExampleB_Full.lstep_Sxz [constructor, in Examples]
ExampleB_Full.lstep_Swy [constructor, in Examples]
ExampleB_Full.lstep [inductive, in Examples]
ExampleB_Full.label [definition, in Examples]
ExampleB_Full.Sz [constructor, in Examples]
ExampleB_Full.Sy [constructor, in Examples]
ExampleB_Full.Sx [constructor, in Examples]
ExampleB_Full.Sw [constructor, in Examples]
ExampleB_Full.Qq [constructor, in Examples]
ExampleB_Full.Qp [constructor, in Examples]
ExampleB_Full.Qo [constructor, in Examples]
ExampleB_Full.Qn [constructor, in Examples]
ExampleB_Full.Qm [constructor, in Examples]
ExampleB_Full.Ql [constructor, in Examples]
ExampleB_Full.Qk [constructor, in Examples]
ExampleB_Full.Qj [constructor, in Examples]
ExampleB_Full.Qi [constructor, in Examples]
ExampleB_Full.Qh [constructor, in Examples]
ExampleB_Full.Qg [constructor, in Examples]
ExampleB_Full.Qf [constructor, in Examples]
ExampleB_Full.Qe [constructor, in Examples]
ExampleB_Full.Qd [constructor, in Examples]
ExampleB_Full.Qc [constructor, in Examples]
ExampleB_Full.Qb [constructor, in Examples]
ExampleB_Full.Qa [constructor, in Examples]
ExampleB_Full.Pe [constructor, in Examples]
ExampleB_Full.Pd [constructor, in Examples]
ExampleB_Full.Pc [constructor, in Examples]
ExampleB_Full.Pb [constructor, in Examples]
ExampleB_Full.Pa [constructor, in Examples]
ExampleB_Full.state [inductive, in Examples]
ExampleB_Full [module, in Examples]
ExampleB' [module, in Examples]
ExampleB'.csim_true [lemma, in Examples]
ExampleB'.cssim_false [lemma, in Examples]
ExampleB'.is_halted [definition, in Examples]
ExampleB'.label [definition, in Examples]
ExampleB'.Lemmas [section, in Examples]
ExampleB'.lstep [inductive, in Examples]
ExampleB'.lstep_df [constructor, in Examples]
ExampleB'.lstep_ce [constructor, in Examples]
ExampleB'.lstep_ab [constructor, in Examples]
ExampleB'.lts [definition, in Examples]
ExampleB'.pbisim_false2 [lemma, in Examples]
ExampleB'.pbisim_true1 [lemma, in Examples]
ExampleB'.Rp [inductive, in Examples]
ExampleB'.Rp_dd [constructor, in Examples]
ExampleB'.Rp_cc [constructor, in Examples]
ExampleB'.Rp_hh [constructor, in Examples]
ExampleB'.Rp_gg [constructor, in Examples]
ExampleB'.Rp_ff [constructor, in Examples]
ExampleB'.Rp_ee [constructor, in Examples]
ExampleB'.Rp_ia [constructor, in Examples]
ExampleB'.Sa [constructor, in Examples]
ExampleB'.Sb [constructor, in Examples]
ExampleB'.Sc [constructor, in Examples]
ExampleB'.Sd [constructor, in Examples]
ExampleB'.Se [constructor, in Examples]
ExampleB'.Sf [constructor, in Examples]
ExampleB'.Sg [constructor, in Examples]
ExampleB'.Sh [constructor, in Examples]
ExampleB'.Si [constructor, in Examples]
ExampleB'.state [inductive, in Examples]
ExampleB'.tstep [inductive, in Examples]
ExampleB'.tstep_id [constructor, in Examples]
ExampleB'.tstep_ic [constructor, in Examples]
ExampleB'.tstep_dh [constructor, in Examples]
ExampleB'.tstep_cg [constructor, in Examples]
ExampleB'.tstep_bf [constructor, in Examples]
ExampleB'.tstep_be [constructor, in Examples]
ExampleB'.tstep_ad [constructor, in Examples]
ExampleB'.tstep_ac [constructor, in Examples]
ExampleB'.wbisim_false [lemma, in Examples]
ExampleB.csim_true [lemma, in Examples]
ExampleB.csim_false [lemma, in Examples]
ExampleB.is_halted [definition, in Examples]
ExampleB.label [definition, in Examples]
ExampleB.Lemmas [section, in Examples]
ExampleB.lstep [inductive, in Examples]
ExampleB.lstep_if [constructor, in Examples]
ExampleB.lstep_he [constructor, in Examples]
ExampleB.lstep_df [constructor, in Examples]
ExampleB.lstep_ce [constructor, in Examples]
ExampleB.lstep_ab [constructor, in Examples]
ExampleB.lts [definition, in Examples]
ExampleB.pbisim_false2 [lemma, in Examples]
ExampleB.pbisim_true1 [lemma, in Examples]
ExampleB.Rp [inductive, in Examples]
ExampleB.Rp_id [constructor, in Examples]
ExampleB.Rp_hc [constructor, in Examples]
ExampleB.Rp_dd [constructor, in Examples]
ExampleB.Rp_cc [constructor, in Examples]
ExampleB.Rp_ff [constructor, in Examples]
ExampleB.Rp_ee [constructor, in Examples]
ExampleB.Rp_ga [constructor, in Examples]
ExampleB.Sa [constructor, in Examples]
ExampleB.Sb [constructor, in Examples]
ExampleB.Sc [constructor, in Examples]
ExampleB.Sd [constructor, in Examples]
ExampleB.Se [constructor, in Examples]
ExampleB.Sf [constructor, in Examples]
ExampleB.Sg [constructor, in Examples]
ExampleB.Sh [constructor, in Examples]
ExampleB.Si [constructor, in Examples]
ExampleB.state [inductive, in Examples]
ExampleB.tstep [inductive, in Examples]
ExampleB.tstep_gi [constructor, in Examples]
ExampleB.tstep_gh [constructor, in Examples]
ExampleB.tstep_bf [constructor, in Examples]
ExampleB.tstep_be [constructor, in Examples]
ExampleB.tstep_ad [constructor, in Examples]
ExampleB.tstep_ac [constructor, in Examples]
ExampleB.wbisim_false [lemma, in Examples]
ExampleC [module, in Examples]
ExampleC.csim_false [lemma, in Examples]
ExampleC.cssim_false [lemma, in Examples]
ExampleC.label [definition, in Examples]
ExampleC.Lemmas [section, in Examples]
ExampleC.lstep [inductive, in Examples]
ExampleC.lstep_fh [constructor, in Examples]
ExampleC.lstep_eg [constructor, in Examples]
ExampleC.lstep_ef [constructor, in Examples]
ExampleC.lstep_bc [constructor, in Examples]
ExampleC.lstep_ab [constructor, in Examples]
ExampleC.lts [definition, in Examples]
ExampleC.pbisim_false1 [lemma, in Examples]
ExampleC.Sa [constructor, in Examples]
ExampleC.Sb [constructor, in Examples]
ExampleC.Sc [constructor, in Examples]
ExampleC.Sd [constructor, in Examples]
ExampleC.Se [constructor, in Examples]
ExampleC.Sf [constructor, in Examples]
ExampleC.Sg [constructor, in Examples]
ExampleC.Sh [constructor, in Examples]
ExampleC.state [inductive, in Examples]
ExampleC.tstep [inductive, in Examples]
ExampleC.wbisim_false2 [lemma, in Examples]
ExampleC.wbisim_false [lemma, in Examples]
ExampleD [module, in Examples]
ExampleD.coffee [constructor, in Examples]
ExampleD.csim_false [lemma, in Examples]
ExampleD.cssim_false [lemma, in Examples]
ExampleD.label [inductive, in Examples]
ExampleD.Lemmas [section, in Examples]
ExampleD.lstep [inductive, in Examples]
ExampleD.lstep_ie [constructor, in Examples]
ExampleD.lstep_he [constructor, in Examples]
ExampleD.lstep_gi [constructor, in Examples]
ExampleD.lstep_fh [constructor, in Examples]
ExampleD.lstep_eg [constructor, in Examples]
ExampleD.lstep_ef [constructor, in Examples]
ExampleD.lstep_da [constructor, in Examples]
ExampleD.lstep_ca [constructor, in Examples]
ExampleD.lstep_bd [constructor, in Examples]
ExampleD.lstep_bc [constructor, in Examples]
ExampleD.lstep_ab [constructor, in Examples]
ExampleD.lts [definition, in Examples]
ExampleD.par_bisim_false2 [lemma, in Examples]
ExampleD.pay_cent [constructor, in Examples]
ExampleD.pbisim_false1 [lemma, in Examples]
ExampleD.pick_coffee [constructor, in Examples]
ExampleD.pick_tea [constructor, in Examples]
ExampleD.Sa [constructor, in Examples]
ExampleD.Sb [constructor, in Examples]
ExampleD.Sc [constructor, in Examples]
ExampleD.Sd [constructor, in Examples]
ExampleD.Se [constructor, in Examples]
ExampleD.Sf [constructor, in Examples]
ExampleD.Sg [constructor, in Examples]
ExampleD.Sh [constructor, in Examples]
ExampleD.Si [constructor, in Examples]
ExampleD.state [inductive, in Examples]
ExampleD.tea [constructor, in Examples]
ExampleD.tstep [inductive, in Examples]
ExampleD.wbisim_false [lemma, in Examples]
ExampleE [module, in Examples]
ExampleE.csim_false [lemma, in Examples]
ExampleE.cssim_false [lemma, in Examples]
ExampleE.label [definition, in Examples]
ExampleE.Lemmas [section, in Examples]
ExampleE.lstep [inductive, in Examples]
ExampleE.lstep_ec [constructor, in Examples]
ExampleE.lstep_ed [constructor, in Examples]
ExampleE.lstep_bd [constructor, in Examples]
ExampleE.lstep_ac [constructor, in Examples]
ExampleE.lts [definition, in Examples]
ExampleE.pbisim_false2 [lemma, in Examples]
ExampleE.pbisim_false1 [lemma, in Examples]
ExampleE.Sa [constructor, in Examples]
ExampleE.Sb [constructor, in Examples]
ExampleE.Sc [constructor, in Examples]
ExampleE.Sd [constructor, in Examples]
ExampleE.Se [constructor, in Examples]
ExampleE.state [inductive, in Examples]
ExampleE.tstep [inductive, in Examples]
ExampleE.tstep_ab [constructor, in Examples]
ExampleE.wbisim_false [lemma, in Examples]
ExampleF [module, in Examples]
ExampleF.csim_true [lemma, in Examples]
ExampleF.cssim_true [lemma, in Examples]
ExampleF.is_halted [definition, in Examples]
ExampleF.label [definition, in Examples]
ExampleF.Lemmas [section, in Examples]
ExampleF.lstep [inductive, in Examples]
ExampleF.lstep_lg [constructor, in Examples]
ExampleF.lstep_kf [constructor, in Examples]
ExampleF.lstep_ie [constructor, in Examples]
ExampleF.lstep_dg [constructor, in Examples]
ExampleF.lstep_cf [constructor, in Examples]
ExampleF.lstep_be [constructor, in Examples]
ExampleF.lts [definition, in Examples]
ExampleF.pbisim_false2 [lemma, in Examples]
ExampleF.pbisim_false1 [lemma, in Examples]
ExampleF.Rc1 [inductive, in Examples]
ExampleF.Rc1_cj [constructor, in Examples]
ExampleF.Rc1_gg [constructor, in Examples]
ExampleF.Rc1_ff [constructor, in Examples]
ExampleF.Rc1_ee [constructor, in Examples]
ExampleF.Rc1_dl [constructor, in Examples]
ExampleF.Rc1_ck [constructor, in Examples]
ExampleF.Rc1_bi [constructor, in Examples]
ExampleF.Rc1_ah [constructor, in Examples]
ExampleF.Rc2 [inductive, in Examples]
ExampleF.Rc2_aj [constructor, in Examples]
ExampleF.Rc2_gg [constructor, in Examples]
ExampleF.Rc2_ff [constructor, in Examples]
ExampleF.Rc2_ee [constructor, in Examples]
ExampleF.Rc2_dl [constructor, in Examples]
ExampleF.Rc2_ck [constructor, in Examples]
ExampleF.Rc2_bi [constructor, in Examples]
ExampleF.Rc2_ah [constructor, in Examples]
ExampleF.Rd [inductive, in Examples]
ExampleF.Rd_gg [constructor, in Examples]
ExampleF.Rd_ff [constructor, in Examples]
ExampleF.Rd_ee [constructor, in Examples]
ExampleF.Rd_ld [constructor, in Examples]
ExampleF.Rd_kc [constructor, in Examples]
ExampleF.Rd_ib [constructor, in Examples]
ExampleF.Rd_dl [constructor, in Examples]
ExampleF.Rd_ck [constructor, in Examples]
ExampleF.Rd_cj [constructor, in Examples]
ExampleF.Rd_bi [constructor, in Examples]
ExampleF.Rd_ah [constructor, in Examples]
ExampleF.Rd_ha [constructor, in Examples]
ExampleF.Sa [constructor, in Examples]
ExampleF.Sb [constructor, in Examples]
ExampleF.Sc [constructor, in Examples]
ExampleF.Sd [constructor, in Examples]
ExampleF.Se [constructor, in Examples]
ExampleF.Sf [constructor, in Examples]
ExampleF.Sg [constructor, in Examples]
ExampleF.Sh [constructor, in Examples]
ExampleF.Si [constructor, in Examples]
ExampleF.Sj [constructor, in Examples]
ExampleF.Sk [constructor, in Examples]
ExampleF.Sl [constructor, in Examples]
ExampleF.state [inductive, in Examples]
ExampleF.tstep [inductive, in Examples]
ExampleF.tstep_jl [constructor, in Examples]
ExampleF.tstep_jk [constructor, in Examples]
ExampleF.tstep_hj [constructor, in Examples]
ExampleF.tstep_hi [constructor, in Examples]
ExampleF.tstep_ad [constructor, in Examples]
ExampleF.tstep_ac [constructor, in Examples]
ExampleF.tstep_ab [constructor, in Examples]
ExampleF.wbisim_false [lemma, in Examples]
ExampleG [module, in Examples]
ExampleG.csim_true [lemma, in Examples]
ExampleG.cssim_true [lemma, in Examples]
ExampleG.is_halted [definition, in Examples]
ExampleG.label [definition, in Examples]
ExampleG.Lemmas [section, in Examples]
ExampleG.lstep [inductive, in Examples]
ExampleG.lstep_dg [constructor, in Examples]
ExampleG.lstep_cf [constructor, in Examples]
ExampleG.lstep_be [constructor, in Examples]
ExampleG.lts [definition, in Examples]
ExampleG.pbisim_true2 [lemma, in Examples]
ExampleG.pbisim_false1 [lemma, in Examples]
ExampleG.Rc1 [inductive, in Examples]
ExampleG.Rc1_cj [constructor, in Examples]
ExampleG.Rc1_gg [constructor, in Examples]
ExampleG.Rc1_ff [constructor, in Examples]
ExampleG.Rc1_ee [constructor, in Examples]
ExampleG.Rc1_dd [constructor, in Examples]
ExampleG.Rc1_cc [constructor, in Examples]
ExampleG.Rc1_bb [constructor, in Examples]
ExampleG.Rc1_ah [constructor, in Examples]
ExampleG.Rc2 [inductive, in Examples]
ExampleG.Rc2_aj [constructor, in Examples]
ExampleG.Rc2_gg [constructor, in Examples]
ExampleG.Rc2_ff [constructor, in Examples]
ExampleG.Rc2_ee [constructor, in Examples]
ExampleG.Rc2_dd [constructor, in Examples]
ExampleG.Rc2_cc [constructor, in Examples]
ExampleG.Rc2_bb [constructor, in Examples]
ExampleG.Rc2_ah [constructor, in Examples]
ExampleG.Rp [inductive, in Examples]
ExampleG.Rp_gg [constructor, in Examples]
ExampleG.Rp_ff [constructor, in Examples]
ExampleG.Rp_ee [constructor, in Examples]
ExampleG.Rp_dd [constructor, in Examples]
ExampleG.Rp_cc [constructor, in Examples]
ExampleG.Rp_bb [constructor, in Examples]
ExampleG.Rp_ah [constructor, in Examples]
ExampleG.Sa [constructor, in Examples]
ExampleG.Sb [constructor, in Examples]
ExampleG.Sc [constructor, in Examples]
ExampleG.Sd [constructor, in Examples]
ExampleG.Se [constructor, in Examples]
ExampleG.Sf [constructor, in Examples]
ExampleG.Sg [constructor, in Examples]
ExampleG.Sh [constructor, in Examples]
ExampleG.Sj [constructor, in Examples]
ExampleG.state [inductive, in Examples]
ExampleG.tstep [inductive, in Examples]
ExampleG.tstep_jd [constructor, in Examples]
ExampleG.tstep_jc [constructor, in Examples]
ExampleG.tstep_hj [constructor, in Examples]
ExampleG.tstep_hb [constructor, in Examples]
ExampleG.tstep_ad [constructor, in Examples]
ExampleG.tstep_ac [constructor, in Examples]
ExampleG.tstep_ab [constructor, in Examples]
ExampleG.wbisim_false [lemma, in Examples]
Examples [module, in CCSSeqSemaphore]
Examples [library]
Examples.list_lts_S_list_proc [definition, in CCSSeqSemaphore]
Examples.lstep_inv [lemma, in CCSSeqSemaphore]
Examples.step_star_par_tsum2 [lemma, in CCSSeqSemaphore]
Examples.SumPar [module, in CCSSeqSemaphore]
Examples.SumPar.coupled_sim_false [lemma, in CCSSeqSemaphore]
Examples.SumPar.csim_true_O [lemma, in CCSSeqSemaphore]
Examples.SumPar.csim_true [lemma, in CCSSeqSemaphore]
Examples.SumPar.esim_true_O [lemma, in CCSSeqSemaphore]
Examples.SumPar.esim_true [lemma, in CCSSeqSemaphore]
Examples.SumPar.p_par_sum [definition, in CCSSeqSemaphore]
Examples.SumPar.p_sum_par [definition, in CCSSeqSemaphore]
Examples.SumPar.Rd [inductive, in CCSSeqSemaphore]
Examples.SumPar.Rd1 [constructor, in CCSSeqSemaphore]
Examples.SumPar.Rd4 [constructor, in CCSSeqSemaphore]
Examples.SumPar.step_star_app' [lemma, in CCSSeqSemaphore]
Examples.SumPar.wbisim_false [lemma, in CCSSeqSemaphore]
Examples.SumPar.wsim_backwards_false [lemma, in CCSSeqSemaphore]
Examples.SumSum [module, in CCSSeqSemaphore]
Examples.SumSum.coupled_sim_false [lemma, in CCSSeqSemaphore]
Examples.SumSum.csim_true [lemma, in CCSSeqSemaphore]
Examples.SumSum.esim_true [lemma, in CCSSeqSemaphore]
Examples.SumSum.p_sum2 [definition, in CCSSeqSemaphore]
Examples.SumSum.p_sum1 [definition, in CCSSeqSemaphore]
Examples.SumSum.Rd [inductive, in CCSSeqSemaphore]
Examples.SumSum.Rd1 [constructor, in CCSSeqSemaphore]
Examples.SumSum.Rd4 [constructor, in CCSSeqSemaphore]
Examples.SumSum.wbisim_false [lemma, in CCSSeqSemaphore]
Examples.SumSum.wsim_backwards_false [lemma, in CCSSeqSemaphore]
ExampleTactics [module, in Examples]
exists_list_unsatE [lemma, in CharacteristicLogics]
exists_list_unsatA [lemma, in CharacteristicLogics]
ext [constructor, in CharacteristicLogics]
extend [definition, in SfLib]
extend_shadow [lemma, in SfLib]
extend_neq [lemma, in SfLib]
extend_eq [lemma, in SfLib]
ex_falso_quodlibet [lemma, in SfLib]
F
flip_pcsim [lemma, in BisimTheory]flip_pcssim [lemma, in BisimTheory]
fn [definition, in CCSSeqSemaphore]
fnl [definition, in Labels]
fn_in_subset_step_star_res_list_parR [lemma, in CCSSeqSemaphore]
fn_in_subset_step_star_res_list_parL [lemma, in CCSSeqSemaphore]
fn_subset_step_star_res_list_parR_In [lemma, in CCSSeqSemaphore]
fn_subset_step_star_res_list_parL_In [lemma, in CCSSeqSemaphore]
fn_subset_step_star_p_res_list_In [lemma, in CCSSeqSemaphore]
fn_p_res_list [lemma, in CCSSeqSemaphore]
fn_In_res_list1 [lemma, in CCSSeqSemaphore]
fn_in_subset_step_star_parR [lemma, in CCSSeqSemaphore]
fn_in_subset_step_star_parL [lemma, in CCSSeqSemaphore]
fn_subset_step_star_parR_In [lemma, in CCSSeqSemaphore]
fn_subset_step_star_parL_In [lemma, in CCSSeqSemaphore]
fn_step_star_In [lemma, in CCSSeqSemaphore]
fn_out_step_star_In [lemma, in CCSSeqSemaphore]
fn_in_step_star_In [lemma, in CCSSeqSemaphore]
fn_out_step_In [lemma, in CCSSeqSemaphore]
fn_in_step_In [lemma, in CCSSeqSemaphore]
fn_subset_step_star [lemma, in CCSSeqSemaphore]
fn_out_subset_step_star [lemma, in CCSSeqSemaphore]
fn_in_subset_step_star [lemma, in CCSSeqSemaphore]
fn_subset_step [lemma, in CCSSeqSemaphore]
fn_out_subset_step [lemma, in CCSSeqSemaphore]
fn_in_subset_step [lemma, in CCSSeqSemaphore]
fn_in_out_equiv [lemma, in CCSSeqSemaphore]
fn_out [definition, in CCSSeqSemaphore]
fn_in [definition, in CCSSeqSemaphore]
Forall2_list_rep [lemma, in CCSSeqSemaphore]
Forall2_symm [lemma, in CCSSeqSemaphore]
forces [definition, in CharacteristicLogics]
forcesA [definition, in CharacteristicLogics]
forcesE [definition, in CharacteristicLogics]
FreeNameLemmas [section, in CCSSeqSemaphore]
FreeNames [section, in CCSSeqSemaphore]
fst_split_app [lemma, in Util]
fst_split [lemma, in Util]
f_list_disjE [lemma, in CharacteristicLogics]
f_list_conjA [lemma, in CharacteristicLogics]
G
get_step_rep_p' [definition, in CCSSeqSemaphore]H
halted_correct2 [projection, in LabeledTransitionSystems]halted_correct1 [projection, in LabeledTransitionSystems]
halted_converge_pcsim [lemma, in BisimTheory]
halted_pcsim2 [lemma, in BisimTheory]
halted_pcsim1 [lemma, in BisimTheory]
halted_converge_ebisim2 [lemma, in BisimTheory]
halted_converge_ebisim1 [lemma, in BisimTheory]
halted_ebisim2 [lemma, in BisimTheory]
halted_ebisim1 [lemma, in BisimTheory]
halted_converge_esim2 [lemma, in BisimTheory]
halted_converge_esim1 [lemma, in BisimTheory]
halted_esim2 [lemma, in BisimTheory]
halted_esim1 [lemma, in BisimTheory]
halted_converge_pbisim2 [lemma, in BisimTheory]
halted_converge_pbisim1 [lemma, in BisimTheory]
halted_pbisim2 [lemma, in BisimTheory]
halted_pbisim1 [lemma, in BisimTheory]
halted_converge_pcssim1 [lemma, in BisimTheory]
halted_pcssim2 [lemma, in BisimTheory]
halted_pcssim1 [lemma, in BisimTheory]
halted_converge_wbisim2 [lemma, in BisimTheory]
halted_converge_wbisim1 [lemma, in BisimTheory]
halted_wbisim2 [lemma, in BisimTheory]
halted_wbisim1 [lemma, in BisimTheory]
halted_converge_sbisim2 [lemma, in BisimTheory]
halted_converge_sbisim1 [lemma, in BisimTheory]
halted_sbisim2 [lemma, in BisimTheory]
halted_sbisim1 [lemma, in BisimTheory]
HiddenProc [section, in CCSSeqSemaphore]
hidden_fn_step_star_res_list_parL [lemma, in CCSSeqSemaphore]
hidden_fn_step_star_res_list_parR [lemma, in CCSSeqSemaphore]
hidden_fn_seq3 [lemma, in CCSSeqSemaphore]
hidden_fn_step_star_parL [lemma, in CCSSeqSemaphore]
hidden_fn_step_star_parR [lemma, in CCSSeqSemaphore]
hidden_fn_step_star [lemma, in CCSSeqSemaphore]
hidden_fn_seq2 [lemma, in CCSSeqSemaphore]
hidden_fn_seq1 [lemma, in CCSSeqSemaphore]
hidden_fn [definition, in CCSSeqSemaphore]
hmlA_hmlE [lemma, in CharacteristicLogics]
hmlA_csim [lemma, in CharacteristicLogics]
hmlE_csim [lemma, in CharacteristicLogics]
hml_csim [lemma, in CharacteristicLogics]
hml_pcsim [lemma, in CharacteristicLogics]
hml_implE_neg [lemma, in CharacteristicLogics]
hml_implA_neg [lemma, in CharacteristicLogics]
hml_equiv [definition, in CharacteristicLogics]
hml_equivE [definition, in CharacteristicLogics]
hml_equivA [definition, in CharacteristicLogics]
hml_implE [definition, in CharacteristicLogics]
hml_implA [definition, in CharacteristicLogics]
_ ⊨ᴬ _ (forces_scope) [notation, in CharacteristicLogics]
_ ⊨ᴱ _ (forces_scope) [notation, in CharacteristicLogics]
⦋ _ ⦌ _ (scopeA) [notation, in CharacteristicLogics]
〈 _ 〉 _ (scopeE) [notation, in CharacteristicLogics]
_ ∨ _ (scopeE) [notation, in CharacteristicLogics]
_ ∧ _ (scopeA) [notation, in CharacteristicLogics]
¬ _ (scopeA) [notation, in CharacteristicLogics]
¬ _ (scopeE) [notation, in CharacteristicLogics]
HML_DecoupledBisimulation.lts [variable, in CharacteristicLogics]
HML_DecoupledBisimulation [section, in CharacteristicLogics]
I
Id [constructor, in SfLib]id [inductive, in SfLib]
iff_intro_swap [lemma, in LibTactics]
image_finite [definition, in CharacteristicLogics]
image_finite_R [definition, in CharacteristicLogics]
inj_pair2 [axiom, in LibTactics]
interleaving [definition, in Labels]
interleaving_app [lemma, in Labels]
interleaving_com [lemma, in Labels]
interleaving_l_nil [lemma, in Labels]
interleaving_r_nil [lemma, in Labels]
interleaving_nil [lemma, in CCSSeqSemaphore]
inv [definition, in BisimTheory]
inv_inv [lemma, in BisimTheory]
in_split_l' [lemma, in Util]
In_combine_swap [lemma, in CCSSeqSemaphore]
in_res_list_filter [lemma, in CCSSeqSemaphore]
in_res_filter [lemma, in CCSSeqSemaphore]
is_halted [projection, in LabeledTransitionSystems]
L
label [inductive, in Labels]LabeledTransitionSystems [library]
labeled_transition_system [record, in LabeledTransitionSystems]
Labels [library]
label_eq [lemma, in Labels]
label_tau_deq [lemma, in Labels]
label_eq_dec [lemma, in Labels]
LibTactics [library]
LibTacticsCompatibility [module, in LibTactics]
ListLE [section, in Util]
ListPairFun [section, in Util]
ListPlus [section, in Util]
ListRep [section, in Util]
Lists [section, in Util]
list_disjE [definition, in CharacteristicLogics]
list_conjA [definition, in CharacteristicLogics]
list_le_zeros [lemma, in Util]
list_zeros_length [lemma, in Util]
list_rep_length [lemma, in Util]
list_plus_zeros1 [lemma, in Util]
list_plus_zeros2 [lemma, in Util]
list_zeros [definition, in Util]
list_rep [definition, in Util]
list_le_cons1 [lemma, in Util]
list_le_cons2 [lemma, in Util]
list_le_refl [lemma, in Util]
list_plus_le [lemma, in Util]
list_le_plus [lemma, in Util]
list_le_single [lemma, in Util]
list_le_app2 [lemma, in Util]
list_le_app1 [lemma, in Util]
list_le_trans [lemma, in Util]
list_le [definition, in Util]
list_plus_nil_r [lemma, in Util]
list_plus_length [lemma, in Util]
list_plus_cons [lemma, in Util]
list_plus_app [lemma, in Util]
list_plus_assoc [lemma, in Util]
list_plus_comm [lemma, in Util]
list_plus [definition, in Util]
list_pair_fun_nil_l [lemma, in Util]
list_pair_fun_nil_r [lemma, in Util]
list_pair_fun_length [lemma, in Util]
list_pair_fun_app [lemma, in Util]
list_pair_fun_cons [lemma, in Util]
list_pair_fun_assoc [lemma, in Util]
list_pair_fun_comm [lemma, in Util]
list_pair_fun [definition, in Util]
list_rep_length [lemma, in CCSSeqSemaphore]
list_rep_mid [lemma, in CCSSeqSemaphore]
list_rep_snoc [lemma, in CCSSeqSemaphore]
list_rep [definition, in CCSSeqSemaphore]
lstep [projection, in LabeledTransitionSystems]
lstep_pcsim [lemma, in BisimTheory]
lstep_ebisim2 [lemma, in BisimTheory]
lstep_ebisim1 [lemma, in BisimTheory]
lstep_esim2 [lemma, in BisimTheory]
lstep_esim1 [lemma, in BisimTheory]
lstep_pbisim2 [lemma, in BisimTheory]
lstep_pbisim1 [lemma, in BisimTheory]
lstep_pcssim [lemma, in BisimTheory]
lstep_wbisim2 [lemma, in BisimTheory]
lstep_wbisim1 [lemma, in BisimTheory]
lstep_sbisim2 [lemma, in BisimTheory]
lstep_sbisim1 [lemma, in BisimTheory]
lstep_rep_esim1_par_list [lemma, in CCSSeqSemaphore]
lstep_rep_wbisim1_par_list [lemma, in CCSSeqSemaphore]
ltac_something_show [lemma, in LibTactics]
ltac_something_hide [lemma, in LibTactics]
ltac_something_eq [lemma, in LibTactics]
ltac_something [definition, in LibTactics]
ltac_to_generalize [definition, in LibTactics]
ltac_tag_subst [definition, in LibTactics]
ltac_nat_from_int [definition, in LibTactics]
ltac_database_provide [lemma, in LibTactics]
ltac_database [definition, in LibTactics]
ltac_mark [constructor, in LibTactics]
ltac_Mark [inductive, in LibTactics]
ltac_wilds [constructor, in LibTactics]
ltac_Wilds [inductive, in LibTactics]
ltac_wild [constructor, in LibTactics]
ltac_Wild [inductive, in LibTactics]
ltac_no_arg [constructor, in LibTactics]
ltac_No_arg [inductive, in LibTactics]
LTS [module, in CCSSeqSemaphore]
lts_L [projection, in LabeledTransitionSystems]
lts_S [projection, in LabeledTransitionSystems]
LTS.is_halted [definition, in CCSSeqSemaphore]
LTS.lstep [inductive, in CCSSeqSemaphore]
LTS.lstep_out [constructor, in CCSSeqSemaphore]
LTS.lstep_in [constructor, in CCSSeqSemaphore]
LTS.lts [definition, in CCSSeqSemaphore]
l_out [constructor, in Labels]
l_in [constructor, in Labels]
l_tau [constructor, in Labels]
M
Machine [section, in CCSSeqSemaphore]min_le [lemma, in Util]
MiscLemmas [section, in CCSSeqSemaphore]
Morphisms [module, in CCSSeqSemaphore]
Morphisms.CBisimCsSetoid [instance, in CCSSeqSemaphore]
Morphisms.eq_ssum [lemma, in CCSSeqSemaphore]
Morphisms.eq_ssumR [lemma, in CCSSeqSemaphore]
Morphisms.eq_ssumL [lemma, in CCSSeqSemaphore]
Morphisms.p_ssum [definition, in CCSSeqSemaphore]
Morphisms.p_ssumR [definition, in CCSSeqSemaphore]
Morphisms.p_ssumL [definition, in CCSSeqSemaphore]
Morphisms.WBisimCsSetoid [instance, in CCSSeqSemaphore]
N
name [definition, in NameSet]nameset [definition, in NameSet]
NameSet [module, in NameSet]
NameSet [library]
NameSetFacts [module, in NameSet]
NameSetProps [module, in NameSet]
NameSet_diff_add [lemma, in NameSet]
NameSet_Subset_inter [lemma, in NameSet]
NameSet_union_remove [lemma, in NameSet]
name_eq [definition, in NameSet]
negA [definition, in CharacteristicLogics]
negA_correct1 [lemma, in CharacteristicLogics]
negE [definition, in CharacteristicLogics]
negE_correct1 [lemma, in CharacteristicLogics]
next_nat [inductive, in SfLib]
nl [definition, in Labels]
nn [constructor, in SfLib]
noninterference_step_star_res_list1 [lemma, in CCSSeqSemaphore]
Notation [module, in NameSet]
Notation [module, in Labels]
Notation [module, in CCSSeqSemaphore]
Notation.U [module, in CCSSeqSemaphore]
_ ? (label_scope) [notation, in Labels]
_ ! (label_scope) [notation, in Labels]
τ (label_scope) [notation, in Labels]
_ ⊆ _ (nameset_scope) [notation, in NameSet]
_ ⋂ _ (nameset_scope) [notation, in NameSet]
_ ⋃ _ (nameset_scope) [notation, in NameSet]
_ ∈ _ (nameset_scope) [notation, in NameSet]
∅ (nameset_scope) [notation, in NameSet]
_ / _ (nameset_scope) [notation, in NameSet]
not_iff [lemma, in CharacteristicLogics]
not_or [lemma, in CharacteristicLogics]
not_and [lemma, in CharacteristicLogics]
not_impl [lemma, in CharacteristicLogics]
not_forall [lemma, in CharacteristicLogics]
not_exists [lemma, in CharacteristicLogics]
not_not [lemma, in CharacteristicLogics]
not_eq_beq_id_false [lemma, in SfLib]
not_eq_beq_false [lemma, in SfLib]
O
one_way_termination_sensitive_id [lemma, in BisimTheory]one_way_termination_sensitive_halted [lemma, in BisimTheory]
one_way_termination_sensitive [definition, in BisimTheory]
P
Parallelization [section, in CCSSeqSemaphore]partial_contrasimilar [definition, in BisimTheory]
partial_coupled_similar [definition, in BisimTheory]
partial_map [definition, in SfLib]
partial_function [definition, in SfLib]
par_eventual_simulation [lemma, in BisimTheory]
par_simulation_lstep [lemma, in BisimTheory]
par_simulation_tstep [lemma, in BisimTheory]
par_simulation_step_star [lemma, in BisimTheory]
par_bisimilar [definition, in BisimTheory]
par_bisimulation [definition, in BisimTheory]
par_simulation [definition, in BisimTheory]
par_seq_inversion [lemma, in CCSSeqSemaphore]
par_nterm [lemma, in CCSSeqSemaphore]
par_list_rep_nterm [lemma, in CCSSeqSemaphore]
par_list_app [lemma, in CCSSeqSemaphore]
par_list_not_halted1 [lemma, in CCSSeqSemaphore]
par_list [definition, in CCSSeqSemaphore]
par_swap_swap [lemma, in CCSSeqSemaphore]
par_swap [definition, in CCSSeqSemaphore]
pbisim_csim [lemma, in BisimTheory]
pbisim_ebisim [lemma, in BisimTheory]
pbisim_esim [lemma, in BisimTheory]
pbisim_par_simulation [lemma, in BisimTheory]
pbisim_weak_simulation [lemma, in BisimTheory]
pbisim_one_way_termination_sensitive2 [lemma, in BisimTheory]
pbisim_one_way_termination_sensitive1 [lemma, in BisimTheory]
pbisim_refl [lemma, in BisimTheory]
pbisim_seq_par [lemma, in CCSSeqSemaphore]
pcsim_hmlE [lemma, in CharacteristicLogics]
pcsim_hmlA [lemma, in CharacteristicLogics]
pcsim_symm_wbisim [lemma, in BisimTheory]
pcsim_tstep [lemma, in BisimTheory]
pcsim_forward [lemma, in BisimTheory]
pcsim_backward [lemma, in BisimTheory]
pcsim_refl_step_star [lemma, in BisimTheory]
pcsim_trans [lemma, in BisimTheory]
pcsim_csim [lemma, in BisimTheory]
pcsim_one_way_termination_sensitive [lemma, in BisimTheory]
pcsim_contrasimulation [lemma, in BisimTheory]
pcsim_refl [lemma, in BisimTheory]
pcsim_rep [lemma, in CCSSeqSemaphore]
pcsim_list [definition, in CCSSeqSemaphore]
pcsim_res [lemma, in CCSSeqSemaphore]
pcsim_out [lemma, in CCSSeqSemaphore]
pcsim_in [lemma, in CCSSeqSemaphore]
pcsim_tau [lemma, in CCSSeqSemaphore]
pcsim_act [lemma, in CCSSeqSemaphore]
pcsim_parR [lemma, in CCSSeqSemaphore]
pcsim_parL [lemma, in CCSSeqSemaphore]
pcssim_pcsim [lemma, in BisimTheory]
pcssim_cssim [lemma, in BisimTheory]
pcssim_weak_simulation [lemma, in BisimTheory]
pcssim_coupled_simulation_flipping [lemma, in BisimTheory]
pcssim_one_way_termination_sensitive [lemma, in BisimTheory]
phi [inductive, in CharacteristicLogics]
phiA [inductive, in CharacteristicLogics]
phiE [inductive, in CharacteristicLogics]
phi1 [constructor, in CharacteristicLogics]
phi2 [constructor, in CharacteristicLogics]
PMapFacts [module, in NameSet]
Pos_OWL.eq_leibniz [definition, in NameSet]
Pos_OWL [module, in NameSet]
proc [inductive, in CCSSeqSemaphore]
proc_eq_dec [lemma, in CCSSeqSemaphore]
p_res_list_eq [lemma, in CCSSeqSemaphore]
p_res_list_inv' [lemma, in CCSSeqSemaphore]
p_res_list_inv [lemma, in CCSSeqSemaphore]
p_res_list_app [lemma, in CCSSeqSemaphore]
p_res_list_nil [lemma, in CCSSeqSemaphore]
p_res_list [definition, in CCSSeqSemaphore]
p_rep [constructor, in CCSSeqSemaphore]
p_res [constructor, in CCSSeqSemaphore]
p_act [constructor, in CCSSeqSemaphore]
p_seq [constructor, in CCSSeqSemaphore]
p_par [constructor, in CCSSeqSemaphore]
p_sum [constructor, in CCSSeqSemaphore]
p_nil [constructor, in CCSSeqSemaphore]
R
refl_step_closure [inductive, in SfLib]relation [definition, in SfLib]
rep_step_result_list_rep [lemma, in CCSSeqSemaphore]
rep_step_result_get [lemma, in CCSSeqSemaphore]
rep_step_result1 [constructor, in CCSSeqSemaphore]
rep_step_result0 [constructor, in CCSSeqSemaphore]
rep_step_result [inductive, in CCSSeqSemaphore]
ResCountLabels [section, in CCSSeqSemaphore]
ResList [section, in CCSSeqSemaphore]
ResListCountLabels [section, in CCSSeqSemaphore]
ResListCountLabelsStepping [section, in CCSSeqSemaphore]
ResListFilter [section, in CCSSeqSemaphore]
ResListFN [section, in CCSSeqSemaphore]
res_list_filter_nil_out_In [lemma, in CCSSeqSemaphore]
res_list_filter_nil_in_In [lemma, in CCSSeqSemaphore]
res_list_count_labels_fun [lemma, in CCSSeqSemaphore]
res_list_count_labels_nIn'' [lemma, in CCSSeqSemaphore]
res_list_count_labels_cons [lemma, in CCSSeqSemaphore]
res_list_count_labels_com [lemma, in CCSSeqSemaphore]
res_list_count_labels_interleaving1 [lemma, in CCSSeqSemaphore]
res_list_count_labels_exists_min [lemma, in CCSSeqSemaphore]
res_list_count_labels_nIn' [lemma, in CCSSeqSemaphore]
res_list_count_labels_list_le_com [lemma, in CCSSeqSemaphore]
res_list_count_labels_nIn1 [lemma, in CCSSeqSemaphore]
res_list_count_labels_list_le [lemma, in CCSSeqSemaphore]
res_list_count_labels_incr [lemma, in CCSSeqSemaphore]
res_list_count_labels_single' [lemma, in CCSSeqSemaphore]
res_list_count_labels_nIn [lemma, in CCSSeqSemaphore]
res_list_count_labels_nil2' [lemma, in CCSSeqSemaphore]
res_list_count_labels_single [lemma, in CCSSeqSemaphore]
res_list_count_labels_nil2 [lemma, in CCSSeqSemaphore]
res_list_count_labels_app2' [lemma, in CCSSeqSemaphore]
res_list_count_labels_app2 [lemma, in CCSSeqSemaphore]
res_list_count_labels_app [lemma, in CCSSeqSemaphore]
res_list_count_labels_length [lemma, in CCSSeqSemaphore]
res_list_count_labels_min [definition, in CCSSeqSemaphore]
res_list_count_labels [definition, in CCSSeqSemaphore]
res_count_labels_com [lemma, in CCSSeqSemaphore]
res_count_labels_interleaving1 [lemma, in CCSSeqSemaphore]
res_count_labels_positive_app_com2 [lemma, in CCSSeqSemaphore]
res_count_labels_exists_min [lemma, in CCSSeqSemaphore]
res_count_labels_fun [lemma, in CCSSeqSemaphore]
res_count_labels_nIn''' [lemma, in CCSSeqSemaphore]
res_count_labels_le_com [lemma, in CCSSeqSemaphore]
res_count_labels_nIn'' [lemma, in CCSSeqSemaphore]
res_count_labels_incr [lemma, in CCSSeqSemaphore]
res_count_labels_nIn' [lemma, in CCSSeqSemaphore]
res_count_labels_nIn [lemma, in CCSSeqSemaphore]
res_count_labels_cons_com [lemma, in CCSSeqSemaphore]
res_count_labels_nil2' [lemma, in CCSSeqSemaphore]
res_count_labels_nil2 [lemma, in CCSSeqSemaphore]
res_count_labels_app2' [lemma, in CCSSeqSemaphore]
res_count_labels_app2 [lemma, in CCSSeqSemaphore]
res_list_filter_interleaving [lemma, in CCSSeqSemaphore]
res_list_filter_count_occ [lemma, in CCSSeqSemaphore]
res_list_filter_single_inv [lemma, in CCSSeqSemaphore]
res_list_filter_interleaving_fn2 [lemma, in CCSSeqSemaphore]
res_list_filter_In_filter [lemma, in CCSSeqSemaphore]
res_list_filter_tau [lemma, in CCSSeqSemaphore]
res_list_filter_rev [lemma, in CCSSeqSemaphore]
res_list_filter_app [lemma, in CCSSeqSemaphore]
res_list_filter_perm [lemma, in CCSSeqSemaphore]
res_filter_comm [lemma, in CCSSeqSemaphore]
res_filter_cons2' [lemma, in CCSSeqSemaphore]
res_list_filter_cons2' [lemma, in CCSSeqSemaphore]
res_list_filter_app2 [lemma, in CCSSeqSemaphore]
res_list_filter_cons2 [lemma, in CCSSeqSemaphore]
res_filter_cons2 [lemma, in CCSSeqSemaphore]
res_list_filter_nIn [lemma, in CCSSeqSemaphore]
res_filter_nIn [lemma, in CCSSeqSemaphore]
res_filter_In_filter [lemma, in CCSSeqSemaphore]
res_filter_app2 [lemma, in CCSSeqSemaphore]
res_list_filter_nil2 [lemma, in CCSSeqSemaphore]
res_list_filter [definition, in CCSSeqSemaphore]
res_count_labels [definition, in CCSSeqSemaphore]
res_filter [definition, in CCSSeqSemaphore]
rm [definition, in LibTactics]
rsc_trans [lemma, in SfLib]
rsc_R [lemma, in SfLib]
rsc_step [constructor, in SfLib]
rsc_refl [constructor, in SfLib]
S
sbisimilar [definition, in BisimTheory]sbisim_wbisim [lemma, in BisimTheory]
sbisim_trans [lemma, in BisimTheory]
sbisim_strong_simulation [lemma, in BisimTheory]
sbisim_strong_one_way_termination_sensitive [lemma, in BisimTheory]
sbisim_refl [lemma, in BisimTheory]
sbisim_symm [lemma, in BisimTheory]
sbisim_rep_step_result [lemma, in CCSSeqSemaphore]
sbisim_list_rep_par_list' [lemma, in CCSSeqSemaphore]
sbisim_list_rep_par_list [lemma, in CCSSeqSemaphore]
sbisim_par_list_rep [lemma, in CCSSeqSemaphore]
sbisim_nterm_par_assoc [lemma, in CCSSeqSemaphore]
sbisim_par_list [lemma, in CCSSeqSemaphore]
sbisim_par [lemma, in CCSSeqSemaphore]
sbisim_parR [lemma, in CCSSeqSemaphore]
sbisim_parL [lemma, in CCSSeqSemaphore]
sbisim_par_rep [lemma, in CCSSeqSemaphore]
sbisim_sum_comm [lemma, in CCSSeqSemaphore]
sbisim_par_swap [lemma, in CCSSeqSemaphore]
sbisim_seq_assoc [lemma, in CCSSeqSemaphore]
SeqParBackwardSimulationFailsContrasimulationHolds [module, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.csim_true [lemma, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.cssim_false [lemma, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.esim_true [lemma, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.Lemmas [section, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.lstep [inductive, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.lts [definition, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.p0 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.p1 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.p2 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.p3 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.p4 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.p5 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.p6 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q0 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q1 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q2 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q3 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q4 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q5 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q6 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q7 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.RR [inductive, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.RR_66 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.RR_55 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.RR_44 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.RR_33 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.RR_22 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.RR_11 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.RR_00 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.state [inductive, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q46 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q24 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q07 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q35 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q13 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_p46 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_p24 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_p35 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_p13 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q74 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q73 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q02 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q01 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_p02 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_p01 [constructor, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.tstep [inductive, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.wbisim_false [lemma, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.wsim_backward_false [lemma, in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.wsim_forward_true [lemma, in Examples]
seq_par_inversion [lemma, in CCSSeqSemaphore]
Sets [section, in NameSet]
SfLib [library]
skipn_length [lemma, in Util]
skip_axiom [variable, in LibTactics]
snd_split_app [lemma, in Util]
snd_split [lemma, in Util]
SplitCombine [section, in Util]
split_combine' [lemma, in Util]
stable_bisimulation [definition, in BisimTheory]
step [inductive, in CCSSeqSemaphore]
StepNotation [module, in CCSSeqSemaphore]
StepNotation.U [module, in CCSSeqSemaphore]
_ ⟶ _ ⟶ _ [notation, in CCSSeqSemaphore]
_ ⟶ _ ― _ → _ [notation, in CCSSeqSemaphore]
_ ― _ → _ ⟶ _ [notation, in CCSSeqSemaphore]
_ ― _ → _ ― _ → _ [notation, in CCSSeqSemaphore]
_ ⟶ _ [notation, in CCSSeqSemaphore]
_ ― _ → _ [notation, in CCSSeqSemaphore]
_ - _ -> _ [notation, in CCSSeqSemaphore]
_ ---> _ [notation, in CCSSeqSemaphore]
Stepping [module, in LabeledTransitionSystems]
Stepping [section, in CCSSeqSemaphore]
Stepping.lstep_star_step_star [lemma, in LabeledTransitionSystems]
Stepping.lstep_star_halted_correct2 [lemma, in LabeledTransitionSystems]
Stepping.lstep_star_halted_resolve [lemma, in LabeledTransitionSystems]
Stepping.lstep_lcons [constructor, in LabeledTransitionSystems]
Stepping.lstep_nil [constructor, in LabeledTransitionSystems]
Stepping.lstep_star [inductive, in LabeledTransitionSystems]
Stepping.single_lstep [lemma, in LabeledTransitionSystems]
Stepping.single_tstep [lemma, in LabeledTransitionSystems]
Stepping.stable [definition, in LabeledTransitionSystems]
Stepping.Stepping [section, in LabeledTransitionSystems]
Stepping.Stepping.lts [variable, in LabeledTransitionSystems]
Stepping.step_star_app [lemma, in LabeledTransitionSystems]
Stepping.step_lsnoc [lemma, in LabeledTransitionSystems]
Stepping.step_tsnoc [lemma, in LabeledTransitionSystems]
Stepping.step_tcons [constructor, in LabeledTransitionSystems]
Stepping.step_lcons [constructor, in LabeledTransitionSystems]
Stepping.step_nil [constructor, in LabeledTransitionSystems]
Stepping.step_star [inductive, in LabeledTransitionSystems]
Stepping.tstep_star_halted_resolve [lemma, in LabeledTransitionSystems]
step_star_det_internal_choice [lemma, in BisimTheory]
step_star_pcsim [lemma, in BisimTheory]
step_star_ebisim2 [lemma, in BisimTheory]
step_star_ebisim1 [lemma, in BisimTheory]
step_star_esim2 [lemma, in BisimTheory]
step_star_esim1 [lemma, in BisimTheory]
step_star_pbisim2 [lemma, in BisimTheory]
step_star_pbisim1 [lemma, in BisimTheory]
step_star_pcssim [lemma, in BisimTheory]
step_star_wbisim2 [lemma, in BisimTheory]
step_star_wbisim1 [lemma, in BisimTheory]
step_star_sbisim2 [lemma, in BisimTheory]
step_star_sbisim1 [lemma, in BisimTheory]
step_star_par_seq_converges2 [lemma, in CCSSeqSemaphore]
step_star_par_seq_converges1 [lemma, in CCSSeqSemaphore]
step_star_par_seq_converges [lemma, in CCSSeqSemaphore]
step_star_rep_pcsim_par_list [lemma, in CCSSeqSemaphore]
step_star_par_list_pcsim [lemma, in CCSSeqSemaphore]
step_star_rep_esim2_par_list [lemma, in CCSSeqSemaphore]
step_star_par_list_esim2 [lemma, in CCSSeqSemaphore]
step_par_rep_resolve [lemma, in CCSSeqSemaphore]
step_star_par_unzip'' [lemma, in CCSSeqSemaphore]
step_star_rep_par_list [lemma, in CCSSeqSemaphore]
step_star_par_list_unzip [lemma, in CCSSeqSemaphore]
step_star_par_list2 [lemma, in CCSSeqSemaphore]
step_star_par_list1 [lemma, in CCSSeqSemaphore]
step_par_list2 [lemma, in CCSSeqSemaphore]
step_par_list1 [lemma, in CCSSeqSemaphore]
step_par_list1_cons [lemma, in CCSSeqSemaphore]
step_par_list1_app_r [lemma, in CCSSeqSemaphore]
step_par_list1_app_l [lemma, in CCSSeqSemaphore]
step_rep_inv' [lemma, in CCSSeqSemaphore]
step_par_list_inv [lemma, in CCSSeqSemaphore]
step_ind' [definition, in CCSSeqSemaphore]
step_step__ [lemma, in CCSSeqSemaphore]
step_rep_result [lemma, in CCSSeqSemaphore]
step__ [inductive, in CCSSeqSemaphore]
step_rep_inv [lemma, in CCSSeqSemaphore]
step_res_list [lemma, in CCSSeqSemaphore]
step_star_res_list_parR_step [lemma, in CCSSeqSemaphore]
step_star_res_list_parL_step [lemma, in CCSSeqSemaphore]
step_star_res_list_par_swap_nil' [lemma, in CCSSeqSemaphore]
step_star_res_list_par_swap' [lemma, in CCSSeqSemaphore]
step_star_res_list_par_swap [lemma, in CCSSeqSemaphore]
step_star_res_list_seq_app [lemma, in CCSSeqSemaphore]
step_star_res_list_par_swap_nil [lemma, in CCSSeqSemaphore]
step_star_res_list' [lemma, in CCSSeqSemaphore]
step_star_res_list [lemma, in CCSSeqSemaphore]
step_star_res_list_inv'' [lemma, in CCSSeqSemaphore]
step_res_list_inv'' [lemma, in CCSSeqSemaphore]
step_star_res_list_inv' [lemma, in CCSSeqSemaphore]
step_res_list_inv [lemma, in CCSSeqSemaphore]
step_res_list_label_wf [definition, in CCSSeqSemaphore]
step_res_list_par_seq_app [lemma, in CCSSeqSemaphore]
step_star_res_list_nIn [lemma, in CCSSeqSemaphore]
step_star_res_list_nil [lemma, in CCSSeqSemaphore]
step_star_hidden [lemma, in CCSSeqSemaphore]
step_star_seq_inv [lemma, in CCSSeqSemaphore]
step_star_par_swap_nil' [lemma, in CCSSeqSemaphore]
step_star_par_swap_nil [lemma, in CCSSeqSemaphore]
step_star_par_seq_inv [lemma, in CCSSeqSemaphore]
step_star_parR_seq_app [lemma, in CCSSeqSemaphore]
step_star_parL_seq_app [lemma, in CCSSeqSemaphore]
step_star_par_zip' [lemma, in CCSSeqSemaphore]
step_star_par_unzip' [lemma, in CCSSeqSemaphore]
step_star_parR_seq_inv [lemma, in CCSSeqSemaphore]
step_star_par_swap [lemma, in CCSSeqSemaphore]
step_star_par_swap' [lemma, in CCSSeqSemaphore]
step_star_parL_seq_inv [lemma, in CCSSeqSemaphore]
step_star_l_tau_nIn [lemma, in CCSSeqSemaphore]
step_star_res_count_out [lemma, in CCSSeqSemaphore]
step_star_res_count_in [lemma, in CCSSeqSemaphore]
step_star_res_inv [lemma, in CCSSeqSemaphore]
step_star_res [lemma, in CCSSeqSemaphore]
step_star_res_nIn [lemma, in CCSSeqSemaphore]
step_star_par_unzip [lemma, in CCSSeqSemaphore]
step_star_nil_resolve [lemma, in CCSSeqSemaphore]
step_star_lstep_inv [lemma, in CCSSeqSemaphore]
step_star_seq_app [lemma, in CCSSeqSemaphore]
step_star_parR_step [lemma, in CCSSeqSemaphore]
step_star_parL_step [lemma, in CCSSeqSemaphore]
strong_csim_wbisim [lemma, in BisimTheory]
strong_pcsim_symm [lemma, in BisimTheory]
strong_weak_simulation [lemma, in BisimTheory]
strong_weak_one_way_termination_sensitive [lemma, in BisimTheory]
strong_simulation_id [lemma, in BisimTheory]
strong_one_way_termination_sensitive_id [lemma, in BisimTheory]
strong_bisimulation_symm [lemma, in BisimTheory]
strong_simulation_step_star [lemma, in BisimTheory]
strong_simulation_lstep [lemma, in BisimTheory]
strong_simulation_tstep [lemma, in BisimTheory]
strong_one_way_termination_sensitive_halted [lemma, in BisimTheory]
strong_bisimulation [definition, in BisimTheory]
strong_simulation [definition, in BisimTheory]
strong_one_way_termination_sensitive [definition, in BisimTheory]
SyntaxNotation [module, in CCSSeqSemaphore]
SyntaxNotation.TestNotation [module, in CCSSeqSemaphore]
SyntaxNotation.U [module, in CCSSeqSemaphore]
Ø (proc_scope) [notation, in CCSSeqSemaphore]
υ _ : _ (proc_scope) [notation, in CCSSeqSemaphore]
υ _ : _ : _ (proc_scope) [notation, in CCSSeqSemaphore]
τ. _ (proc_scope) [notation, in CCSSeqSemaphore]
_ ?. _ (proc_scope) [notation, in CCSSeqSemaphore]
_ ̄ !. _ (proc_scope) [notation, in CCSSeqSemaphore]
_ ‖ _ (proc_scope) [notation, in CCSSeqSemaphore]
_ !! (proc_scope) [notation, in CCSSeqSemaphore]
O (proc_scope) [notation, in CCSSeqSemaphore]
(). _ (proc_scope) [notation, in CCSSeqSemaphore]
_ #: _ (proc_scope) [notation, in CCSSeqSemaphore]
_ # _ : _ (proc_scope) [notation, in CCSSeqSemaphore]
_ !. _ (proc_scope) [notation, in CCSSeqSemaphore]
_ ?. _ (proc_scope) [notation, in CCSSeqSemaphore]
_ ;; _ (proc_scope) [notation, in CCSSeqSemaphore]
_ || _ (proc_scope) [notation, in CCSSeqSemaphore]
_ + _ (proc_scope) [notation, in CCSSeqSemaphore]
s_res_nil__ [constructor, in CCSSeqSemaphore]
s_seq_nil__ [constructor, in CCSSeqSemaphore]
s_sum_nil__ [constructor, in CCSSeqSemaphore]
s_par_nil__ [constructor, in CCSSeqSemaphore]
s_rep__ [constructor, in CCSSeqSemaphore]
s_res_count_out__ [constructor, in CCSSeqSemaphore]
s_res_count_in__ [constructor, in CCSSeqSemaphore]
s_res__ [constructor, in CCSSeqSemaphore]
s_seq__ [constructor, in CCSSeqSemaphore]
s_sumR__ [constructor, in CCSSeqSemaphore]
s_sumL__ [constructor, in CCSSeqSemaphore]
s_parR__ [constructor, in CCSSeqSemaphore]
s_parL__ [constructor, in CCSSeqSemaphore]
s_act__ [constructor, in CCSSeqSemaphore]
s_res_list [lemma, in CCSSeqSemaphore]
s_res_nil [constructor, in CCSSeqSemaphore]
s_seq_nil [constructor, in CCSSeqSemaphore]
s_sum_nil [constructor, in CCSSeqSemaphore]
s_par_nil [constructor, in CCSSeqSemaphore]
s_rep [constructor, in CCSSeqSemaphore]
s_res_count_out [constructor, in CCSSeqSemaphore]
s_res_count_in [constructor, in CCSSeqSemaphore]
s_res [constructor, in CCSSeqSemaphore]
s_seq [constructor, in CCSSeqSemaphore]
s_sumR [constructor, in CCSSeqSemaphore]
s_sumL [constructor, in CCSSeqSemaphore]
s_parR [constructor, in CCSSeqSemaphore]
s_parL [constructor, in CCSSeqSemaphore]
s_act [constructor, in CCSSeqSemaphore]
T
term_impl_nil [lemma, in CCSSeqSemaphore]term_impl_step_star2 [lemma, in CCSSeqSemaphore]
term_impl_step_star1 [lemma, in CCSSeqSemaphore]
term_impl [definition, in CCSSeqSemaphore]
TestParallelization [module, in CCSSeqSemaphore]
TestParallelization.csim_M_N [lemma, in CCSSeqSemaphore]
TestParallelization.esim_M_N [lemma, in CCSSeqSemaphore]
TestParallelization.l0 [definition, in CCSSeqSemaphore]
TestParallelization.l1 [definition, in CCSSeqSemaphore]
TestParallelization.l2 [definition, in CCSSeqSemaphore]
TestParallelization.M [variable, in CCSSeqSemaphore]
TestParallelization.N [variable, in CCSSeqSemaphore]
TestParallelization.wbisim_converges [lemma, in CCSSeqSemaphore]
top [constructor, in CharacteristicLogics]
topE [definition, in CharacteristicLogics]
topE_correct [lemma, in CharacteristicLogics]
tot [constructor, in SfLib]
total_relation [inductive, in SfLib]
TraceEquivalence [section, in BisimTheory]
TraceEquivalence.lts [variable, in BisimTheory]
trace_equivalent [definition, in BisimTheory]
tstep [projection, in LabeledTransitionSystems]
tstep_contrasimulation [definition, in BisimTheory]
tstep_pcsim [lemma, in BisimTheory]
tstep_ebisim2 [lemma, in BisimTheory]
tstep_ebisim1 [lemma, in BisimTheory]
tstep_esim2 [lemma, in BisimTheory]
tstep_esim1 [lemma, in BisimTheory]
tstep_pbisim2 [lemma, in BisimTheory]
tstep_pbisim1 [lemma, in BisimTheory]
tstep_pcssim [lemma, in BisimTheory]
tstep_weak_bisimulation [definition, in BisimTheory]
tstep_wbisim2 [lemma, in BisimTheory]
tstep_wbisim1 [lemma, in BisimTheory]
tstep_sbisim2 [lemma, in BisimTheory]
tstep_sbisim1 [lemma, in BisimTheory]
tstep_rep_esim1_par_list [lemma, in CCSSeqSemaphore]
tstep_rep_wbisim1_par_list [lemma, in CCSSeqSemaphore]
U
Util [library]W
wbisimilar [definition, in BisimTheory]wbisim_pcsim [lemma, in BisimTheory]
wbisim_csim [lemma, in BisimTheory]
wbisim_ebisim [lemma, in BisimTheory]
wbisim_esim [lemma, in BisimTheory]
wbisim_pbisim [lemma, in BisimTheory]
wbisim_coupled_sim [lemma, in BisimTheory]
wbisim_tstep_det [lemma, in BisimTheory]
wbisim_step [lemma, in BisimTheory]
wbisim_tstep [lemma, in BisimTheory]
wbisim_trans [lemma, in BisimTheory]
wbisim_weak_simulation [lemma, in BisimTheory]
wbisim_one_way_termination_sensitive [lemma, in BisimTheory]
wbisim_refl [lemma, in BisimTheory]
wbisim_symm [lemma, in BisimTheory]
wbisim_res_list_out [lemma, in CCSSeqSemaphore]
wbisim_res_list_in [lemma, in CCSSeqSemaphore]
wbisim_res_list_act_comm [lemma, in CCSSeqSemaphore]
wbisim_res_list_tau_sum [lemma, in CCSSeqSemaphore]
wbisim_rep [lemma, in CCSSeqSemaphore]
wbisim_list_symm [lemma, in CCSSeqSemaphore]
wbisim_list_same_split [lemma, in CCSSeqSemaphore]
wbisim_list_single [lemma, in CCSSeqSemaphore]
wbisim_list_nil [lemma, in CCSSeqSemaphore]
wbisim_list_app [lemma, in CCSSeqSemaphore]
wbisim_list_cons [lemma, in CCSSeqSemaphore]
wbisim_list [definition, in CCSSeqSemaphore]
wbisim_act [lemma, in CCSSeqSemaphore]
wbisim_internal_sum [lemma, in CCSSeqSemaphore]
wbisim_stable_sum [lemma, in CCSSeqSemaphore]
wbisim_res_list [lemma, in CCSSeqSemaphore]
wbisim_res [lemma, in CCSSeqSemaphore]
wbisim_par [lemma, in CCSSeqSemaphore]
wbisim_parR [lemma, in CCSSeqSemaphore]
wbisim_parL [lemma, in CCSSeqSemaphore]
wbisim_seq [lemma, in CCSSeqSemaphore]
wbisim_seq2 [lemma, in CCSSeqSemaphore]
wbisim_seq1 [lemma, in CCSSeqSemaphore]
wbisim_sum_dup [lemma, in CCSSeqSemaphore]
wbisim_res_out [lemma, in CCSSeqSemaphore]
wbisim_res_in [lemma, in CCSSeqSemaphore]
wbisim_res_tau_sum [lemma, in CCSSeqSemaphore]
wbisim_sum_nilR [lemma, in CCSSeqSemaphore]
wbisim_sum_nilL [lemma, in CCSSeqSemaphore]
wbisim_par_rep [lemma, in CCSSeqSemaphore]
wbisim_res_out_comm [lemma, in CCSSeqSemaphore]
wbisim_res_in_comm [lemma, in CCSSeqSemaphore]
wbisim_res_act_comm [lemma, in CCSSeqSemaphore]
wbisim_res_comm [lemma, in CCSSeqSemaphore]
wbisim_res_nil [lemma, in CCSSeqSemaphore]
wbisim_intro_tau [lemma, in CCSSeqSemaphore]
wbisim_sum_comm [lemma, in CCSSeqSemaphore]
wbisim_par_assoc [lemma, in CCSSeqSemaphore]
wbisim_par_nil2 [lemma, in CCSSeqSemaphore]
wbisim_par_nil1 [lemma, in CCSSeqSemaphore]
wbisim_par_swap [lemma, in CCSSeqSemaphore]
wbisim_seq_assoc [lemma, in CCSSeqSemaphore]
wbisim_seq_nil [lemma, in CCSSeqSemaphore]
wbisim_nil_seq [lemma, in CCSSeqSemaphore]
weakly_image_finite [definition, in CharacteristicLogics]
weak_eventual_simulation [lemma, in BisimTheory]
weak_par_simulation [lemma, in BisimTheory]
weak_simulation_id [lemma, in BisimTheory]
weak_bisimulation_symm [lemma, in BisimTheory]
weak_simulation_step_star [lemma, in BisimTheory]
weak_simulation_lstep [lemma, in BisimTheory]
weak_simulation_tstep [lemma, in BisimTheory]
weak_bisimulation [definition, in BisimTheory]
weak_simulation [definition, in BisimTheory]
other
>> _ _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]>> _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ (ltac_scope) [notation, in LibTactics]
>> _ (ltac_scope) [notation, in LibTactics]
>> (ltac_scope) [notation, in LibTactics]
___ (ltac_scope) [notation, in LibTactics]
__ (ltac_scope) [notation, in LibTactics]
exists _ _ _ _ _ _ _ _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ _ _ _ _ _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ _ _ _ _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ _ _ _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ _ _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ _ , _ (type_scope) [notation, in LibTactics]
exists _ _ , _ (type_scope) [notation, in LibTactics]
exists _ , _ (type_scope) [notation, in LibTactics]
_ =' _ [notation, in LibTactics]
_ ++ _ [notation, in SfLib]
nosimpl _ [notation, in LibTactics]
Register _ _ [notation, in LibTactics]
Something [notation, in LibTactics]
[ _ , .. , _ ] [notation, in SfLib]
[ ] [notation, in SfLib]
Instance Index
M
Morphisms.CBisimCsSetoid [in CCSSeqSemaphore]Morphisms.WBisimCsSetoid [in CCSSeqSemaphore]
Projection Index
H
halted_correct2 [in LabeledTransitionSystems]halted_correct1 [in LabeledTransitionSystems]
I
is_halted [in LabeledTransitionSystems]L
lstep [in LabeledTransitionSystems]lts_L [in LabeledTransitionSystems]
lts_S [in LabeledTransitionSystems]
T
tstep [in LabeledTransitionSystems]Record Index
L
labeled_transition_system [in LabeledTransitionSystems]Lemma Index
A
andb_true [in SfLib]andb_true_elim2 [in SfLib]
andb_true_elim1 [in SfLib]
app_inv [in Util]
app_split3 [in Util]
B
beq_id_sym [in SfLib]beq_id_false_not_eq [in SfLib]
beq_id_eq [in SfLib]
beq_id_refl [in SfLib]
beq_nat_sym [in SfLib]
ble_nat_false [in SfLib]
ble_nat_true [in SfLib]
botA_correct [in CharacteristicLogics]
C
combine_app [in Util]combine_nil2 [in Util]
contrasimulation_symm_weak_bisimulation [in BisimTheory]
contrasimulation_id [in BisimTheory]
contrasimulation_flip [in BisimTheory]
contrasimulation_lstep [in BisimTheory]
contrasimulation_tstep [in BisimTheory]
contrasimulation_step_star [in BisimTheory]
converges_term_impl [in CCSSeqSemaphore]
converges_step_star [in CCSSeqSemaphore]
converges_nil [in CCSSeqSemaphore]
converges_converges'_equiv [in CCSSeqSemaphore]
count_occ_nIn [in Util]
coupled_simulation_flipping_id [in BisimTheory]
coupled_similar_equiv [in BisimTheory]
csim_hml [in CharacteristicLogics]
csim_hmlE [in CharacteristicLogics]
csim_hmlA [in CharacteristicLogics]
csim_trace_equivalent [in BisimTheory]
csim_stable_bisim [in BisimTheory]
csim_symm [in BisimTheory]
csim_trans [in BisimTheory]
csim_pcsim2 [in BisimTheory]
csim_pcsim1 [in BisimTheory]
csim_refl [in BisimTheory]
csim_seq_par_simpl [in CCSSeqSemaphore]
csim_seq_par [in CCSSeqSemaphore]
csim_rep [in CCSSeqSemaphore]
csim_res_list [in CCSSeqSemaphore]
csim_internal_sum [in CCSSeqSemaphore]
csim_stable_sum [in CCSSeqSemaphore]
csim_res [in CCSSeqSemaphore]
csim_out [in CCSSeqSemaphore]
csim_in [in CCSSeqSemaphore]
csim_act [in CCSSeqSemaphore]
csim_par [in CCSSeqSemaphore]
csim_parR [in CCSSeqSemaphore]
csim_parL [in CCSSeqSemaphore]
csim_seq [in CCSSeqSemaphore]
csim_seq2 [in CCSSeqSemaphore]
csim_seq1 [in CCSSeqSemaphore]
csim_intro_tau [in CCSSeqSemaphore]
csim_sum_comm [in CCSSeqSemaphore]
csim_par_assoc [in CCSSeqSemaphore]
csim_seq_assoc [in CCSSeqSemaphore]
csim_par_nil2 [in CCSSeqSemaphore]
csim_par_nil1 [in CCSSeqSemaphore]
csim_par_swap [in CCSSeqSemaphore]
cssim_csim [in BisimTheory]
cssim_coupled_simulation_flipping [in BisimTheory]
cssim_pcssim2 [in BisimTheory]
cssim_pcssim1 [in BisimTheory]
cssim_refl [in BisimTheory]
cssim_symm [in BisimTheory]
D
det_internal_choice_csim_wbisim [in BisimTheory]det_internal_choice_pcsim_wbisim [in BisimTheory]
det_internal_choice_pcsim_symm [in BisimTheory]
dup_lemma [in LibTactics]
E
ebisim_trans_false.ebisim_trans_false [in Examples]ebisim_trans_false.ebisimPR_false [in Examples]
ebisim_trans_false.step_star_s2_out [in Examples]
ebisim_trans_false.esimRQ [in Examples]
ebisim_trans_false.esimPQ [in Examples]
ebisim_trans_false.nat_div2 [in Examples]
ebisim_trans_false.step_star_s2_inv [in Examples]
ebisim_trans_false.step_star_s2_tau [in Examples]
ebisim_trans_false.step_star_s1_inv [in Examples]
ebisim_trans_false.step_star_s1_tau [in Examples]
ebisim_trans_false.step_star_s0_inv [in Examples]
ebisim_csim [in BisimTheory]
ebisim_symm [in BisimTheory]
ebisim_eventual_simulation2 [in BisimTheory]
ebisim_eventual_simulation1 [in BisimTheory]
ebisim_one_way_termination_sensitive2 [in BisimTheory]
ebisim_one_way_termination_sensitive1 [in BisimTheory]
ebisim_refl [in BisimTheory]
equates_6 [in LibTactics]
equates_5 [in LibTactics]
equates_4 [in LibTactics]
equates_3 [in LibTactics]
equates_2 [in LibTactics]
equates_1 [in LibTactics]
equates_0 [in LibTactics]
esim_trans [in BisimTheory]
esim_par_simulation [in BisimTheory]
esim_weak_simulation [in BisimTheory]
esim_one_way_termination_sensitive [in BisimTheory]
esim_ebisim2 [in BisimTheory]
esim_ebisim1 [in BisimTheory]
esim_refl [in BisimTheory]
esim_seq_par_simpl [in CCSSeqSemaphore]
esim_seq_par [in CCSSeqSemaphore]
esim_rep [in CCSSeqSemaphore]
esim_act [in CCSSeqSemaphore]
esim_internal_sum [in CCSSeqSemaphore]
esim_stable_sum [in CCSSeqSemaphore]
esim_res_list [in CCSSeqSemaphore]
esim_res [in CCSSeqSemaphore]
esim_par [in CCSSeqSemaphore]
esim_parR [in CCSSeqSemaphore]
esim_parL [in CCSSeqSemaphore]
esim_seq [in CCSSeqSemaphore]
esim_seq2 [in CCSSeqSemaphore]
esim_seq1 [in CCSSeqSemaphore]
esim_list_same_split [in CCSSeqSemaphore]
esim_list_single [in CCSSeqSemaphore]
esim_list_nil [in CCSSeqSemaphore]
esim_list_app [in CCSSeqSemaphore]
esim_list_cons [in CCSSeqSemaphore]
eventual_simulation_lstep [in BisimTheory]
eventual_simulation_tstep [in BisimTheory]
eventual_simulation_step_star [in BisimTheory]
ev_not_ev_S [in SfLib]
ExampleA.csim_false [in Examples]
ExampleA.cssim_false [in Examples]
ExampleA.pbisim_false2 [in Examples]
ExampleA.pbisim_false1 [in Examples]
ExampleA.wbisim_false [in Examples]
ExampleB_Full.csim_true [in Examples]
ExampleB_Full.pbisim_false1 [in Examples]
ExampleB_Full.pbisim_true2 [in Examples]
ExampleB_Full.cssim_false [in Examples]
ExampleB_Full.wbisim_false [in Examples]
ExampleB'.csim_true [in Examples]
ExampleB'.cssim_false [in Examples]
ExampleB'.pbisim_false2 [in Examples]
ExampleB'.pbisim_true1 [in Examples]
ExampleB'.wbisim_false [in Examples]
ExampleB.csim_true [in Examples]
ExampleB.csim_false [in Examples]
ExampleB.pbisim_false2 [in Examples]
ExampleB.pbisim_true1 [in Examples]
ExampleB.wbisim_false [in Examples]
ExampleC.csim_false [in Examples]
ExampleC.cssim_false [in Examples]
ExampleC.pbisim_false1 [in Examples]
ExampleC.wbisim_false2 [in Examples]
ExampleC.wbisim_false [in Examples]
ExampleD.csim_false [in Examples]
ExampleD.cssim_false [in Examples]
ExampleD.par_bisim_false2 [in Examples]
ExampleD.pbisim_false1 [in Examples]
ExampleD.wbisim_false [in Examples]
ExampleE.csim_false [in Examples]
ExampleE.cssim_false [in Examples]
ExampleE.pbisim_false2 [in Examples]
ExampleE.pbisim_false1 [in Examples]
ExampleE.wbisim_false [in Examples]
ExampleF.csim_true [in Examples]
ExampleF.cssim_true [in Examples]
ExampleF.pbisim_false2 [in Examples]
ExampleF.pbisim_false1 [in Examples]
ExampleF.wbisim_false [in Examples]
ExampleG.csim_true [in Examples]
ExampleG.cssim_true [in Examples]
ExampleG.pbisim_true2 [in Examples]
ExampleG.pbisim_false1 [in Examples]
ExampleG.wbisim_false [in Examples]
Examples.lstep_inv [in CCSSeqSemaphore]
Examples.step_star_par_tsum2 [in CCSSeqSemaphore]
Examples.SumPar.coupled_sim_false [in CCSSeqSemaphore]
Examples.SumPar.csim_true_O [in CCSSeqSemaphore]
Examples.SumPar.csim_true [in CCSSeqSemaphore]
Examples.SumPar.esim_true_O [in CCSSeqSemaphore]
Examples.SumPar.esim_true [in CCSSeqSemaphore]
Examples.SumPar.step_star_app' [in CCSSeqSemaphore]
Examples.SumPar.wbisim_false [in CCSSeqSemaphore]
Examples.SumPar.wsim_backwards_false [in CCSSeqSemaphore]
Examples.SumSum.coupled_sim_false [in CCSSeqSemaphore]
Examples.SumSum.csim_true [in CCSSeqSemaphore]
Examples.SumSum.esim_true [in CCSSeqSemaphore]
Examples.SumSum.wbisim_false [in CCSSeqSemaphore]
Examples.SumSum.wsim_backwards_false [in CCSSeqSemaphore]
exists_list_unsatE [in CharacteristicLogics]
exists_list_unsatA [in CharacteristicLogics]
extend_shadow [in SfLib]
extend_neq [in SfLib]
extend_eq [in SfLib]
ex_falso_quodlibet [in SfLib]
F
flip_pcsim [in BisimTheory]flip_pcssim [in BisimTheory]
fn_in_subset_step_star_res_list_parR [in CCSSeqSemaphore]
fn_in_subset_step_star_res_list_parL [in CCSSeqSemaphore]
fn_subset_step_star_res_list_parR_In [in CCSSeqSemaphore]
fn_subset_step_star_res_list_parL_In [in CCSSeqSemaphore]
fn_subset_step_star_p_res_list_In [in CCSSeqSemaphore]
fn_p_res_list [in CCSSeqSemaphore]
fn_In_res_list1 [in CCSSeqSemaphore]
fn_in_subset_step_star_parR [in CCSSeqSemaphore]
fn_in_subset_step_star_parL [in CCSSeqSemaphore]
fn_subset_step_star_parR_In [in CCSSeqSemaphore]
fn_subset_step_star_parL_In [in CCSSeqSemaphore]
fn_step_star_In [in CCSSeqSemaphore]
fn_out_step_star_In [in CCSSeqSemaphore]
fn_in_step_star_In [in CCSSeqSemaphore]
fn_out_step_In [in CCSSeqSemaphore]
fn_in_step_In [in CCSSeqSemaphore]
fn_subset_step_star [in CCSSeqSemaphore]
fn_out_subset_step_star [in CCSSeqSemaphore]
fn_in_subset_step_star [in CCSSeqSemaphore]
fn_subset_step [in CCSSeqSemaphore]
fn_out_subset_step [in CCSSeqSemaphore]
fn_in_subset_step [in CCSSeqSemaphore]
fn_in_out_equiv [in CCSSeqSemaphore]
Forall2_list_rep [in CCSSeqSemaphore]
Forall2_symm [in CCSSeqSemaphore]
fst_split_app [in Util]
fst_split [in Util]
f_list_disjE [in CharacteristicLogics]
f_list_conjA [in CharacteristicLogics]
H
halted_converge_pcsim [in BisimTheory]halted_pcsim2 [in BisimTheory]
halted_pcsim1 [in BisimTheory]
halted_converge_ebisim2 [in BisimTheory]
halted_converge_ebisim1 [in BisimTheory]
halted_ebisim2 [in BisimTheory]
halted_ebisim1 [in BisimTheory]
halted_converge_esim2 [in BisimTheory]
halted_converge_esim1 [in BisimTheory]
halted_esim2 [in BisimTheory]
halted_esim1 [in BisimTheory]
halted_converge_pbisim2 [in BisimTheory]
halted_converge_pbisim1 [in BisimTheory]
halted_pbisim2 [in BisimTheory]
halted_pbisim1 [in BisimTheory]
halted_converge_pcssim1 [in BisimTheory]
halted_pcssim2 [in BisimTheory]
halted_pcssim1 [in BisimTheory]
halted_converge_wbisim2 [in BisimTheory]
halted_converge_wbisim1 [in BisimTheory]
halted_wbisim2 [in BisimTheory]
halted_wbisim1 [in BisimTheory]
halted_converge_sbisim2 [in BisimTheory]
halted_converge_sbisim1 [in BisimTheory]
halted_sbisim2 [in BisimTheory]
halted_sbisim1 [in BisimTheory]
hidden_fn_step_star_res_list_parL [in CCSSeqSemaphore]
hidden_fn_step_star_res_list_parR [in CCSSeqSemaphore]
hidden_fn_seq3 [in CCSSeqSemaphore]
hidden_fn_step_star_parL [in CCSSeqSemaphore]
hidden_fn_step_star_parR [in CCSSeqSemaphore]
hidden_fn_step_star [in CCSSeqSemaphore]
hidden_fn_seq2 [in CCSSeqSemaphore]
hidden_fn_seq1 [in CCSSeqSemaphore]
hmlA_hmlE [in CharacteristicLogics]
hmlA_csim [in CharacteristicLogics]
hmlE_csim [in CharacteristicLogics]
hml_csim [in CharacteristicLogics]
hml_pcsim [in CharacteristicLogics]
hml_implE_neg [in CharacteristicLogics]
hml_implA_neg [in CharacteristicLogics]
I
iff_intro_swap [in LibTactics]interleaving_app [in Labels]
interleaving_com [in Labels]
interleaving_l_nil [in Labels]
interleaving_r_nil [in Labels]
interleaving_nil [in CCSSeqSemaphore]
inv_inv [in BisimTheory]
in_split_l' [in Util]
In_combine_swap [in CCSSeqSemaphore]
in_res_list_filter [in CCSSeqSemaphore]
in_res_filter [in CCSSeqSemaphore]
L
label_eq [in Labels]label_tau_deq [in Labels]
label_eq_dec [in Labels]
list_le_zeros [in Util]
list_zeros_length [in Util]
list_rep_length [in Util]
list_plus_zeros1 [in Util]
list_plus_zeros2 [in Util]
list_le_cons1 [in Util]
list_le_cons2 [in Util]
list_le_refl [in Util]
list_plus_le [in Util]
list_le_plus [in Util]
list_le_single [in Util]
list_le_app2 [in Util]
list_le_app1 [in Util]
list_le_trans [in Util]
list_plus_nil_r [in Util]
list_plus_length [in Util]
list_plus_cons [in Util]
list_plus_app [in Util]
list_plus_assoc [in Util]
list_plus_comm [in Util]
list_pair_fun_nil_l [in Util]
list_pair_fun_nil_r [in Util]
list_pair_fun_length [in Util]
list_pair_fun_app [in Util]
list_pair_fun_cons [in Util]
list_pair_fun_assoc [in Util]
list_pair_fun_comm [in Util]
list_rep_length [in CCSSeqSemaphore]
list_rep_mid [in CCSSeqSemaphore]
list_rep_snoc [in CCSSeqSemaphore]
lstep_pcsim [in BisimTheory]
lstep_ebisim2 [in BisimTheory]
lstep_ebisim1 [in BisimTheory]
lstep_esim2 [in BisimTheory]
lstep_esim1 [in BisimTheory]
lstep_pbisim2 [in BisimTheory]
lstep_pbisim1 [in BisimTheory]
lstep_pcssim [in BisimTheory]
lstep_wbisim2 [in BisimTheory]
lstep_wbisim1 [in BisimTheory]
lstep_sbisim2 [in BisimTheory]
lstep_sbisim1 [in BisimTheory]
lstep_rep_esim1_par_list [in CCSSeqSemaphore]
lstep_rep_wbisim1_par_list [in CCSSeqSemaphore]
ltac_something_show [in LibTactics]
ltac_something_hide [in LibTactics]
ltac_something_eq [in LibTactics]
ltac_database_provide [in LibTactics]
M
min_le [in Util]Morphisms.eq_ssum [in CCSSeqSemaphore]
Morphisms.eq_ssumR [in CCSSeqSemaphore]
Morphisms.eq_ssumL [in CCSSeqSemaphore]
N
NameSet_diff_add [in NameSet]NameSet_Subset_inter [in NameSet]
NameSet_union_remove [in NameSet]
negA_correct1 [in CharacteristicLogics]
negE_correct1 [in CharacteristicLogics]
noninterference_step_star_res_list1 [in CCSSeqSemaphore]
not_iff [in CharacteristicLogics]
not_or [in CharacteristicLogics]
not_and [in CharacteristicLogics]
not_impl [in CharacteristicLogics]
not_forall [in CharacteristicLogics]
not_exists [in CharacteristicLogics]
not_not [in CharacteristicLogics]
not_eq_beq_id_false [in SfLib]
not_eq_beq_false [in SfLib]
O
one_way_termination_sensitive_id [in BisimTheory]one_way_termination_sensitive_halted [in BisimTheory]
P
par_eventual_simulation [in BisimTheory]par_simulation_lstep [in BisimTheory]
par_simulation_tstep [in BisimTheory]
par_simulation_step_star [in BisimTheory]
par_seq_inversion [in CCSSeqSemaphore]
par_nterm [in CCSSeqSemaphore]
par_list_rep_nterm [in CCSSeqSemaphore]
par_list_app [in CCSSeqSemaphore]
par_list_not_halted1 [in CCSSeqSemaphore]
par_swap_swap [in CCSSeqSemaphore]
pbisim_csim [in BisimTheory]
pbisim_ebisim [in BisimTheory]
pbisim_esim [in BisimTheory]
pbisim_par_simulation [in BisimTheory]
pbisim_weak_simulation [in BisimTheory]
pbisim_one_way_termination_sensitive2 [in BisimTheory]
pbisim_one_way_termination_sensitive1 [in BisimTheory]
pbisim_refl [in BisimTheory]
pbisim_seq_par [in CCSSeqSemaphore]
pcsim_hmlE [in CharacteristicLogics]
pcsim_hmlA [in CharacteristicLogics]
pcsim_symm_wbisim [in BisimTheory]
pcsim_tstep [in BisimTheory]
pcsim_forward [in BisimTheory]
pcsim_backward [in BisimTheory]
pcsim_refl_step_star [in BisimTheory]
pcsim_trans [in BisimTheory]
pcsim_csim [in BisimTheory]
pcsim_one_way_termination_sensitive [in BisimTheory]
pcsim_contrasimulation [in BisimTheory]
pcsim_refl [in BisimTheory]
pcsim_rep [in CCSSeqSemaphore]
pcsim_res [in CCSSeqSemaphore]
pcsim_out [in CCSSeqSemaphore]
pcsim_in [in CCSSeqSemaphore]
pcsim_tau [in CCSSeqSemaphore]
pcsim_act [in CCSSeqSemaphore]
pcsim_parR [in CCSSeqSemaphore]
pcsim_parL [in CCSSeqSemaphore]
pcssim_pcsim [in BisimTheory]
pcssim_cssim [in BisimTheory]
pcssim_weak_simulation [in BisimTheory]
pcssim_coupled_simulation_flipping [in BisimTheory]
pcssim_one_way_termination_sensitive [in BisimTheory]
proc_eq_dec [in CCSSeqSemaphore]
p_res_list_eq [in CCSSeqSemaphore]
p_res_list_inv' [in CCSSeqSemaphore]
p_res_list_inv [in CCSSeqSemaphore]
p_res_list_app [in CCSSeqSemaphore]
p_res_list_nil [in CCSSeqSemaphore]
R
rep_step_result_list_rep [in CCSSeqSemaphore]rep_step_result_get [in CCSSeqSemaphore]
res_list_filter_nil_out_In [in CCSSeqSemaphore]
res_list_filter_nil_in_In [in CCSSeqSemaphore]
res_list_count_labels_fun [in CCSSeqSemaphore]
res_list_count_labels_nIn'' [in CCSSeqSemaphore]
res_list_count_labels_cons [in CCSSeqSemaphore]
res_list_count_labels_com [in CCSSeqSemaphore]
res_list_count_labels_interleaving1 [in CCSSeqSemaphore]
res_list_count_labels_exists_min [in CCSSeqSemaphore]
res_list_count_labels_nIn' [in CCSSeqSemaphore]
res_list_count_labels_list_le_com [in CCSSeqSemaphore]
res_list_count_labels_nIn1 [in CCSSeqSemaphore]
res_list_count_labels_list_le [in CCSSeqSemaphore]
res_list_count_labels_incr [in CCSSeqSemaphore]
res_list_count_labels_single' [in CCSSeqSemaphore]
res_list_count_labels_nIn [in CCSSeqSemaphore]
res_list_count_labels_nil2' [in CCSSeqSemaphore]
res_list_count_labels_single [in CCSSeqSemaphore]
res_list_count_labels_nil2 [in CCSSeqSemaphore]
res_list_count_labels_app2' [in CCSSeqSemaphore]
res_list_count_labels_app2 [in CCSSeqSemaphore]
res_list_count_labels_app [in CCSSeqSemaphore]
res_list_count_labels_length [in CCSSeqSemaphore]
res_count_labels_com [in CCSSeqSemaphore]
res_count_labels_interleaving1 [in CCSSeqSemaphore]
res_count_labels_positive_app_com2 [in CCSSeqSemaphore]
res_count_labels_exists_min [in CCSSeqSemaphore]
res_count_labels_fun [in CCSSeqSemaphore]
res_count_labels_nIn''' [in CCSSeqSemaphore]
res_count_labels_le_com [in CCSSeqSemaphore]
res_count_labels_nIn'' [in CCSSeqSemaphore]
res_count_labels_incr [in CCSSeqSemaphore]
res_count_labels_nIn' [in CCSSeqSemaphore]
res_count_labels_nIn [in CCSSeqSemaphore]
res_count_labels_cons_com [in CCSSeqSemaphore]
res_count_labels_nil2' [in CCSSeqSemaphore]
res_count_labels_nil2 [in CCSSeqSemaphore]
res_count_labels_app2' [in CCSSeqSemaphore]
res_count_labels_app2 [in CCSSeqSemaphore]
res_list_filter_interleaving [in CCSSeqSemaphore]
res_list_filter_count_occ [in CCSSeqSemaphore]
res_list_filter_single_inv [in CCSSeqSemaphore]
res_list_filter_interleaving_fn2 [in CCSSeqSemaphore]
res_list_filter_In_filter [in CCSSeqSemaphore]
res_list_filter_tau [in CCSSeqSemaphore]
res_list_filter_rev [in CCSSeqSemaphore]
res_list_filter_app [in CCSSeqSemaphore]
res_list_filter_perm [in CCSSeqSemaphore]
res_filter_comm [in CCSSeqSemaphore]
res_filter_cons2' [in CCSSeqSemaphore]
res_list_filter_cons2' [in CCSSeqSemaphore]
res_list_filter_app2 [in CCSSeqSemaphore]
res_list_filter_cons2 [in CCSSeqSemaphore]
res_filter_cons2 [in CCSSeqSemaphore]
res_list_filter_nIn [in CCSSeqSemaphore]
res_filter_nIn [in CCSSeqSemaphore]
res_filter_In_filter [in CCSSeqSemaphore]
res_filter_app2 [in CCSSeqSemaphore]
res_list_filter_nil2 [in CCSSeqSemaphore]
rsc_trans [in SfLib]
rsc_R [in SfLib]
S
sbisim_wbisim [in BisimTheory]sbisim_trans [in BisimTheory]
sbisim_strong_simulation [in BisimTheory]
sbisim_strong_one_way_termination_sensitive [in BisimTheory]
sbisim_refl [in BisimTheory]
sbisim_symm [in BisimTheory]
sbisim_rep_step_result [in CCSSeqSemaphore]
sbisim_list_rep_par_list' [in CCSSeqSemaphore]
sbisim_list_rep_par_list [in CCSSeqSemaphore]
sbisim_par_list_rep [in CCSSeqSemaphore]
sbisim_nterm_par_assoc [in CCSSeqSemaphore]
sbisim_par_list [in CCSSeqSemaphore]
sbisim_par [in CCSSeqSemaphore]
sbisim_parR [in CCSSeqSemaphore]
sbisim_parL [in CCSSeqSemaphore]
sbisim_par_rep [in CCSSeqSemaphore]
sbisim_sum_comm [in CCSSeqSemaphore]
sbisim_par_swap [in CCSSeqSemaphore]
sbisim_seq_assoc [in CCSSeqSemaphore]
SeqParBackwardSimulationFailsContrasimulationHolds.csim_true [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.cssim_false [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.esim_true [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.wbisim_false [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.wsim_backward_false [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.wsim_forward_true [in Examples]
seq_par_inversion [in CCSSeqSemaphore]
skipn_length [in Util]
snd_split_app [in Util]
snd_split [in Util]
split_combine' [in Util]
Stepping.lstep_star_step_star [in LabeledTransitionSystems]
Stepping.lstep_star_halted_correct2 [in LabeledTransitionSystems]
Stepping.lstep_star_halted_resolve [in LabeledTransitionSystems]
Stepping.single_lstep [in LabeledTransitionSystems]
Stepping.single_tstep [in LabeledTransitionSystems]
Stepping.step_star_app [in LabeledTransitionSystems]
Stepping.step_lsnoc [in LabeledTransitionSystems]
Stepping.step_tsnoc [in LabeledTransitionSystems]
Stepping.tstep_star_halted_resolve [in LabeledTransitionSystems]
step_star_det_internal_choice [in BisimTheory]
step_star_pcsim [in BisimTheory]
step_star_ebisim2 [in BisimTheory]
step_star_ebisim1 [in BisimTheory]
step_star_esim2 [in BisimTheory]
step_star_esim1 [in BisimTheory]
step_star_pbisim2 [in BisimTheory]
step_star_pbisim1 [in BisimTheory]
step_star_pcssim [in BisimTheory]
step_star_wbisim2 [in BisimTheory]
step_star_wbisim1 [in BisimTheory]
step_star_sbisim2 [in BisimTheory]
step_star_sbisim1 [in BisimTheory]
step_star_par_seq_converges2 [in CCSSeqSemaphore]
step_star_par_seq_converges1 [in CCSSeqSemaphore]
step_star_par_seq_converges [in CCSSeqSemaphore]
step_star_rep_pcsim_par_list [in CCSSeqSemaphore]
step_star_par_list_pcsim [in CCSSeqSemaphore]
step_star_rep_esim2_par_list [in CCSSeqSemaphore]
step_star_par_list_esim2 [in CCSSeqSemaphore]
step_par_rep_resolve [in CCSSeqSemaphore]
step_star_par_unzip'' [in CCSSeqSemaphore]
step_star_rep_par_list [in CCSSeqSemaphore]
step_star_par_list_unzip [in CCSSeqSemaphore]
step_star_par_list2 [in CCSSeqSemaphore]
step_star_par_list1 [in CCSSeqSemaphore]
step_par_list2 [in CCSSeqSemaphore]
step_par_list1 [in CCSSeqSemaphore]
step_par_list1_cons [in CCSSeqSemaphore]
step_par_list1_app_r [in CCSSeqSemaphore]
step_par_list1_app_l [in CCSSeqSemaphore]
step_rep_inv' [in CCSSeqSemaphore]
step_par_list_inv [in CCSSeqSemaphore]
step_step__ [in CCSSeqSemaphore]
step_rep_result [in CCSSeqSemaphore]
step_rep_inv [in CCSSeqSemaphore]
step_res_list [in CCSSeqSemaphore]
step_star_res_list_parR_step [in CCSSeqSemaphore]
step_star_res_list_parL_step [in CCSSeqSemaphore]
step_star_res_list_par_swap_nil' [in CCSSeqSemaphore]
step_star_res_list_par_swap' [in CCSSeqSemaphore]
step_star_res_list_par_swap [in CCSSeqSemaphore]
step_star_res_list_seq_app [in CCSSeqSemaphore]
step_star_res_list_par_swap_nil [in CCSSeqSemaphore]
step_star_res_list' [in CCSSeqSemaphore]
step_star_res_list [in CCSSeqSemaphore]
step_star_res_list_inv'' [in CCSSeqSemaphore]
step_res_list_inv'' [in CCSSeqSemaphore]
step_star_res_list_inv' [in CCSSeqSemaphore]
step_res_list_inv [in CCSSeqSemaphore]
step_res_list_par_seq_app [in CCSSeqSemaphore]
step_star_res_list_nIn [in CCSSeqSemaphore]
step_star_res_list_nil [in CCSSeqSemaphore]
step_star_hidden [in CCSSeqSemaphore]
step_star_seq_inv [in CCSSeqSemaphore]
step_star_par_swap_nil' [in CCSSeqSemaphore]
step_star_par_swap_nil [in CCSSeqSemaphore]
step_star_par_seq_inv [in CCSSeqSemaphore]
step_star_parR_seq_app [in CCSSeqSemaphore]
step_star_parL_seq_app [in CCSSeqSemaphore]
step_star_par_zip' [in CCSSeqSemaphore]
step_star_par_unzip' [in CCSSeqSemaphore]
step_star_parR_seq_inv [in CCSSeqSemaphore]
step_star_par_swap [in CCSSeqSemaphore]
step_star_par_swap' [in CCSSeqSemaphore]
step_star_parL_seq_inv [in CCSSeqSemaphore]
step_star_l_tau_nIn [in CCSSeqSemaphore]
step_star_res_count_out [in CCSSeqSemaphore]
step_star_res_count_in [in CCSSeqSemaphore]
step_star_res_inv [in CCSSeqSemaphore]
step_star_res [in CCSSeqSemaphore]
step_star_res_nIn [in CCSSeqSemaphore]
step_star_par_unzip [in CCSSeqSemaphore]
step_star_nil_resolve [in CCSSeqSemaphore]
step_star_lstep_inv [in CCSSeqSemaphore]
step_star_seq_app [in CCSSeqSemaphore]
step_star_parR_step [in CCSSeqSemaphore]
step_star_parL_step [in CCSSeqSemaphore]
strong_csim_wbisim [in BisimTheory]
strong_pcsim_symm [in BisimTheory]
strong_weak_simulation [in BisimTheory]
strong_weak_one_way_termination_sensitive [in BisimTheory]
strong_simulation_id [in BisimTheory]
strong_one_way_termination_sensitive_id [in BisimTheory]
strong_bisimulation_symm [in BisimTheory]
strong_simulation_step_star [in BisimTheory]
strong_simulation_lstep [in BisimTheory]
strong_simulation_tstep [in BisimTheory]
strong_one_way_termination_sensitive_halted [in BisimTheory]
s_res_list [in CCSSeqSemaphore]
T
term_impl_nil [in CCSSeqSemaphore]term_impl_step_star2 [in CCSSeqSemaphore]
term_impl_step_star1 [in CCSSeqSemaphore]
TestParallelization.csim_M_N [in CCSSeqSemaphore]
TestParallelization.esim_M_N [in CCSSeqSemaphore]
TestParallelization.wbisim_converges [in CCSSeqSemaphore]
topE_correct [in CharacteristicLogics]
tstep_pcsim [in BisimTheory]
tstep_ebisim2 [in BisimTheory]
tstep_ebisim1 [in BisimTheory]
tstep_esim2 [in BisimTheory]
tstep_esim1 [in BisimTheory]
tstep_pbisim2 [in BisimTheory]
tstep_pbisim1 [in BisimTheory]
tstep_pcssim [in BisimTheory]
tstep_wbisim2 [in BisimTheory]
tstep_wbisim1 [in BisimTheory]
tstep_sbisim2 [in BisimTheory]
tstep_sbisim1 [in BisimTheory]
tstep_rep_esim1_par_list [in CCSSeqSemaphore]
tstep_rep_wbisim1_par_list [in CCSSeqSemaphore]
W
wbisim_pcsim [in BisimTheory]wbisim_csim [in BisimTheory]
wbisim_ebisim [in BisimTheory]
wbisim_esim [in BisimTheory]
wbisim_pbisim [in BisimTheory]
wbisim_coupled_sim [in BisimTheory]
wbisim_tstep_det [in BisimTheory]
wbisim_step [in BisimTheory]
wbisim_tstep [in BisimTheory]
wbisim_trans [in BisimTheory]
wbisim_weak_simulation [in BisimTheory]
wbisim_one_way_termination_sensitive [in BisimTheory]
wbisim_refl [in BisimTheory]
wbisim_symm [in BisimTheory]
wbisim_res_list_out [in CCSSeqSemaphore]
wbisim_res_list_in [in CCSSeqSemaphore]
wbisim_res_list_act_comm [in CCSSeqSemaphore]
wbisim_res_list_tau_sum [in CCSSeqSemaphore]
wbisim_rep [in CCSSeqSemaphore]
wbisim_list_symm [in CCSSeqSemaphore]
wbisim_list_same_split [in CCSSeqSemaphore]
wbisim_list_single [in CCSSeqSemaphore]
wbisim_list_nil [in CCSSeqSemaphore]
wbisim_list_app [in CCSSeqSemaphore]
wbisim_list_cons [in CCSSeqSemaphore]
wbisim_act [in CCSSeqSemaphore]
wbisim_internal_sum [in CCSSeqSemaphore]
wbisim_stable_sum [in CCSSeqSemaphore]
wbisim_res_list [in CCSSeqSemaphore]
wbisim_res [in CCSSeqSemaphore]
wbisim_par [in CCSSeqSemaphore]
wbisim_parR [in CCSSeqSemaphore]
wbisim_parL [in CCSSeqSemaphore]
wbisim_seq [in CCSSeqSemaphore]
wbisim_seq2 [in CCSSeqSemaphore]
wbisim_seq1 [in CCSSeqSemaphore]
wbisim_sum_dup [in CCSSeqSemaphore]
wbisim_res_out [in CCSSeqSemaphore]
wbisim_res_in [in CCSSeqSemaphore]
wbisim_res_tau_sum [in CCSSeqSemaphore]
wbisim_sum_nilR [in CCSSeqSemaphore]
wbisim_sum_nilL [in CCSSeqSemaphore]
wbisim_par_rep [in CCSSeqSemaphore]
wbisim_res_out_comm [in CCSSeqSemaphore]
wbisim_res_in_comm [in CCSSeqSemaphore]
wbisim_res_act_comm [in CCSSeqSemaphore]
wbisim_res_comm [in CCSSeqSemaphore]
wbisim_res_nil [in CCSSeqSemaphore]
wbisim_intro_tau [in CCSSeqSemaphore]
wbisim_sum_comm [in CCSSeqSemaphore]
wbisim_par_assoc [in CCSSeqSemaphore]
wbisim_par_nil2 [in CCSSeqSemaphore]
wbisim_par_nil1 [in CCSSeqSemaphore]
wbisim_par_swap [in CCSSeqSemaphore]
wbisim_seq_assoc [in CCSSeqSemaphore]
wbisim_seq_nil [in CCSSeqSemaphore]
wbisim_nil_seq [in CCSSeqSemaphore]
weak_eventual_simulation [in BisimTheory]
weak_par_simulation [in BisimTheory]
weak_simulation_id [in BisimTheory]
weak_bisimulation_symm [in BisimTheory]
weak_simulation_step_star [in BisimTheory]
weak_simulation_lstep [in BisimTheory]
weak_simulation_tstep [in BisimTheory]
Section Index
A
Algebraic [in CCSSeqSemaphore]B
Bisimulation [in BisimTheory]C
Congruence [in CCSSeqSemaphore]ContrasimulationAlgebraic [in CCSSeqSemaphore]
ContrasimulationCongruence [in CCSSeqSemaphore]
E
ebisim_trans_false.Lemmas [in Examples]equatesLemma [in LibTactics]
EventualSimulationCompositionality [in CCSSeqSemaphore]
ExampleA.Lemmas [in Examples]
ExampleB_Full.Lemmas [in Examples]
ExampleB'.Lemmas [in Examples]
ExampleB.Lemmas [in Examples]
ExampleC.Lemmas [in Examples]
ExampleD.Lemmas [in Examples]
ExampleE.Lemmas [in Examples]
ExampleF.Lemmas [in Examples]
ExampleG.Lemmas [in Examples]
F
FreeNameLemmas [in CCSSeqSemaphore]FreeNames [in CCSSeqSemaphore]
H
HiddenProc [in CCSSeqSemaphore]HML_DecoupledBisimulation [in CharacteristicLogics]
L
ListLE [in Util]ListPairFun [in Util]
ListPlus [in Util]
ListRep [in Util]
Lists [in Util]
M
Machine [in CCSSeqSemaphore]MiscLemmas [in CCSSeqSemaphore]
P
Parallelization [in CCSSeqSemaphore]R
ResCountLabels [in CCSSeqSemaphore]ResList [in CCSSeqSemaphore]
ResListCountLabels [in CCSSeqSemaphore]
ResListCountLabelsStepping [in CCSSeqSemaphore]
ResListFilter [in CCSSeqSemaphore]
ResListFN [in CCSSeqSemaphore]
S
SeqParBackwardSimulationFailsContrasimulationHolds.Lemmas [in Examples]Sets [in NameSet]
SplitCombine [in Util]
Stepping [in CCSSeqSemaphore]
Stepping.Stepping [in LabeledTransitionSystems]
T
TraceEquivalence [in BisimTheory]Constructor Index
A
ai_later [in SfLib]ai_here [in SfLib]
all [in CharacteristicLogics]
B
bot [in CharacteristicLogics]boxer [in LibTactics]
C
conj [in CharacteristicLogics]D
disj [in CharacteristicLogics]E
ebisim_trans_false.s_s1' [in Examples]ebisim_trans_false.s_s1 [in Examples]
ebisim_trans_false.s_sR [in Examples]
ebisim_trans_false.s_sL [in Examples]
ebisim_trans_false.s_t1' [in Examples]
ebisim_trans_false.s_t1 [in Examples]
ebisim_trans_false.s_t2 [in Examples]
ebisim_trans_false.s0 [in Examples]
ebisim_trans_false.s1' [in Examples]
ebisim_trans_false.s2 [in Examples]
ebisim_trans_false.s1 [in Examples]
ev_SS [in SfLib]
ev_0 [in SfLib]
ExampleA.lstep_gi [in Examples]
ExampleA.lstep_fh [in Examples]
ExampleA.lstep_eg [in Examples]
ExampleA.lstep_ef [in Examples]
ExampleA.lstep_bd [in Examples]
ExampleA.lstep_bc [in Examples]
ExampleA.lstep_ab [in Examples]
ExampleA.Sa [in Examples]
ExampleA.Sb [in Examples]
ExampleA.Sc [in Examples]
ExampleA.Sd [in Examples]
ExampleA.Se [in Examples]
ExampleA.Sf [in Examples]
ExampleA.Sg [in Examples]
ExampleA.Sh [in Examples]
ExampleA.Si [in Examples]
ExampleB_Full.Rp_ex [in Examples]
ExampleB_Full.Rp_dw [in Examples]
ExampleB_Full.Rp_cx [in Examples]
ExampleB_Full.Rp_bw [in Examples]
ExampleB_Full.Rp_zz [in Examples]
ExampleB_Full.Rp_yy [in Examples]
ExampleB_Full.Rp_xx [in Examples]
ExampleB_Full.Rp_ww [in Examples]
ExampleB_Full.Rp_init [in Examples]
ExampleB_Full.tstep_Qqz [in Examples]
ExampleB_Full.tstep_Qpy [in Examples]
ExampleB_Full.tstep_Qoz [in Examples]
ExampleB_Full.tstep_Qny [in Examples]
ExampleB_Full.tstep_Qmz [in Examples]
ExampleB_Full.tstep_Qly [in Examples]
ExampleB_Full.tstep_Qkx [in Examples]
ExampleB_Full.tstep_Qjx [in Examples]
ExampleB_Full.tstep_Qiw [in Examples]
ExampleB_Full.tstep_Qhw [in Examples]
ExampleB_Full.tstep_Qgx [in Examples]
ExampleB_Full.tstep_Qfw [in Examples]
ExampleB_Full.tstep_Qem [in Examples]
ExampleB_Full.tstep_Qel [in Examples]
ExampleB_Full.tstep_Qdk [in Examples]
ExampleB_Full.tstep_Qdj [in Examples]
ExampleB_Full.tstep_Qci [in Examples]
ExampleB_Full.tstep_Qch [in Examples]
ExampleB_Full.tstep_Qbg [in Examples]
ExampleB_Full.tstep_Qbf [in Examples]
ExampleB_Full.tstep_Qad [in Examples]
ExampleB_Full.tstep_Qac [in Examples]
ExampleB_Full.tstep_Qab [in Examples]
ExampleB_Full.tstep_Pex [in Examples]
ExampleB_Full.tstep_Pdw [in Examples]
ExampleB_Full.tstep_Pce [in Examples]
ExampleB_Full.tstep_Pbd [in Examples]
ExampleB_Full.tstep_Pac [in Examples]
ExampleB_Full.tstep_Pab [in Examples]
ExampleB_Full.lstep_Qjq [in Examples]
ExampleB_Full.lstep_Qhp [in Examples]
ExampleB_Full.lstep_Qgo [in Examples]
ExampleB_Full.lstep_Qfn [in Examples]
ExampleB_Full.lstep_Qbe [in Examples]
ExampleB_Full.lstep_Sxz [in Examples]
ExampleB_Full.lstep_Swy [in Examples]
ExampleB_Full.Sz [in Examples]
ExampleB_Full.Sy [in Examples]
ExampleB_Full.Sx [in Examples]
ExampleB_Full.Sw [in Examples]
ExampleB_Full.Qq [in Examples]
ExampleB_Full.Qp [in Examples]
ExampleB_Full.Qo [in Examples]
ExampleB_Full.Qn [in Examples]
ExampleB_Full.Qm [in Examples]
ExampleB_Full.Ql [in Examples]
ExampleB_Full.Qk [in Examples]
ExampleB_Full.Qj [in Examples]
ExampleB_Full.Qi [in Examples]
ExampleB_Full.Qh [in Examples]
ExampleB_Full.Qg [in Examples]
ExampleB_Full.Qf [in Examples]
ExampleB_Full.Qe [in Examples]
ExampleB_Full.Qd [in Examples]
ExampleB_Full.Qc [in Examples]
ExampleB_Full.Qb [in Examples]
ExampleB_Full.Qa [in Examples]
ExampleB_Full.Pe [in Examples]
ExampleB_Full.Pd [in Examples]
ExampleB_Full.Pc [in Examples]
ExampleB_Full.Pb [in Examples]
ExampleB_Full.Pa [in Examples]
ExampleB'.lstep_df [in Examples]
ExampleB'.lstep_ce [in Examples]
ExampleB'.lstep_ab [in Examples]
ExampleB'.Rp_dd [in Examples]
ExampleB'.Rp_cc [in Examples]
ExampleB'.Rp_hh [in Examples]
ExampleB'.Rp_gg [in Examples]
ExampleB'.Rp_ff [in Examples]
ExampleB'.Rp_ee [in Examples]
ExampleB'.Rp_ia [in Examples]
ExampleB'.Sa [in Examples]
ExampleB'.Sb [in Examples]
ExampleB'.Sc [in Examples]
ExampleB'.Sd [in Examples]
ExampleB'.Se [in Examples]
ExampleB'.Sf [in Examples]
ExampleB'.Sg [in Examples]
ExampleB'.Sh [in Examples]
ExampleB'.Si [in Examples]
ExampleB'.tstep_id [in Examples]
ExampleB'.tstep_ic [in Examples]
ExampleB'.tstep_dh [in Examples]
ExampleB'.tstep_cg [in Examples]
ExampleB'.tstep_bf [in Examples]
ExampleB'.tstep_be [in Examples]
ExampleB'.tstep_ad [in Examples]
ExampleB'.tstep_ac [in Examples]
ExampleB.lstep_if [in Examples]
ExampleB.lstep_he [in Examples]
ExampleB.lstep_df [in Examples]
ExampleB.lstep_ce [in Examples]
ExampleB.lstep_ab [in Examples]
ExampleB.Rp_id [in Examples]
ExampleB.Rp_hc [in Examples]
ExampleB.Rp_dd [in Examples]
ExampleB.Rp_cc [in Examples]
ExampleB.Rp_ff [in Examples]
ExampleB.Rp_ee [in Examples]
ExampleB.Rp_ga [in Examples]
ExampleB.Sa [in Examples]
ExampleB.Sb [in Examples]
ExampleB.Sc [in Examples]
ExampleB.Sd [in Examples]
ExampleB.Se [in Examples]
ExampleB.Sf [in Examples]
ExampleB.Sg [in Examples]
ExampleB.Sh [in Examples]
ExampleB.Si [in Examples]
ExampleB.tstep_gi [in Examples]
ExampleB.tstep_gh [in Examples]
ExampleB.tstep_bf [in Examples]
ExampleB.tstep_be [in Examples]
ExampleB.tstep_ad [in Examples]
ExampleB.tstep_ac [in Examples]
ExampleC.lstep_fh [in Examples]
ExampleC.lstep_eg [in Examples]
ExampleC.lstep_ef [in Examples]
ExampleC.lstep_bc [in Examples]
ExampleC.lstep_ab [in Examples]
ExampleC.Sa [in Examples]
ExampleC.Sb [in Examples]
ExampleC.Sc [in Examples]
ExampleC.Sd [in Examples]
ExampleC.Se [in Examples]
ExampleC.Sf [in Examples]
ExampleC.Sg [in Examples]
ExampleC.Sh [in Examples]
ExampleD.coffee [in Examples]
ExampleD.lstep_ie [in Examples]
ExampleD.lstep_he [in Examples]
ExampleD.lstep_gi [in Examples]
ExampleD.lstep_fh [in Examples]
ExampleD.lstep_eg [in Examples]
ExampleD.lstep_ef [in Examples]
ExampleD.lstep_da [in Examples]
ExampleD.lstep_ca [in Examples]
ExampleD.lstep_bd [in Examples]
ExampleD.lstep_bc [in Examples]
ExampleD.lstep_ab [in Examples]
ExampleD.pay_cent [in Examples]
ExampleD.pick_coffee [in Examples]
ExampleD.pick_tea [in Examples]
ExampleD.Sa [in Examples]
ExampleD.Sb [in Examples]
ExampleD.Sc [in Examples]
ExampleD.Sd [in Examples]
ExampleD.Se [in Examples]
ExampleD.Sf [in Examples]
ExampleD.Sg [in Examples]
ExampleD.Sh [in Examples]
ExampleD.Si [in Examples]
ExampleD.tea [in Examples]
ExampleE.lstep_ec [in Examples]
ExampleE.lstep_ed [in Examples]
ExampleE.lstep_bd [in Examples]
ExampleE.lstep_ac [in Examples]
ExampleE.Sa [in Examples]
ExampleE.Sb [in Examples]
ExampleE.Sc [in Examples]
ExampleE.Sd [in Examples]
ExampleE.Se [in Examples]
ExampleE.tstep_ab [in Examples]
ExampleF.lstep_lg [in Examples]
ExampleF.lstep_kf [in Examples]
ExampleF.lstep_ie [in Examples]
ExampleF.lstep_dg [in Examples]
ExampleF.lstep_cf [in Examples]
ExampleF.lstep_be [in Examples]
ExampleF.Rc1_cj [in Examples]
ExampleF.Rc1_gg [in Examples]
ExampleF.Rc1_ff [in Examples]
ExampleF.Rc1_ee [in Examples]
ExampleF.Rc1_dl [in Examples]
ExampleF.Rc1_ck [in Examples]
ExampleF.Rc1_bi [in Examples]
ExampleF.Rc1_ah [in Examples]
ExampleF.Rc2_aj [in Examples]
ExampleF.Rc2_gg [in Examples]
ExampleF.Rc2_ff [in Examples]
ExampleF.Rc2_ee [in Examples]
ExampleF.Rc2_dl [in Examples]
ExampleF.Rc2_ck [in Examples]
ExampleF.Rc2_bi [in Examples]
ExampleF.Rc2_ah [in Examples]
ExampleF.Rd_gg [in Examples]
ExampleF.Rd_ff [in Examples]
ExampleF.Rd_ee [in Examples]
ExampleF.Rd_ld [in Examples]
ExampleF.Rd_kc [in Examples]
ExampleF.Rd_ib [in Examples]
ExampleF.Rd_dl [in Examples]
ExampleF.Rd_ck [in Examples]
ExampleF.Rd_cj [in Examples]
ExampleF.Rd_bi [in Examples]
ExampleF.Rd_ah [in Examples]
ExampleF.Rd_ha [in Examples]
ExampleF.Sa [in Examples]
ExampleF.Sb [in Examples]
ExampleF.Sc [in Examples]
ExampleF.Sd [in Examples]
ExampleF.Se [in Examples]
ExampleF.Sf [in Examples]
ExampleF.Sg [in Examples]
ExampleF.Sh [in Examples]
ExampleF.Si [in Examples]
ExampleF.Sj [in Examples]
ExampleF.Sk [in Examples]
ExampleF.Sl [in Examples]
ExampleF.tstep_jl [in Examples]
ExampleF.tstep_jk [in Examples]
ExampleF.tstep_hj [in Examples]
ExampleF.tstep_hi [in Examples]
ExampleF.tstep_ad [in Examples]
ExampleF.tstep_ac [in Examples]
ExampleF.tstep_ab [in Examples]
ExampleG.lstep_dg [in Examples]
ExampleG.lstep_cf [in Examples]
ExampleG.lstep_be [in Examples]
ExampleG.Rc1_cj [in Examples]
ExampleG.Rc1_gg [in Examples]
ExampleG.Rc1_ff [in Examples]
ExampleG.Rc1_ee [in Examples]
ExampleG.Rc1_dd [in Examples]
ExampleG.Rc1_cc [in Examples]
ExampleG.Rc1_bb [in Examples]
ExampleG.Rc1_ah [in Examples]
ExampleG.Rc2_aj [in Examples]
ExampleG.Rc2_gg [in Examples]
ExampleG.Rc2_ff [in Examples]
ExampleG.Rc2_ee [in Examples]
ExampleG.Rc2_dd [in Examples]
ExampleG.Rc2_cc [in Examples]
ExampleG.Rc2_bb [in Examples]
ExampleG.Rc2_ah [in Examples]
ExampleG.Rp_gg [in Examples]
ExampleG.Rp_ff [in Examples]
ExampleG.Rp_ee [in Examples]
ExampleG.Rp_dd [in Examples]
ExampleG.Rp_cc [in Examples]
ExampleG.Rp_bb [in Examples]
ExampleG.Rp_ah [in Examples]
ExampleG.Sa [in Examples]
ExampleG.Sb [in Examples]
ExampleG.Sc [in Examples]
ExampleG.Sd [in Examples]
ExampleG.Se [in Examples]
ExampleG.Sf [in Examples]
ExampleG.Sg [in Examples]
ExampleG.Sh [in Examples]
ExampleG.Sj [in Examples]
ExampleG.tstep_jd [in Examples]
ExampleG.tstep_jc [in Examples]
ExampleG.tstep_hj [in Examples]
ExampleG.tstep_hb [in Examples]
ExampleG.tstep_ad [in Examples]
ExampleG.tstep_ac [in Examples]
ExampleG.tstep_ab [in Examples]
Examples.SumPar.Rd1 [in CCSSeqSemaphore]
Examples.SumPar.Rd4 [in CCSSeqSemaphore]
Examples.SumSum.Rd1 [in CCSSeqSemaphore]
Examples.SumSum.Rd4 [in CCSSeqSemaphore]
ext [in CharacteristicLogics]
I
Id [in SfLib]L
ltac_mark [in LibTactics]ltac_wilds [in LibTactics]
ltac_wild [in LibTactics]
ltac_no_arg [in LibTactics]
LTS.lstep_out [in CCSSeqSemaphore]
LTS.lstep_in [in CCSSeqSemaphore]
l_out [in Labels]
l_in [in Labels]
l_tau [in Labels]
N
nn [in SfLib]P
phi1 [in CharacteristicLogics]phi2 [in CharacteristicLogics]
p_rep [in CCSSeqSemaphore]
p_res [in CCSSeqSemaphore]
p_act [in CCSSeqSemaphore]
p_seq [in CCSSeqSemaphore]
p_par [in CCSSeqSemaphore]
p_sum [in CCSSeqSemaphore]
p_nil [in CCSSeqSemaphore]
R
rep_step_result1 [in CCSSeqSemaphore]rep_step_result0 [in CCSSeqSemaphore]
rsc_step [in SfLib]
rsc_refl [in SfLib]
S
SeqParBackwardSimulationFailsContrasimulationHolds.p0 [in Examples]SeqParBackwardSimulationFailsContrasimulationHolds.p1 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.p2 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.p3 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.p4 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.p5 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.p6 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q0 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q1 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q2 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q3 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q4 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q5 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q6 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.q7 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.RR_66 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.RR_55 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.RR_44 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.RR_33 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.RR_22 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.RR_11 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.RR_00 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q46 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q24 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q07 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q35 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q13 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_p46 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_p24 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_p35 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_p13 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q74 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q73 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q02 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_q01 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_p02 [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.s_p01 [in Examples]
Stepping.lstep_lcons [in LabeledTransitionSystems]
Stepping.lstep_nil [in LabeledTransitionSystems]
Stepping.step_tcons [in LabeledTransitionSystems]
Stepping.step_lcons [in LabeledTransitionSystems]
Stepping.step_nil [in LabeledTransitionSystems]
s_res_nil__ [in CCSSeqSemaphore]
s_seq_nil__ [in CCSSeqSemaphore]
s_sum_nil__ [in CCSSeqSemaphore]
s_par_nil__ [in CCSSeqSemaphore]
s_rep__ [in CCSSeqSemaphore]
s_res_count_out__ [in CCSSeqSemaphore]
s_res_count_in__ [in CCSSeqSemaphore]
s_res__ [in CCSSeqSemaphore]
s_seq__ [in CCSSeqSemaphore]
s_sumR__ [in CCSSeqSemaphore]
s_sumL__ [in CCSSeqSemaphore]
s_parR__ [in CCSSeqSemaphore]
s_parL__ [in CCSSeqSemaphore]
s_act__ [in CCSSeqSemaphore]
s_res_nil [in CCSSeqSemaphore]
s_seq_nil [in CCSSeqSemaphore]
s_sum_nil [in CCSSeqSemaphore]
s_par_nil [in CCSSeqSemaphore]
s_rep [in CCSSeqSemaphore]
s_res_count_out [in CCSSeqSemaphore]
s_res_count_in [in CCSSeqSemaphore]
s_res [in CCSSeqSemaphore]
s_seq [in CCSSeqSemaphore]
s_sumR [in CCSSeqSemaphore]
s_sumL [in CCSSeqSemaphore]
s_parR [in CCSSeqSemaphore]
s_parL [in CCSSeqSemaphore]
s_act [in CCSSeqSemaphore]
T
top [in CharacteristicLogics]tot [in SfLib]
Notation Index
H
_ ⊨ᴬ _ (forces_scope) [in CharacteristicLogics]_ ⊨ᴱ _ (forces_scope) [in CharacteristicLogics]
⦋ _ ⦌ _ (scopeA) [in CharacteristicLogics]
〈 _ 〉 _ (scopeE) [in CharacteristicLogics]
_ ∨ _ (scopeE) [in CharacteristicLogics]
_ ∧ _ (scopeA) [in CharacteristicLogics]
¬ _ (scopeA) [in CharacteristicLogics]
¬ _ (scopeE) [in CharacteristicLogics]
N
_ ? (label_scope) [in Labels]_ ! (label_scope) [in Labels]
τ (label_scope) [in Labels]
_ ⊆ _ (nameset_scope) [in NameSet]
_ ⋂ _ (nameset_scope) [in NameSet]
_ ⋃ _ (nameset_scope) [in NameSet]
_ ∈ _ (nameset_scope) [in NameSet]
∅ (nameset_scope) [in NameSet]
_ / _ (nameset_scope) [in NameSet]
S
_ ⟶ _ ⟶ _ [in CCSSeqSemaphore]_ ⟶ _ ― _ → _ [in CCSSeqSemaphore]
_ ― _ → _ ⟶ _ [in CCSSeqSemaphore]
_ ― _ → _ ― _ → _ [in CCSSeqSemaphore]
_ ⟶ _ [in CCSSeqSemaphore]
_ ― _ → _ [in CCSSeqSemaphore]
_ - _ -> _ [in CCSSeqSemaphore]
_ ---> _ [in CCSSeqSemaphore]
Ø (proc_scope) [in CCSSeqSemaphore]
υ _ : _ (proc_scope) [in CCSSeqSemaphore]
υ _ : _ : _ (proc_scope) [in CCSSeqSemaphore]
τ. _ (proc_scope) [in CCSSeqSemaphore]
_ ?. _ (proc_scope) [in CCSSeqSemaphore]
_ ̄ !. _ (proc_scope) [in CCSSeqSemaphore]
_ ‖ _ (proc_scope) [in CCSSeqSemaphore]
_ !! (proc_scope) [in CCSSeqSemaphore]
O (proc_scope) [in CCSSeqSemaphore]
(). _ (proc_scope) [in CCSSeqSemaphore]
_ #: _ (proc_scope) [in CCSSeqSemaphore]
_ # _ : _ (proc_scope) [in CCSSeqSemaphore]
_ !. _ (proc_scope) [in CCSSeqSemaphore]
_ ?. _ (proc_scope) [in CCSSeqSemaphore]
_ ;; _ (proc_scope) [in CCSSeqSemaphore]
_ || _ (proc_scope) [in CCSSeqSemaphore]
_ + _ (proc_scope) [in CCSSeqSemaphore]
other
>> _ _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]>> _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ (ltac_scope) [in LibTactics]
>> _ _ (ltac_scope) [in LibTactics]
>> _ (ltac_scope) [in LibTactics]
>> (ltac_scope) [in LibTactics]
___ (ltac_scope) [in LibTactics]
__ (ltac_scope) [in LibTactics]
exists _ _ _ _ _ _ _ _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ _ _ _ _ _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ _ _ _ _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ _ _ _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ _ _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ _ , _ (type_scope) [in LibTactics]
exists _ _ , _ (type_scope) [in LibTactics]
exists _ , _ (type_scope) [in LibTactics]
_ =' _ [in LibTactics]
_ ++ _ [in SfLib]
nosimpl _ [in LibTactics]
Register _ _ [in LibTactics]
Something [in LibTactics]
[ _ , .. , _ ] [in SfLib]
[ ] [in SfLib]
Inductive Index
A
appears_in [in SfLib]B
Boxer [in LibTactics]E
ebisim_trans_false.lstep [in Examples]ebisim_trans_false.tstep [in Examples]
ebisim_trans_false.state [in Examples]
empty_relation [in SfLib]
ev [in SfLib]
ExampleA.lstep [in Examples]
ExampleA.state [in Examples]
ExampleA.tstep [in Examples]
ExampleB_Full.Rp [in Examples]
ExampleB_Full.tstep [in Examples]
ExampleB_Full.lstep [in Examples]
ExampleB_Full.state [in Examples]
ExampleB'.lstep [in Examples]
ExampleB'.Rp [in Examples]
ExampleB'.state [in Examples]
ExampleB'.tstep [in Examples]
ExampleB.lstep [in Examples]
ExampleB.Rp [in Examples]
ExampleB.state [in Examples]
ExampleB.tstep [in Examples]
ExampleC.lstep [in Examples]
ExampleC.state [in Examples]
ExampleC.tstep [in Examples]
ExampleD.label [in Examples]
ExampleD.lstep [in Examples]
ExampleD.state [in Examples]
ExampleD.tstep [in Examples]
ExampleE.lstep [in Examples]
ExampleE.state [in Examples]
ExampleE.tstep [in Examples]
ExampleF.lstep [in Examples]
ExampleF.Rc1 [in Examples]
ExampleF.Rc2 [in Examples]
ExampleF.Rd [in Examples]
ExampleF.state [in Examples]
ExampleF.tstep [in Examples]
ExampleG.lstep [in Examples]
ExampleG.Rc1 [in Examples]
ExampleG.Rc2 [in Examples]
ExampleG.Rp [in Examples]
ExampleG.state [in Examples]
ExampleG.tstep [in Examples]
Examples.SumPar.Rd [in CCSSeqSemaphore]
Examples.SumSum.Rd [in CCSSeqSemaphore]
I
id [in SfLib]L
label [in Labels]ltac_Mark [in LibTactics]
ltac_Wilds [in LibTactics]
ltac_Wild [in LibTactics]
ltac_No_arg [in LibTactics]
LTS.lstep [in CCSSeqSemaphore]
N
next_nat [in SfLib]P
phi [in CharacteristicLogics]phiA [in CharacteristicLogics]
phiE [in CharacteristicLogics]
proc [in CCSSeqSemaphore]
R
refl_step_closure [in SfLib]rep_step_result [in CCSSeqSemaphore]
S
SeqParBackwardSimulationFailsContrasimulationHolds.lstep [in Examples]SeqParBackwardSimulationFailsContrasimulationHolds.RR [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.state [in Examples]
SeqParBackwardSimulationFailsContrasimulationHolds.tstep [in Examples]
step [in CCSSeqSemaphore]
Stepping.lstep_star [in LabeledTransitionSystems]
Stepping.step_star [in LabeledTransitionSystems]
step__ [in CCSSeqSemaphore]
T
total_relation [in SfLib]Definition Index
A
admit [in SfLib]B
beq_id [in SfLib]ble_nat [in SfLib]
bn [in CCSSeqSemaphore]
bnl [in Labels]
botA [in CharacteristicLogics]
C
contrasimilar [in BisimTheory]contrasimulation [in BisimTheory]
converges [in CCSSeqSemaphore]
converges' [in CCSSeqSemaphore]
coupled_similar [in BisimTheory]
coupled_similar' [in BisimTheory]
coupled_simulation_flipping [in BisimTheory]
D
deterministic_lts [in LabeledTransitionSystems]deterministic_internal_choice [in BisimTheory]
E
ebisim_trans_false.lts [in Examples]empty [in SfLib]
eq' [in LibTactics]
esim_list [in CCSSeqSemaphore]
eventually_bisimilar [in BisimTheory]
eventually_similar [in BisimTheory]
eventual_simulation [in BisimTheory]
ExampleA.label [in Examples]
ExampleA.lts [in Examples]
ExampleB_Full.lts [in Examples]
ExampleB_Full.is_halted [in Examples]
ExampleB_Full.label [in Examples]
ExampleB'.is_halted [in Examples]
ExampleB'.label [in Examples]
ExampleB'.lts [in Examples]
ExampleB.is_halted [in Examples]
ExampleB.label [in Examples]
ExampleB.lts [in Examples]
ExampleC.label [in Examples]
ExampleC.lts [in Examples]
ExampleD.lts [in Examples]
ExampleE.label [in Examples]
ExampleE.lts [in Examples]
ExampleF.is_halted [in Examples]
ExampleF.label [in Examples]
ExampleF.lts [in Examples]
ExampleG.is_halted [in Examples]
ExampleG.label [in Examples]
ExampleG.lts [in Examples]
Examples.list_lts_S_list_proc [in CCSSeqSemaphore]
Examples.SumPar.p_par_sum [in CCSSeqSemaphore]
Examples.SumPar.p_sum_par [in CCSSeqSemaphore]
Examples.SumSum.p_sum2 [in CCSSeqSemaphore]
Examples.SumSum.p_sum1 [in CCSSeqSemaphore]
extend [in SfLib]
F
fn [in CCSSeqSemaphore]fnl [in Labels]
fn_out [in CCSSeqSemaphore]
fn_in [in CCSSeqSemaphore]
forces [in CharacteristicLogics]
forcesA [in CharacteristicLogics]
forcesE [in CharacteristicLogics]
G
get_step_rep_p' [in CCSSeqSemaphore]H
hidden_fn [in CCSSeqSemaphore]hml_equiv [in CharacteristicLogics]
hml_equivE [in CharacteristicLogics]
hml_equivA [in CharacteristicLogics]
hml_implE [in CharacteristicLogics]
hml_implA [in CharacteristicLogics]
I
image_finite [in CharacteristicLogics]image_finite_R [in CharacteristicLogics]
interleaving [in Labels]
inv [in BisimTheory]
L
list_disjE [in CharacteristicLogics]list_conjA [in CharacteristicLogics]
list_zeros [in Util]
list_rep [in Util]
list_le [in Util]
list_plus [in Util]
list_pair_fun [in Util]
list_rep [in CCSSeqSemaphore]
ltac_something [in LibTactics]
ltac_to_generalize [in LibTactics]
ltac_tag_subst [in LibTactics]
ltac_nat_from_int [in LibTactics]
ltac_database [in LibTactics]
LTS.is_halted [in CCSSeqSemaphore]
LTS.lts [in CCSSeqSemaphore]
M
Morphisms.p_ssum [in CCSSeqSemaphore]Morphisms.p_ssumR [in CCSSeqSemaphore]
Morphisms.p_ssumL [in CCSSeqSemaphore]
N
name [in NameSet]nameset [in NameSet]
name_eq [in NameSet]
negA [in CharacteristicLogics]
negE [in CharacteristicLogics]
nl [in Labels]
O
one_way_termination_sensitive [in BisimTheory]P
partial_contrasimilar [in BisimTheory]partial_coupled_similar [in BisimTheory]
partial_map [in SfLib]
partial_function [in SfLib]
par_bisimilar [in BisimTheory]
par_bisimulation [in BisimTheory]
par_simulation [in BisimTheory]
par_list [in CCSSeqSemaphore]
par_swap [in CCSSeqSemaphore]
pcsim_list [in CCSSeqSemaphore]
Pos_OWL.eq_leibniz [in NameSet]
p_res_list [in CCSSeqSemaphore]
R
relation [in SfLib]res_list_count_labels_min [in CCSSeqSemaphore]
res_list_count_labels [in CCSSeqSemaphore]
res_list_filter [in CCSSeqSemaphore]
res_count_labels [in CCSSeqSemaphore]
res_filter [in CCSSeqSemaphore]
rm [in LibTactics]
S
sbisimilar [in BisimTheory]SeqParBackwardSimulationFailsContrasimulationHolds.lts [in Examples]
stable_bisimulation [in BisimTheory]
Stepping.stable [in LabeledTransitionSystems]
step_ind' [in CCSSeqSemaphore]
step_res_list_label_wf [in CCSSeqSemaphore]
strong_bisimulation [in BisimTheory]
strong_simulation [in BisimTheory]
strong_one_way_termination_sensitive [in BisimTheory]
T
term_impl [in CCSSeqSemaphore]TestParallelization.l0 [in CCSSeqSemaphore]
TestParallelization.l1 [in CCSSeqSemaphore]
TestParallelization.l2 [in CCSSeqSemaphore]
topE [in CharacteristicLogics]
trace_equivalent [in BisimTheory]
tstep_contrasimulation [in BisimTheory]
tstep_weak_bisimulation [in BisimTheory]
W
wbisimilar [in BisimTheory]wbisim_list [in CCSSeqSemaphore]
weakly_image_finite [in CharacteristicLogics]
weak_bisimulation [in BisimTheory]
weak_simulation [in BisimTheory]
Module Index
E
ebisim_trans_false [in Examples]ExampleA [in Examples]
ExampleB [in Examples]
ExampleB_Full [in Examples]
ExampleB' [in Examples]
ExampleC [in Examples]
ExampleD [in Examples]
ExampleE [in Examples]
ExampleF [in Examples]
ExampleG [in Examples]
Examples [in CCSSeqSemaphore]
Examples.SumPar [in CCSSeqSemaphore]
Examples.SumSum [in CCSSeqSemaphore]
ExampleTactics [in Examples]
L
LibTacticsCompatibility [in LibTactics]LTS [in CCSSeqSemaphore]
M
Morphisms [in CCSSeqSemaphore]N
NameSet [in NameSet]NameSetFacts [in NameSet]
NameSetProps [in NameSet]
Notation [in NameSet]
Notation [in Labels]
Notation [in CCSSeqSemaphore]
Notation.U [in CCSSeqSemaphore]
P
PMapFacts [in NameSet]Pos_OWL [in NameSet]
S
SeqParBackwardSimulationFailsContrasimulationHolds [in Examples]StepNotation [in CCSSeqSemaphore]
StepNotation.U [in CCSSeqSemaphore]
Stepping [in LabeledTransitionSystems]
SyntaxNotation [in CCSSeqSemaphore]
SyntaxNotation.TestNotation [in CCSSeqSemaphore]
SyntaxNotation.U [in CCSSeqSemaphore]
T
TestParallelization [in CCSSeqSemaphore]Axiom Index
I
inj_pair2 [in LibTactics]Variable Index
B
Bisimulation.lts [in BisimTheory]E
equatesLemma.A0 [in LibTactics]equatesLemma.A1 [in LibTactics]
equatesLemma.A2 [in LibTactics]
equatesLemma.A3 [in LibTactics]
equatesLemma.A4 [in LibTactics]
equatesLemma.A5 [in LibTactics]
equatesLemma.A6 [in LibTactics]
H
HML_DecoupledBisimulation.lts [in CharacteristicLogics]S
skip_axiom [in LibTactics]Stepping.Stepping.lts [in LabeledTransitionSystems]
T
TestParallelization.M [in CCSSeqSemaphore]TestParallelization.N [in CCSSeqSemaphore]
TraceEquivalence.lts [in BisimTheory]
Library Index
B
BisimTheoryC
CCSSeqSemaphoreCharacteristicLogics
E
ExamplesL
LabeledTransitionSystemsLabels
LibTactics
N
NameSetS
SfLibU
Util| 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 | (1466 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 | (2 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 | (7 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 | (1 entry) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (673 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 | (41 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 | (405 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 | (75 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (69 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 | (134 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 | (34 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 | (1 entry) |
| 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 | (14 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 | (10 entries) |
This page has been generated by coqdoc