Science Overview
All Publications
Talks
PhD
CCSL
Robin
PhD Overview
Table of Contents
Detailed description
of the files in this directory
Download area
| File | Theory | Name of lemmas | |
|---|---|---|---|
| Lemma 2.4.5 (1) | fibprops.pvs | PredProps | mon_prod, mon_coprod, mon_exp |
| Lemma 2.4.5 (2) | fibprops.pvs | RelProps | mon_prod, mon_coprod, mon_exp |
| Lemma 2.4.6 (1) | fibrations.pvs | Bc, BCRel | bc, bc_rel |
| Lemma 2.4.6 (2) | fibrations.pvs | Frobenius, | frobenius |
| FrobeniusRel | frobenius_rel | ||
| Lemma 2.4.7 | fibprops.pvs | PredProps | truth_prod, truth_coprod, truth_exp |
| Lemma 2.4.8 | fibprops.pvs | RelProps | eq_prod, eq_coprod, eq_exp |
| Lemma 2.4.9 (1) | fibprops.pvs | PredProps | coll_and_prod, coll_and_coprod, coll_and_exp_pol, coll_and_exp |
| Lemma 2.4.9 (2) | fibprops.pvs | RelProps | coll_and_prod, coll_and_coprod, coll_and_exp_pol, coll_and_exp |
| Lemma 2.4.10 (1) | fibprops.pvs | PredProps | coll_or_prod, coll_or_coprod, coll_or_exp_pol |
| Lemma 2.4.10 (2) | fibprops.pvs | RelProps | coll_or_prod, coll_or_coprod,coll_or_exp_pol |
| Lemma 2.4.11 | fibprops.pvs | RelPropsOp | op_prod, op_coprod, op_exp |
| Lemma 2.4.12 | fibprops.pvs | RelProps | comp_prod, comp_coprod,comp_exp_pol, comp_exp_left |
| Lemma 2.4.13 | fibprops.pvs | BisimProjProp | times, sum, exp_pol, exp_left |
| Lemma 2.4.14 | fibprops.pvs | CapInvProp | times, sum, exp, exp_pol, exp_nonempty |
| Lemma 2.4.15 (1) | fibprops.pvs | FibProps | fibred_product, fibred_coproduct, fibred_exp |
| Lemma 2.4.15 (2) | fibprops.pvs | FibRel | rel_prod_fib, rel_coprod_fib, rel_exp_fib |
| Example 2.4.16 | exp.pvs | ExpCounter2 | |
| Lemma 2.4.17 (1) | fibprops.pvs | FibProps | cofibred_product, cofibred_coproduct |
| Lemma 2.4.17 (1) | fibprops.pvs | CofibRel | rel_prod_cofib, rel_coprod_cofib |
| Lemma 2.4.17 (2) | fibprops.pvs | FibProps | const_exp1 |
| Lemma 2.4.17 (3) | fibprops.pvs | CofibRel | rel_exp_cofib1 |
| Equation 2.7 | fibrations.pvs | PredCont | graf, graf2 |
| Equation 2.7 | fibrations.pvs | BCfor_graph | |
| Equation 3.1 | per.pvs | PerUnion | percl_rel_exp_pol_coll |
| Fact 3.3.7 (1) | intersection.pvs | InterCounter | |
| Fact 3.3.7 (1) | union.pvs | UnionBisim | |
| Fact 3.3.7 (2) | relcomp.pvs | BisimComp | |
| Fact 3.3.7 (3) | graph.pvs | GraphCounter | |
| Fact 3.3.7 (4) | image_morph.pvs | Image_Morph_counter | |
| Fact 3.3.7 (5) | mendler_counter.pvs | ||
| Fact 3.3.7 (6) | inv-char.pvs | InvCharCounter | |
| Fact 3.3.7 (7) | invariant.pvs | BisimProjCounter | |
| Fact 3.3.7 (8) | invariant.pvs | BisimCapInvCounter | |
| Fact 3.3.7 (9) | kernel.pvs | KernelCounter | |
| Example 3.3.8 | t.pvs | ||
| Example 3.3.8 | intersection.pvs | InterCounter | |
| Example 3.3.9 | union.pvs | UnionBisim | |
| Example 3.3.11 | aczel.pvs | counter3 | Fun_not_T |
| Example 3.3.12 | aczel.pvs | counter3 | Bisim_not_T |
| Lemma 3.4.10 | invariant.pvs | BisimProj | bisim_proj_const, bisim_proj_id, bisim_proj_times, bisim_proj_plus, bisim_proj_exp, bisim_proj_exp_epf |
| Example 3.4.12 | invariant.pvs | BisimProjCounter | |
| Lemma 3.4.13 | invariant.pvs | BisimCapInv | bisim_cap_inv_const, bisim_cap_inv_id, bisim_cap_inv_prod, bisim_cap_inv_coprod, bisim_cap_inv_exp, bisim_cap_inv_exp_epf |
| Example 3.4.15 | invariant.pvs | BisimCapInvCounter | |
| Example 3.4.17 | image_morph.pvs | Image_Morph_counter | |
| Example 3.4.19 | inv-char.pvs | InvCharCounter | |
| Proposition 3.4.20 | aczel.pvs | ||
| Lemma 3.4.29 | per.pvs | PReflexive | prefl_union |
| Lemma 3.5.2 (1) | per.pvs | PerLift | per_eq, per_sum, per_prod, per_exp |
| Lemma 3.5.3 | per.pvs | DomainLift | domain_sum, domain_prod, domain_exp_pol |
| Lemma 3.5.4 (1) | per.pvs | PerLift | per_cl_sum |
| Lemma 3.5.4 (2) | per.pvs | PerLift | per_cl_prod |
| Lemma 3.5.5 (1) | per.pvs | PerUnion | percl_rel_prod_coll |
| Lemma 3.5.5 (2) | per.pvs | PerUnion | percl_rel_sum_coll |
| Equation 3.1 | per.pvs | PerUnion | percl_rel_exp_pol_coll |
| Lemma 3.5.8 | per.pvs | extended | |
| Example 3.5.10 | perlift_counter.pvs | PerBisimCounter2 | |
| Proposition 3.6.1 | union.pvs | KNoFinal | |
| Lemma 3.7.1 (1) | rellist.pvs | PredList | predlist_mon |
| Lemma 3.7.1 (1) | rellist.pvs | RelList | rellist_mon |
| Lemma 3.7.1 (2) | rellist.pvs | FibPredList, FibRelList | |
| Lemma 3.7.1 (3) | rellist.pvs | PredListProps, RelListProps, CapInvProj | |
| Lemma 3.7.1 (4) | rellist.pvs | RelListPer | |
| Lemma 4.2.2 (1) | variance.pvs | Variance | join_well, subst_well |
| Lemma 4.2.2 (2) | variance.pvs | Variance | subst_comm, subst_asso, subst_zero |
| Lemma 4.2.2 (3) | variance.pvs | Variance | join_comm, join_asso, join_id |
| Lemma 4.2.2 (4) | variance.pvs | Variance | distrib |
| Example 4.4.6 | Queue_model.pvs | QueueModel | |
| Example 4.5.10 | variance.pvs | QueueModal |
Home
Science Overview
All Publications
Talks
PhD
CCSL
Robin