{ 
[L:Top List]. (null-dataflow()*(L) ~ null-dataflow()) }
{ Proof }
Definitions occuring in Statement :
null-dataflow: null-dataflow(),
iterate-dataflow: P*(inputs),
uall: [x:A]. B[x],
top: Top,
list: type List,
sqequal: s ~ t
Definitions :
tactic: Error :tactic,
CollapseTHEN: Error :CollapseTHEN,
Auto: Error :Auto,
sqequal: s ~ t,
list: type List,
top: Top,
null-dataflow: null-dataflow(),
iterate-dataflow: P*(inputs),
dataflow-ap: df(a),
pi1: fst(t),
iter_df_cons: iter_df_cons{iter_df_cons_compseq_tag_def:o}(as; a; P),
iter_df_nil: iter_df_nil{iter_df_nil_compseq_tag_def:o}(P),
equal: s = t,
member: t 
T,
function: x:A 
B[x],
all: x:A. B[x],
isect: 
x:A. B[x],
uall: [x:A]. B[x],
universe: Type,
prop: 
,
so_lambda: 
x.t[x],
subtype_rel: A 
r B,
uiff: uiff(P;Q),
and: P 
Q,
product: x:A 
B[x],
uimplies: b supposing a,
less_than: a < b,
not: 
A,
ge: i 
j ,
le: A 
B,
strong-subtype: strong-subtype(A;B),
rec_dataflow_ap: rec_dataflow_ap_compseq_tag_def
Lemmas :
top_wf,
uall_wf
\mforall{}[L:Top List]. (null-dataflow()*(L) \msim{} null-dataflow())
Date html generated:
2011_08_10-AM-08_18_02
Last ObjectModification:
2011_06_16-PM-03_33_28
Home
Index