RV-CuBES
An International Workshop on Competitions, Usability, Benchmarks, Evaluation,
and Standardisation for Runtime Verification Tools
Held in conjunction with the 17th International Conference on Runtime
Verification (RV 2017)
http://rv2017.cs.manchester.ac.uk/rv-cubes/
The goal of this w
Hi,
Currently I have the following Datatype "(‘a, ‘b) CCS" which supports binary
“sum” operation:
val _ = Datatype `CCS = nil
| var 'a
| prefix ('b Action) CCS
| sum CCS CCS
...`;
I also have a recursive function for calculating
Hi again ...
Suppose I have the following things:
1. An equivalence relation R (|- equivalence R) for type ‘a
2. A ONE-ONE function f (:num->’a). It’s known that all its values are distinct
according to R.
3. A finite set J of values of the same type.
What theorems could assert the existence of
