Nuprl Lemma : aa_min_ltree_wf
[t:aa_ltree(
)]. (aa_min_ltree(t) 
?)
Proof
Definitions occuring in Statement :
aa_min_ltree: aa_min_ltree(t),
aa_ltree: aa_ltree(T),
uall: [x:A]. B[x],
unit: Unit,
member: t T,
union: left + right,
int:
Definitions :
so_lambda: so_lambda(x,y,z,w,v.t[x; y; z; w; v]),
aa_min_ltree: aa_min_ltree(t),
member: t T,
uall: [x:A]. B[x],
all: x:A. B[x],
so_apply: x[s1;s2;s3;s4;s5],
guard: {T}
Lemmas :
subtype_rel_self,
aa_ltree_wf,
aa_min_w_unit_wf,
it_wf,
unit_wf2,
aa_ltree_ind_wf
\mforall{}[t:aa\_ltree(\mBbbZ{})]. (aa\_min\_ltree(t) \mmember{} \mBbbZ{}?)
Date html generated:
2013_03_20-AM-09_52_29
Last ObjectModification:
2012_11_27-AM-10_32_45
Home
Index