# Documentation

Mathlib.Data.Seq.Parallel

# Parallel computation #

Parallel computation of a computable sequence of computations by a diagonal enumeration. The important theorems of this operation are proven as terminates_parallel and exists_of_mem_parallel. (This operation is nondeterministic in the sense that it does not honor sequence equivalence (irrelevance of computation time).)

def Computation.parallel.aux2 {α : Type u} :
List ()α List ()
Instances For
def Computation.parallel.aux1 {α : Type u} :
List () × α List () ×
Instances For
def Computation.parallel {α : Type u} (S : ) :

Parallel computation of an infinite stream of computations, taking the first result

Instances For
theorem Computation.terminates_parallel.aux {α : Type u} {l : List ()} {S : } {c : } :
c lComputation.Terminates (Computation.corec Computation.parallel.aux1 (l, S))
theorem Computation.terminates_parallel {α : Type u} {S : } {c : } (h : c S) [T : ] :
theorem Computation.exists_of_mem_parallel {α : Type u} {S : } {a : α} (h : ) :
c, c S a c
theorem Computation.map_parallel {α : Type u} {β : Type v} (f : αβ) (S : ) :
theorem Computation.parallel_empty {α : Type u} (S : ) (h : ) :
def Computation.parallelRec {α : Type u} {S : } (C : αSort v) (H : (s : ) → s S(a : α) → a sC a) {a : α} (h : ) :
C a
Instances For
theorem Computation.parallel_promises {α : Type u} {S : } {a : α} (H : ∀ (s : ), s S) :
theorem Computation.mem_parallel {α : Type u} {S : } {a : α} (H : ∀ (s : ), s S) {c : } (cs : c S) (ac : a c) :
theorem Computation.parallel_congr_lem {α : Type u} {S : } {T : } {a : α} (H : Stream'.WSeq.LiftRel Computation.Equiv S T) :
(∀ (s : ), s S) ∀ (t : ), t T
theorem Computation.parallel_congr_left {α : Type u} {S : } {T : } {a : α} (h1 : ∀ (s : ), s S) (H : Stream'.WSeq.LiftRel Computation.Equiv S T) :
theorem Computation.parallel_congr_right {α : Type u} {S : } {T : } {a : α} (h2 : ∀ (t : ), t T) (H : Stream'.WSeq.LiftRel Computation.Equiv S T) :