Errata TOCL'15
Definition 4.4: While correct as stated, the notion of differential expressiveness should have limited the formula G to be in L, in which case the notion is more interesting. All proofs about differential expressiveness work in that case. Also see 

Definition A.1:(5) The union for sequential compositions should be for t^g(\beta)(|t|_s) instead of g(\beta)(|t|_s) to retain the prefix t of the tree similar to case (6) for repetitions.

[1] Andre Platzer. A complete uniform substitution calculus for differential dynamic logic.  Journal of Automated Reasoning, 59(2), pp. 219-265, 2017. DOI 10.1007/s10817-016-9385-1

[2] Andre Platzer. Uniform substitution at one fell swoop. In Pascal Fontaine, editor, CADE, volume 11716 of LNCS, pp. 425-441. Springer, 2019. DOI 10.1007/978-3-030-29436-6_25