English
If a → b in m1 steps and b → c in m2 steps, then a → c in m2 + m1 steps: transitivity with step counts.
Русский
Если a переходит в b за m1 шагов и b в c за m2 шагов, то a переходит в c за m2 + m1 шагов: транспозиция по количеству шагов.
LaTeX
$$$$ \\text{If } E^{\\text{InTime}}(f,a,b,m_1) \\text{ and } E^{\\text{InTime}}(f,b,c,m_2), \\text{ then } E^{\\text{InTime}}(f,a,c,m_2+m_1). $$$$
Lean4
/-- Transitivity of `EvalsToInTime` in the sum of the numbers of steps. -/
@[trans]
def trans {σ : Type*} (f : σ → Option σ) (m₁ : ℕ) (m₂ : ℕ) (a : σ) (b : σ) (c : Option σ) (h₁ : EvalsToInTime f a b m₁)
(h₂ : EvalsToInTime f b c m₂) : EvalsToInTime f a c (m₂ + m₁) :=
⟨EvalsTo.trans f a b c h₁.toEvalsTo h₂.toEvalsTo, add_le_add h₂.steps_le_m h₁.steps_le_m⟩
