Nuprl Lemma : aa_data_wrapper_ind_wf
[X:
{j}]. [T:Type]. [x:aa_data_wrapper(T)]. [node:nd:aa_data_wrapper(T) 
rec1:X X]. [leaf:val:T X].
(aa_data_wrapper_ind(x;nd,rec1.node[nd;rec1];val.leaf[val]) 
X)
Proof
Definitions occuring in Statement :
aa_data_wrapper_ind: aa_data_wrapper_ind(x;nd,rec1.node[nd; rec1];val.leaf[val]),
aa_data_wrapper: aa_data_wrapper(T),
uall: [x:A]. B[x],
so_apply: x[s1;s2],
so_apply: x[s],
member: t T,
function: x:A B[x],
universe: Type
Definitions :
uall: [x:A]. B[x],
aa_data_wrapper: aa_data_wrapper(T),
member: t T,
aa_data_wrapper_ind: aa_data_wrapper_ind(x;nd,rec1.node[nd; rec1];val.leaf[val]),
so_apply: x[s1;s2],
so_apply: x[s],
type-monotone: Monotone(T.F[T]),
uimplies: b supposing a,
guard: {T}
Lemmas :
subtype_rel_sum,
subtype_rel_self,
aa_data_wrapper_wf
\mforall{}[X:\mBbbU{}\{j\}]. \mforall{}[T:Type]. \mforall{}[x:aa\_data\_wrapper(T)]. \mforall{}[node:nd:aa\_data\_wrapper(T) {}\mrightarrow{} rec1:X {}\mrightarrow{} X].
\mforall{}[leaf:val:T {}\mrightarrow{} X].
(aa\_data\_wrapper\_ind(x;nd,rec1.node[nd;rec1];val.leaf[val]) \mmember{} X)
Date html generated:
2013_03_20-AM-11_02_30
Last ObjectModification:
2012_11_27-AM-10_33_09
Home
Index