Изменения

{{Определение

|id = global_time_model

'''Модель глобального времени''' определим так, что это модель, в которой в качестве '''операции''' используется временной интервал: <tex> e = [t_{inv}(e), t_{res}(e)], </tex> причём <tex> t_{inv}(e), t_{res}(e) \in \mathbb{R} </tex>. Зададим в этой модели отношение <tex> \rightarrow </tex> следующим образом: <tex> e \rightarrow f = t_{inv}(f) > t_{res}(e) </tex>. Неформально это означает, что вход в функцию, выполняющую операцию <tex> f </tex>, был осуществлён строго позже, чем был получен результат работы функции, выполняющей операцию <tex> e </tex>. <br />'''Замечание''': глобального времени не существует из-за физических ограничений, поэтому в доказательствах такая модель не используется, но помогает при визуализации различных исполнений

}}