Nuprl Lemma : aa_ltree_ind_wf
[X:
{j}]. [T:Type]. [x:aa_ltree(T)]. [leaf:X]. [node:val:T
left_subtree:aa_ltree(T)
right_subtree:aa_ltree(T)
rec1:X
rec2:X
X].
(aa_ltree_ind(x;leaf;val,left_subtree,right_subtree,rec1,rec2.node[val;left_subtree;right_subtree;rec1;rec2]) 
X)
Proof
Definitions occuring in Statement :
aa_ltree_ind: aa_ltree_ind(x;leaf;val,left_subtree,right_subtree,rec1,rec2.node[val; left_subtree; right_subtree; rec1; rec2]),
aa_ltree: aa_ltree(T),
uall: [x:A]. B[x],
so_apply: x[s1;s2;s3;s4;s5],
member: t T,
function: x:A B[x],
universe: Type
Definitions :
uall: [x:A]. B[x],
aa_ltree: aa_ltree(T),
member: t T,
aa_ltree_ind: aa_ltree_ind(x;leaf;val,left_subtree,right_subtree,rec1,rec2.node[val; left_subtree; right_subtree; rec1; rec2]),
so_apply: x[s1;s2;s3;s4;s5],
type-monotone: Monotone(T.F[T]),
uimplies: b supposing a,
pi1: fst(t),
pi2: snd(t)
Lemmas :
unit_wf2,
subtype_rel_sum,
subtype_rel_simple_product,
subtype_rel_self,
aa_ltree_wf
\mforall{}[X:\mBbbU{}\{j\}]. \mforall{}[T:Type]. \mforall{}[x:aa\_ltree(T)]. \mforall{}[leaf:X]. \mforall{}[node:val:T
{}\mrightarrow{} left$_{subtree}$:aa\000C\_ltree(T)
{}\mrightarrow{} right$_{subtree}$:a\000Ca\_ltree(T)
{}\mrightarrow{} rec1:X
{}\mrightarrow{} rec2:X
{}\mrightarrow{} X].
(aa\_ltree\_ind(x;leaf;val,left$_{subtree}$,right$_{subtree}\mbackslash{}ff2\000C4,rec1,rec2.node[val;left$_{subtree}$;...;rec1;rec2])
\mmember{} X)
Date html generated:
2013_03_20-AM-10_57_46
Last ObjectModification:
2012_11_27-AM-10_32_24
Home
Index