Nuprl Lemma : aa_ltree-induction
[T:Type]. [P:aa_ltree(T) 
].
(P[aa_lt_leaf()]
(val:T. left_subtree,right_subtree:aa_ltree(T).
(P[left_subtree] P[right_subtree] P[aa_lt_node(val;left_subtree;right_subtree)]))
{x:aa_ltree(T). P[x]})
Proof
Definitions occuring in Statement :
aa_lt_node: aa_lt_node(val;left_subtree;right_subtree),
aa_lt_leaf: aa_lt_leaf(),
aa_ltree: aa_ltree(T),
uall: [x:A]. B[x],
prop: ,
guard: {T},
so_apply: x[s],
all: x:A. B[x],
implies: P Q,
function: x:A B[x],
universe: Type
Definitions :
uall: [x:A]. B[x],
prop: ,
implies: P Q,
so_apply: x[s],
all: x:A. B[x],
guard: {T},
member: t 
T,
type-monotone: Monotone(T.F[T]),
uimplies: b supposing a,
so_lambda: 
x.t[x],
aa_ltree: aa_ltree(T),
aa_lt_leaf: aa_lt_leaf(),
aa_lt_node: aa_lt_node(val;left_subtree;right_subtree),
unit: Unit,
it: 
Lemmas :
unit_wf2,
subtype_rel_sum,
subtype_rel_simple_product,
aa_ltree_wf,
all_wf,
aa_lt_node_wf,
aa_lt_leaf_wf
\mforall{}[T:Type]. \mforall{}[P:aa\_ltree(T) {}\mrightarrow{} \mBbbP{}].
(P[aa\_lt\_leaf()]
{}\mRightarrow{} (\mforall{}val:T. \mforall{}left$_{subtree}$,right$_{subtree}$:aa\_ltree(T\000C).
(P[left$_{subtree}$] {}\mRightarrow{} P[right$_{subtree}$] {}\mRightarrow{} P[aa\000C\_lt\_node(val;left$_{subtree}$;right$_{subtree}$)]))
{}\mRightarrow{} \{\mforall{}x:aa\_ltree(T). P[x]\})
Date html generated:
2013_03_20-AM-10_57_50
Last ObjectModification:
2012_11_27-AM-10_32_24
Home
Index