Nuprl Lemma : iterate-constant-dataflow
∀[L:Top List]. ∀[b:Top].  (constant-dataflow(b)*(L) ~ constant-dataflow(b))
Proof
Definitions occuring in Statement : 
iterate-dataflow: P*(inputs)
, 
constant-dataflow: constant-dataflow(b)
, 
list: T List
, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
sqequal: s ~ t
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
constant-dataflow: constant-dataflow(b)
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
Latex:
\mforall{}[L:Top  List].  \mforall{}[b:Top].    (constant-dataflow(b)*(L)  \msim{}  constant-dataflow(b))
Date html generated:
2016_05_17-AM-10_21_43
Last ObjectModification:
2015_12_29-PM-05_28_47
Theory : process-model
Home
Index