Nuprl Lemma : pv8_p1_add_if_new_wf
pv8_p1_add_if_new() 
A:
'. (A 
A 
A A List (A List))
Proof not projected
Definitions occuring in Statement :
pv8_p1_add_if_new: pv8_p1_add_if_new(),
bool: ,
member: t T,
isect: x:A. B[x],
function: x:A B[x],
list: type List,
universe: Type
Definitions :
so_lambda: 
x.t[x],
pv8_p1_add_if_new: pv8_p1_add_if_new(),
member: t T,
prop: 
,
so_apply: x[s],
uall: 
[x:A]. B[x]
Lemmas :
bool_wf,
append_wf,
l_member_wf,
bl-exists_wf,
ifthenelse_wf
pv8\_p1\_add\_if\_new() \mmember{} \mcap{}A:\mBbbU{}'. (A {}\mrightarrow{} A {}\mrightarrow{} \mBbbB{} {}\mrightarrow{} A {}\mrightarrow{} A List {}\mrightarrow{} (A List))
Date html generated:
2012_02_20-PM-07_16_10
Last ObjectModification:
2012_02_06-PM-02_03_10
Home
Index