Nuprl Lemma : pv8_p1_on_p1a_wf

[Cid,Op:ValueAllType]. [ldrs_uid:Id  ].
  (pv8_p1_on_p1a(Cid;Op;ldrs_uid)  Id
                                     Id  (  Id?)
                                       Id?  ((  Id?    Id  Cid  Op) List)
                                     (  Id?  ((  Id?    Id  Cid  Op) List)))


Proof not projected



Definitions occuring in Statement :  pv8_p1_on_p1a: pv8_p1_on_p1a(Cid;Op;ldrs_uid),  Id: Id,  uall: [x:A]. B[x],  unit: Unit,  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  union: left + right,  list: type List,  int: ,  vatype: ValueAllType
Definitions :  pv8_p1_on_p1a: pv8_p1_on_p1a(Cid;Op;ldrs_uid),  member: t  T,  vatype: ValueAllType,  uall: [x:A]. B[x]
Lemmas :  valueall-type_wf,  unit_wf2,  Id_wf,  pv8_p1_max_bnum_wf
\mforall{}[Cid,Op:ValueAllType].  \mforall{}[ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}].
    (pv8\_p1\_on\_p1a(Cid;Op;ldrs$_{uid}$)  \mmember{}  Id
                                                                      {}\mrightarrow{}  Id  \mtimes{}  (\mBbbZ{}  \mtimes{}  Id?)
                                                                      {}\mrightarrow{}  \mBbbZ{}  \mtimes{}  Id?  \mtimes{}  ((\mBbbZ{}  \mtimes{}  Id?  \mtimes{}  \mBbbZ{}  \mtimes{}  Id  \mtimes{}  Cid  \mtimes{}  Op)  List)
                                                                      {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  Id?  \mtimes{}  ((\mBbbZ{}  \mtimes{}  Id?  \mtimes{}  \mBbbZ{}  \mtimes{}  Id  \mtimes{}  Cid  \mtimes{}  Op)  List)))


Date html generated: 2012_02_20-PM-07_24_42
Last ObjectModification: 2012_02_06-PM-01_58_06

Home Index