Nuprl Lemma : mData-examples

(<, 33>  mData)  (<, tt>  mData)  (<  , x.(x + 1)>  mData)  (<  , 33, ff>  mData)


Proof not projected



Definitions occuring in Statement :  mData: mData,  bfalse: ff,  btrue: tt,  bool: ,  and: P  Q,  member: t  T,  lambda: x.A[x],  function: x:A  B[x],  pair: <a, b>,  product: x:A  B[x],  add: n + m,  natural_number: $n,  int:
Definitions :  all: x:A. B[x],  so_lambda: x.t[x],  unit: Unit,  bool: ,  mData: mData,  member: t  T,  and: P  Q,  true: True,  squash: T,  so_apply: x[s],  uimplies: b supposing a,  implies: P  Q,  uall: [x:A]. B[x]
Lemmas :  bfalse_wf,  product-valueall-type,  function-valueall-type,  btrue_wf,  equal-valueall-type,  unit_wf2,  union-valueall-type,  bool_wf,  valueall-type_wf,  int-valueall-type
(<\mBbbZ{},  33>  \mmember{}  mData)  \mwedge{}  (<\mBbbB{},  tt>  \mmember{}  mData)  \mwedge{}  (<\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{},  \mlambda{}x.(x  +  1)>  \mmember{}  mData)  \mwedge{}  (<\mBbbZ{}  \mtimes{}  \mBbbB{},  33,  ff>  \mmember{}  mData)


Date html generated: 2012_01_23-PM-12_46_07
Last ObjectModification: 2011_12_05-PM-04_31_59

Home Index