| Figure 1: |
state,
tstep,
lstep
|
| labeled transition system (LTS): |
labeled_transition_system
|
| Definition 1: |
weak_simulation
|
| Definition 2: |
weak_bisimulation,
wbisimilar
|
| Lemma 1: |
wsim_backward_false
|
| Definition 3: |
eventual_simulation,
eventually_similar
|
| Lemma 2: |
wbisim_esim
|
| Lemma 3: |
esim_refl,
esim_trans
|
| Lemma 4: |
esim_true
|
| Figure 2 (CCS-Seq): |
proc,
step
|
| Definition 4: |
p_res_list
|
| Definition 5: |
one_way_termination_sensitive
|
| Definition 6: |
weak_bisimulation,
wbisimilar
|
| Definition 7: |
eventual_simulation,
eventually_similar
|
| Lemma 5 (Compositional properties): |
wbisim_par,
wbisim_act,
wbisim_rep,
wbisim_res,
wbisim_seq2,
wbisim_internal_sum,
wbisim_seq1,
esim_par,
esim_act,
esim_rep,
esim_res,
esim_seq2,
esim_internal_sum,
esim_seq1
|
| Lemma 6: |
SumPar.wsim_backward_false,
SumPar.esim_true
|
| Proposition 1: |
esim_seq_par_simpl
|
| Proposition 2: |
pbisim_seq_par,
esim_seq_par
|
| Lemma 7: |
esim_M_N
|
| Definition 8: |
eventually_bisimilar
|
| Figure 3: |
ebisim_trans_false
|
| Lemma 8: |
esim_ebisim1,
esim_ebisim2
|
| Definition 9: |
contrasimulation,
partial_contrasimilar,
contrasimilar
|
| Lemma 9: |
ebisim_csim
|
| Lemma 10: |
csim_refl,
csim_symm,
csim_trans
|
| Definition 10: |
trace_equivalent
|
| Lemma 11: |
csim_trace_equivalent
|
| Theorem 1: |
det_internal_choice_csim_wbisim
|
| Definition 11: |
contrasimilar
|
| Lemma 12 (Compositional properties): |
csim_par,
csim_act,
csim_rep,
csim_res,
csim_seq2,
csim_internal_sum,
csim_seq1
|
| Definition 12: |
stable
|
| Lemma 13: |
csim_internal_sum,
csim_stable_sum
|
| Lemma 14: |
SumSum.wsim_backwards_false
SumSum.esim_true,
|
| Definition 13: |
res_list_filter
|
| Definition 14: |
res_count_labels,
res_list_count_labels
|
| Definition 15 (Silent termination): |
converges,
converges',
converges_converges'_equiv
|
| Definition 16: |
term_impl
|
| Definitions 17 & 18: |
fn_in,
fn_out,
fn
|
| Lemma 15: |
seq_par_inversion
|
| Lemma 16: |
par_seq_inversion
|
| Theorem 2: |
pbisim_seq_par,
esim_seq_par
|
| Corollary 1: |
esim_seq_par_simpl
|