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