Nuprl Lemma : aa_lt_node-right_subtree_wf
[T:Type]. [x:aa_ltree(T)]. aa_lt_node-right_subtree(x) 
aa_ltree(T) supposing 
aa_lt_node?(x)
Proof
Definitions occuring in Statement :
aa_lt_node-right_subtree: aa_lt_node-right_subtree(x),
aa_lt_node?: aa_lt_node?(x),
aa_ltree: aa_ltree(T),
assert: b,
uimplies: b supposing a,
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
uall: [x:A]. B[x],
aa_ltree: aa_ltree(T),
uimplies: b supposing a,
assert: b,
aa_lt_node?: aa_lt_node?(x),
member: t T,
aa_lt_node-right_subtree: aa_lt_node-right_subtree(x),
implies: P 
Q,
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
unit: Unit,
false: False,
it: 
,
aa_lt_leaf: aa_lt_leaf(),
prop: 
,
aa_lt_node: aa_lt_node(val;left_subtree;right_subtree)
Lemmas :
false_wf,
true_wf,
assert_wf,
aa_lt_node?_wf,
aa_ltree_wf,
subtype_rel_self
\mforall{}[T:Type]. \mforall{}[x:aa\_ltree(T)]. aa\_lt\_node-right\_subtree(x) \mmember{} aa\_ltree(T) supposing \muparrow{}aa\_lt\_node?(x)
Date html generated:
2013_03_20-AM-10_58_18
Last ObjectModification:
2012_11_27-AM-10_32_42
Home
Index