Nuprl Lemma : aa_data_wrapnode-nd_wf
[T:Type]. [x:aa_data_wrapper(T)]. aa_data_wrapnode-nd(x) 
aa_data_wrapper(T) supposing 
aa_data_wrapnode?(x)
Proof
Definitions occuring in Statement :
aa_data_wrapnode-nd: aa_data_wrapnode-nd(x),
aa_data_wrapnode?: aa_data_wrapnode?(x),
aa_data_wrapper: aa_data_wrapper(T),
assert: b,
uimplies: b supposing a,
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
uall: [x:A]. B[x],
aa_data_wrapper: aa_data_wrapper(T),
uimplies: b supposing a,
assert: b,
aa_data_wrapnode?: aa_data_wrapnode?(x),
member: t T,
aa_data_wrapnode-nd: aa_data_wrapnode-nd(x),
implies: P 
Q,
btrue: tt,
bfalse: ff,
ifthenelse: if b then t else f fi ,
false: False,
aa_data_wrapnode: aa_data_wrapnode(nd),
prop: 
,
aa_data_wrapleaf: aa_data_wrapleaf(val),
guard: {T}
Lemmas :
true_wf,
false_wf,
assert_wf,
aa_data_wrapnode?_wf,
aa_data_wrapper_wf,
subtype_rel_self
\mforall{}[T:Type]. \mforall{}[x:aa\_data\_wrapper(T)].
aa\_data\_wrapnode-nd(x) \mmember{} aa\_data\_wrapper(T) supposing \muparrow{}aa\_data\_wrapnode?(x)
Date html generated:
2013_03_20-AM-11_02_44
Last ObjectModification:
2012_11_27-AM-10_33_22
Home
Index