Add theorems about R.
Update obsolete '_eqn' terms.
Solved optimize_0plus_b_sound.
Add an example.
Add examples.
Update subseq definition for accrate pattern match.
Solved subseq_trans.