Nuprl Lemma : max_w_ord_wf

[T:Type]. ∀[t1,t2:T]. ∀[f:T ─→ ℤ].  (max_w_ord(t1;t2;f) ∈ T)


Proof




Definitions occuring in Statement :  max_w_ord: max_w_ord(t1;t2;f) uall: [x:A]. B[x] member: t ∈ T function: x:A ─→ B[x] int: universe: Type
Lemmas :  lt_int_wf bool_wf uiff_transitivity equal-wf-T-base assert_wf less_than_wf eqtt_to_assert assert_of_lt_int le_int_wf le_wf bnot_wf eqff_to_assert assert_functionality_wrt_uiff bnot_of_lt_int assert_of_le_int
\mforall{}[T:Type].  \mforall{}[t1,t2:T].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].    (max\_w\_ord(t1;t2;f)  \mmember{}  T)



Date html generated: 2015_07_17-AM-07_41_45
Last ObjectModification: 2015_01_27-AM-09_30_59

Home Index