Nuprl Lemma : test36

z,loc,L.if (lL.IdDeq l loc)_b then {L} else {[loc / L]} fi   A:Type. (A  Id  Id List  bag(Id List))


Proof not projected



Definitions occuring in Statement :  id-deq: IdDeq,  Id: Id,  ifthenelse: if b then t else f fi ,  member: t  T,  apply: f a,  lambda: x.A[x],  isect: x:A. B[x],  function: x:A  B[x],  cons: [car / cdr],  list: type List,  universe: Type,  single-bag: {x},  bag: bag(T),  bl-exists: (xL.P[x])_b
Definitions :  so_lambda: x.t[x],  so_apply: x[s],  uall: [x:A]. B[x],  member: t  T,  all: x:A. B[x],  prop: ,  deq: EqDecider(T)
Lemmas :  cons_wf,  single-bag_wf,  id-deq_wf,  bl-exists_wf,  ifthenelse_wf,  bag_wf,  l_member_wf,  deq_wf,  bool_wf,  Id_wf
\mlambda{}z,loc,L.if  (\mexists{}l\mmember{}L.IdDeq  l  loc)\_b  then  \{L\}  else  \{[loc  /  L]\}  fi    \mmember{}  \mcap{}A:Type
                                                                                                                                      (A
                                                                                                                                      {}\mrightarrow{}  Id
                                                                                                                                      {}\mrightarrow{}  Id  List
                                                                                                                                      {}\mrightarrow{}  bag(Id  List))


Date html generated: 2012_01_23-AM-11_51_38
Last ObjectModification: 2011_12_09-PM-07_13_23

Home Index