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