Base.Base
- Base Library for ICL
- De Morgan laws
- Size recursion
- Iteration
- Decidability
- Lists
- Decidability laws for lists
- Membership
- Disjointness
- Inclusion
- Setoid rewriting with list inclusion and list equivalence
- Equivalence
- Filter
- Element removal
- Cardinality
- Duplicate-free lists
- Power lists
- Finite closure iteration
- Deprecated names, defined for backward compatibilitly
HOcore.Prelim
HOcore.ComplLat
- Monotonicity
- Relation inclusion
- Pointwise extension of relation inclusion to functions
- Reflexive closure
- Union
- Extensiveness
- (Pre-, Post-, Greatest) Fixed Points
- Congruence
- Soundness and Correctness
- Intersection
- Transposition
- Symmetry
- Relation composition
- Monoid preservation
- Decreasify
- Increasify
- Monotonization
HOcore.Compat
- Definition
- Primitive compatible functions
- Closure properties
- Congruence
- Monotonization
- Compat implies soundness
HOcore.CondClos
HOcore.HoCore
HOcore.Multiset
HOcore.Ren
- Preliminaries
- Injective renamings
- Decidable injective renamings
- Bijective renamings
- Inclusions of renaming classes
- Preservation of renamings
HOcore.Subst
- Substitutivity of transitions
- Propagation via context
- Inversion lemmas for transitions of substituted processes
- Substitution Closure
HOcore.Bis
- Definitions of bisimilarity components through their functionals
- Monotonicity of functionals
- Preservation of the monoid (part 1): 1 <2= s(1)
- Preservation of the monoid (part 2): s x ° s y <2= s(x ° y)
HOcore.BisDecInjRen
HOcore.BisSubstit
HOcore.BisCongr
- Context closures for send, ceceive and parallel construct
- Weaker notion of CondClos
- Congruence for send closure
- Congruence for receive closure
- Congruence for parallel closure
HOcore.UpToNu
HOcore.IoCxtBis
- IO cxt bis is closed under decidable injective renamings
- IO cxt bis is substitutive
- IO cxt bis is a congruence
- Soundness of up-to bisimilarity technique
HOcore.IoMultiBis
- IO multi bis is closed under decidable injective renamings
- Soundness of up-to bisimilarity technique
HOcore.InclIoMultiBisIoCxtBis
- Connection between unguarded variable occurrence and variable context transitions
- f_reach
- CondClos for s_ho_out, s_ho_in, s_var_multi
- Main result