Nuprl Lemma : max_l_tree_wf
∀[L,T:Type]. ∀t:l_tree(L;T). ∀f:T ─→ ℤ. (max_l_tree(t;f) ∈ T?)
Proof
Definitions occuring in Statement :
max_l_tree: max_l_tree(t;f),
l_tree: l_tree(L;T),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
unit: Unit,
member: t ∈ T,
function: x:A ─→ B[x],
union: left + right,
int: ℤ,
universe: Type
Lemmas :
l_tree_ind_wf_simple,
top_wf,
unit_wf2,
l_tree_covariant,
it_wf,
max_w_unit_l_tree_wf,
l_tree_wf
\mforall{}[L,T:Type]. \mforall{}t:l\_tree(L;T). \mforall{}f:T {}\mrightarrow{} \mBbbZ{}. (max\_l\_tree(t;f) \mmember{} T?)
Date html generated:
2015_07_17-AM-07_41_47
Last ObjectModification:
2015_01_27-AM-09_30_58
Home
Index