Nuprl Lemma : bm_compare_less_less_false

[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K].  (compare k1 k2 <  compare k2 k1 <  False)


Proof




Definitions occuring in Statement :  bm_compare: bm_compare(K) less_than: a < b uall: [x:A]. B[x] implies:  Q false: False apply: a natural_number: $n universe: Type
Lemmas :  bm_compare_less_to_greater_eq less_than_transitivity1 less_than_irreflexivity less_than_wf bm_compare_wf
\mforall{}[K:Type].  \mforall{}[compare:bm\_compare(K)].  \mforall{}[k1,k2:K].    (compare  k1  k2  <  0  {}\mRightarrow{}  compare  k2  k1  <  0  {}\mRightarrow{}  False)



Date html generated: 2015_07_17-AM-08_19_35
Last ObjectModification: 2015_01_27-PM-00_36_45

Home Index