Theorems · Theorem · logic and foundations
Computation.terminates_parallel
∀ {α : Type u} {S : Stream'.WSeq (Computation α)} {c : Computation α},
c ∈ S → ∀ [T : c.Terminates], (Computation.parallel S).Terminates- Defined in
- Mathlib.Data.Seq.Parallel
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Computation.Terminates
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Stream'.Seqproof · cited by 226
- Computationstatement and proof · cited by 182
- Stream'.WSeqstatement and proof · cited by 149
- Stream'.Seq.get?proof · cited by 122
- Stream'.getproof · cited by 86
- Stream'.Seq.nilproof · cited by 72
- Computation.pureproof · cited by 61
- Stream'.Seq1proof · cited by 58
- Computation.Terminatesstatement and proof · cited by 48
- Stream'.Seq.destructproof · cited by 47
- Computation.thinkproof · cited by 41
- Stream'.Seq.tailproof · cited by 34
Cited by1
Results whose statement or proof uses this declaration.
- Computation.mem_parallelproof · cited by 1