Nuprl Lemma : rec-dataflow-state_wf
∀[S,A,B:Type]. ∀[s0:S]. ∀[next:S ─→ A ─→ (S × B)]. ∀[L:A List]. (rec-dataflow-state(s0;s,m.next[s;m];L) ∈ S)
Proof
Definitions occuring in Statement :
rec-dataflow-state: rec-dataflow-state(s0;s,m.next[s; m];L),
list: T List,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2],
member: t ∈ T,
function: x:A ─→ B[x],
product: x:A × B[x],
universe: Type
Lemmas :
list_accum_wf,
list_wf
Latex:
\mforall{}[S,A,B:Type]. \mforall{}[s0:S]. \mforall{}[next:S {}\mrightarrow{} A {}\mrightarrow{} (S \mtimes{} B)]. \mforall{}[L:A List].
(rec-dataflow-state(s0;s,m.next[s;m];L) \mmember{} S)
Date html generated:
2015_07_23-AM-11_05_30
Last ObjectModification:
2015_01_28-PM-11_34_40
Home
Index