Nuprl Lemma : reduce-bool-bfalse
T:Type. f:T 
. L:T List. (reduce(
x,b.(b 
f[x;b]);ff;L) ~ ff)
Proof not projected
Definitions occuring in Statement :
reduce: reduce(f;k;as),
band: p q,
bfalse: ff,
bool: ,
so_apply: x[s1;s2],
all: x:A. B[x],
lambda: x.A[x],
function: x:A B[x],
list: type List,
universe: Type,
sqequal: s ~ t
Definitions :
all: x:A. B[x],
reduce: reduce(f;k;as),
band: p q,
bfalse: ff,
member: t 
T,
ifthenelse: if b then t else f fi ,
sq_type: SQType(T),
uall: [x:A]. B[x],
uimplies: b supposing a,
implies: P 
Q,
guard: {T}
Lemmas :
subtype_base_sq,
bool_wf,
bool_subtype_base,
bfalse_wf
\mforall{}T:Type. \mforall{}f:T {}\mrightarrow{} \mBbbB{} {}\mrightarrow{} \mBbbB{}. \mforall{}L:T List. (reduce(\mlambda{}x,b.(b \mwedge{}\msubb{} f[x;b]);ff;L) \msim{} ff)
Date html generated:
2012_01_23-PM-12_08_33
Last ObjectModification:
2011_11_29-PM-03_15_26
Home
Index