CSSK Axiomatisation

[aubertc]

We could implement the axiomatisation of CSSK (cf. Fig. 3), knowing that:

fn(a.P) = fn(P) $\cup$ {a, 'a}
fn('a.P) = fn(P) $\cup$ {a, 'a}
fn(P + Q) = fn(P) $\cup$ fn(Q)
fn(P | Q) = fn(P) $\cup$ fn(Q)
fn(0) = $\emptyset$
fn(P \ a) = fn(P) \ {a, 'a} (in the sense "fn(P) minus a, 'a")

and std(X) is X without its keys (its "standard" form)

[aubertc]

I guess that the meaning of this issue is "couldn't we use this to solve #22", so it is not really a bug report, more like a question.