Nuprl Lemma : test36
λz,loc,L. if (∃l∈L.IdDeq l loc)_b then {L} else {[loc / L]} fi ∈ ∩A:Type. (A ─→ Id ─→ (Id List) ─→ bag(Id List))
Proof
Definitions occuring in Statement :
id-deq: IdDeq,
Id: Id,
bl-exists: (∃x∈L.P[x])_b,
cons: [a / b],
list: T List,
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],
universe: Type,
single-bag: {x},
bag: bag(T)
Lemmas :
Id_wf,
bool_wf,
deq_wf,
l_member_wf,
bag_wf,
list_wf,
ifthenelse_wf,
bl-exists_wf,
id-deq_wf,
single-bag_wf,
cons_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:
2015_07_17-AM-07_53_04
Last ObjectModification:
2015_01_27-AM-09_21_48
Home
Index