Nuprl Lemma : mem_test_mem_max

es:EO'. e1,e2:E. n1,n2,n:.
  ((e1 <loc e2)
   n  mem_test_int'base()(e1)
   n1  mem_test_Maximum()(e1)
   n2  mem_test_Maximum()(e2)
   ((n1  n2)  (n  n2)))


Proof not projected

Error : references
\mforall{}es:EO'.  \mforall{}e1,e2:E.  \mforall{}n1,n2,n:\mBbbZ{}.
    ((e1  <loc  e2)
    {}\mRightarrow{}  n  \mmember{}  mem\_test\_int'base()(e1)
    {}\mRightarrow{}  n1  \mmember{}  mem\_test\_Maximum()(e1)
    {}\mRightarrow{}  n2  \mmember{}  mem\_test\_Maximum()(e2)
    {}\mRightarrow{}  ((n1  \mleq{}  n2)  \mwedge{}  (n  \mleq{}  n2)))


Date html generated: 2012_02_20-PM-07_51_04
Last ObjectModification: 2012_02_17-PM-06_28_23

Home Index