Nuprl Lemma : pv8_p1_on_p2b_wf
pv8_p1_on_p2b() 
Id? 
Id ( Id?) bag(Id) bag(Id)
Proof not projected
Definitions occuring in Statement :
pv8_p1_on_p2b: pv8_p1_on_p2b(),
Id: Id,
unit: Unit,
member: t T,
function: x:A B[x],
product: x:A B[x],
union: left + right,
int: ,
bag: bag(T)
Definitions :
pv8_p1_on_p2b: pv8_p1_on_p2b(),
member: t T,
uall: 
[x:A]. B[x]
Lemmas :
bag-remove_wf,
bag_wf,
unit-deq_wf,
id-deq_wf,
int-deq_wf,
product-deq_wf,
union-deq_wf,
unit_wf2,
Id_wf,
eqof_wf,
ifthenelse_wf
pv8\_p1\_on\_p2b() \mmember{} \mBbbZ{} \mtimes{} Id? {}\mrightarrow{} Id \mtimes{} (\mBbbZ{} \mtimes{} Id?) {}\mrightarrow{} bag(Id) {}\mrightarrow{} bag(Id)
Date html generated:
2012_02_20-PM-07_27_01
Last ObjectModification:
2012_02_06-PM-01_56_38
Home
Index