Step
*
of Lemma
data-stream_wf
∀[A,B:Type]. ∀[L:A List]. ∀[P:dataflow(A;B)]. (data-stream(P;L) ∈ B List)
BY
{ (InductionOnList THEN Auto THEN ProveWfLemma THEN Reduce 0 THEN Auto THEN Fold `data-stream` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[A,B:Type]. \mforall{}[L:A List]. \mforall{}[P:dataflow(A;B)]. (data-stream(P;L) \mmember{} B List)
By
Latex:
(InductionOnList
THEN Auto
THEN ProveWfLemma
THEN Reduce 0
THEN Auto
THEN Fold `data-stream` 0
THEN Auto)
Home
Index