English
If two computations S and T are related by a LiftRel Equiv relation, then the property of promising a value a is equivalent for S and T.
Русский
Если два вычисления S и T связаны отношением LiftRel Equiv, то свойство обещания значения a эквивалентно для S и T.
LaTeX
$$$ \forall {S,T},\ S,LiftRel Equiv T \rightarrow (\forall s\in S, s \Rightarrow s.Promises a) \leftrightarrow (\forall t\in T, t.Promises a).$$$
Lean4
theorem parallel_congr_lem {S T : WSeq (Computation α)} {a} (H : S.LiftRel Equiv T) :
(∀ s ∈ S, s ~> a) ↔ ∀ t ∈ T, t ~> a :=
⟨fun h1 _ tT =>
let ⟨_, sS, se⟩ := WSeq.exists_of_liftRel_right H tT
(promises_congr se _).1 (h1 _ sS),
fun h2 _ sS =>
let ⟨_, tT, se⟩ := WSeq.exists_of_liftRel_left H sS
(promises_congr se _).2 (h2 _ tT)⟩
-- The parallel operation is only deterministic when all computation paths lead to the same value
