Strict inversion of an additive restarted clock

Finite strict inverses of a monotone clock respect restart at an attained level.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VI.

theorem BGW.StableTrees.supLadderTime_add_of_clock_restart {θ : ℝ} {f g : Skorokhod.DLoc} {z s : NNReal} (hm : Monotone (supLocalTime θ f)) (hf : ∀ (w : NNReal), supLocalTimeInverse θ f w = ↑(supLadderTime θ w f)) (hg : ∀ (w : NNReal), supLocalTimeInverse θ g w = ↑(supLadderTime θ w g)) (hs : supLocalTime θ f s = ↑z) (hrestart : ∀ (t : NNReal), supLocalTime θ f (s + t) = ↑z + supLocalTime θ g t) (u : NNReal) : supLadderTime θ (z + u) f = s + supLadderTime θ u g

A clock restart at level z implies addition of its finite strict inverses.