Nuprl Lemma : add-bottom_wf
[T:Type]. [ord:T 
T 
]. (add-bottom(ord) 
T? T? )
Proof not projected
Definitions occuring in Statement :
add-bottom: add-bottom(ord),
uall: [x:A]. B[x],
prop: ,
unit: Unit,
member: t T,
function: x:A B[x],
union: left + right,
universe: Type
Definitions :
true: True,
guard: {T},
implies: P 
Q,
btrue: tt,
subtype_rel: A 
r B,
sq_type: SQType(T),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
uimplies: b supposing a,
outl: outl(x),
apply: f a,
product: x:A 
B[x],
isl: isl(x),
assert: 
b,
all: x:A. B[x],
not: 
A,
cand: A c
B,
and: P Q,
or: P 
Q,
lambda: 
x.A[x],
bool: 
,
union: left + right,
unit: Unit,
add-bottom: add-bottom(ord),
axiom: Ax,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
function: x:A B[x],
prop: ,
universe: Type,
equal: s = t,
member: t T
Lemmas :
not_wf,
outl_wf,
assert_wf,
subtype_base_sq,
bool_subtype_base,
bool_wf,
assert_elim,
isl_wf,
unit_wf
\mforall{}[T:Type]. \mforall{}[ord:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}]. (add-bottom(ord) \mmember{} T? {}\mrightarrow{} T? {}\mrightarrow{} \mBbbP{})
Date html generated:
2011_10_20-PM-04_51_19
Last ObjectModification:
2011_05_19-AM-11_17_28
Home
Index