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