Nuprl Lemma : aa_lt_node_wf
[T:Type]. [val:T]. [left_subtree,right_subtree:aa_ltree(T)].
(aa_lt_node(val;left_subtree;right_subtree) 
aa_ltree(T))
Proof
Definitions occuring in Statement :
aa_lt_node: aa_lt_node(val;left_subtree;right_subtree),
aa_ltree: aa_ltree(T),
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
uall: [x:A]. B[x],
aa_ltree: aa_ltree(T),
member: t T,
aa_lt_node: aa_lt_node(val;left_subtree;right_subtree),
type-monotone: Monotone(T.F[T]),
uimplies: b supposing a
Lemmas :
unit_wf2,
subtype_rel_sum,
subtype_rel_simple_product,
subtype_rel_self
\mforall{}[T:Type]. \mforall{}[val:T]. \mforall{}[left$_{subtree}$,right$_{subtree}$:aa\000C\_ltree(T)].
(aa\_lt\_node(val;left$_{subtree}$;right$_{subtree}$) \mmember{} aa\_l\000Ctree(T))
Date html generated:
2013_03_20-AM-10_57_41
Last ObjectModification:
2012_11_27-AM-10_32_21
Home
Index