Nuprl Lemma : filter-interface-predecessors-lower-bound
[Info:Type]. [es:EO+(Info)]. [T:Type]. [X:EClass(T)]. [P:E(X) 
]. [n:
]. [f:n {e:E(X)| 
P[e]} ].
[k:n]. n 
||filter(
e.P[e];(X)(f k))|| supposing i:n. f i loc f k supposing Inj(n;{e:E(X)| P[e]} ;f)
Proof not projected
Definitions occuring in Statement :
es-interface-predecessors: (X)(e),
es-E-interface: E(X),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-le: e loc e' ,
length: ||as||,
inject: Inj(A;B;f),
assert: b,
bool: ,
int_seg: {i..j
},
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
le: A B,
all: x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
natural_number: $n,
universe: Type,
filter: filter(P;l)
Definitions :
so_lambda: 
x y.t[x; y],
so_lambda: x.t[x],
prop: 
,
subtype: S 
T,
false: False,
not: 
A,
implies: P 
Q,
member: t 
T,
le: A B,
all: x:A. B[x],
uimplies: b supposing a,
so_apply: x[s],
uall: [x:A]. B[x],
and: P 
Q,
lelt: i j < k,
exists: 
x:A. B[x],
int_seg: {i..j},
pi1: fst(t),
nat: ,
true: True,
squash: 
T,
so_apply: x[s1;s2],
es-E-interface: E(X),
cand: A c B,
l_member: (x l),
inject: Inj(A;B;f),
guard: {T}
Lemmas :
event-ordering+_wf,
eclass_wf,
bool_wf,
nat_wf,
inject_wf,
int_seg_wf,
es-le_wf,
all_wf,
es-interface-predecessors_wf,
filter_type,
es-E_wf,
assert_wf,
event-ordering+_inc,
es-loc_wf,
Id_wf,
es-interface-top,
es-E-interface_wf,
length_wf,
equal_wf,
l_member_wf,
filter_wf3,
select_wf,
lelt_wf,
le_wf,
exists_wf,
length_wf_nat,
non_neg_length
\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[T:Type]. \mforall{}[X:EClass(T)]. \mforall{}[P:E(X) {}\mrightarrow{} \mBbbB{}]. \mforall{}[n:\mBbbN{}].
\mforall{}[f:\mBbbN{}n {}\mrightarrow{} \{e:E(X)| \muparrow{}P[e]\} ].
\mforall{}[k:\mBbbN{}n]. n \mleq{} ||filter(\mlambda{}e.P[e];\mleq{}(X)(f k))|| supposing \mforall{}i:\mBbbN{}n. f i \mleq{}loc f k
supposing Inj(\mBbbN{}n;\{e:E(X)| \muparrow{}P[e]\} ;f)
Date html generated:
2012_01_23-PM-12_27_15
Last ObjectModification:
2011_12_13-PM-02_22_06
Home
Index