English
If every s ∈ S promises a and S is lift-relatable to T, then (parallel S) is equivalent to (parallel T); moreover, the equivalence respects the promises of components.
Русский
Если для всех s ∈ S обещано a и S сопоставимо по LiftRel с T, то parallel S эквивалентен parallel T; аналогично сохраняется обещание компонент.
LaTeX
$$$ \forall S,T, a: \alpha, (S).Promises a \Rightarrow (T).Promises a \Rightarrow (\mathrm{parallel}(S)) \Equiv (\mathrm{parallel}(T)).$$$
Lean4
theorem parallel_congr_left {S T : WSeq (Computation α)} {a} (h1 : ∀ s ∈ S, s ~> a) (H : S.LiftRel Equiv T) :
parallel S ~ parallel T :=
let h2 := (parallel_congr_lem H).1 h1
fun a' =>
⟨fun h => by
have aa := parallel_promises h1 h
rw [← aa]
rw [← aa] at h
exact
let ⟨s, sS, as⟩ := exists_of_mem_parallel h
let ⟨t, tT, st⟩ := WSeq.exists_of_liftRel_left H sS
let aT := (st _).1 as
mem_parallel h2 tT aT,
fun h => by
have aa := parallel_promises h2 h
rw [← aa]
rw [← aa] at h
exact
let ⟨s, sS, as⟩ := exists_of_mem_parallel h
let ⟨t, tT, st⟩ := WSeq.exists_of_liftRel_right H sS
let aT := (st _).2 as
mem_parallel h1 tT aT⟩
