Encode fr relation

Beware that this encoding is different from the one in the literature.
In particular, the antecedents in the fr-encoding rely on the ones in
the read-from (rf) relation. Proofs about these encodings is subject
of future work.