You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
There's a fair few lemmas and definitions within the codebase which are axiomised, and would be good to fill in:
Species
Some decision procedure for species equivalence.
Prime decomposition of species. Here we mostly need to be able to show things like is_prime nil.
Transitions
transition.rename_from - Effectively undoes a transition - if we have (rename A) —[a]→ E, then there is some a', E' such that rename a' = a, and likewise for E'.
Show that transition.equivalent_of is a bijection.
Provide some way of enumerating over every transition. Ideally as a fintype, but as a multiset/finset otherwise.
Decision procedure for transition equality.
Semantics
Show appropriate equalities for dP/dt and ∂P under ≡⁺.
Show process spaces are embedded in processes.
Non-cπ related
fin_fn.bind_distrib (fin_fn.bind distributes over +)
There's a fair few lemmas and definitions within the codebase which are axiomised, and would be good to fill in:
Species
is_prime nil.Transitions
transition.rename_from- Effectively undoes a transition - if we have(rename A) —[a]→ E, then there is some a', E' such thatrename a' = a, and likewise for E'.transition.equivalent_ofis a bijection.Semantics
Non-cπ related
fin_fn.bind_distrib(fin_fn.binddistributes over+)fin_fn.bind₂_swap(fin_fn.bind₂can be swapped).