Nuprl Lemma : simple-comb-es-sv

[Info,B:Type].

[n:

].

[A:

n

Type].

[Xs:k:

n

EClass(A k)].

[F:k:

n

bag(A k)

bag(B)].

[es:EO+(Info)].
(es-sv-class(es;simple-comb(F;Xs))) supposing
((

bs:k:

n

bag(A k). ((

k:

n. (bag-size(bs k)

1))

(bag-size(F bs)

1))) and
(

k:

n. es-sv-class(es;Xs k)))

Proof not projected

Definitions occuring in Statement : simple-comb: simple-comb(F;Xs), es-sv-class: es-sv-class(es;X), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), int_seg: {i..j

}, nat:

, uimplies: b supposing a, uall:

[x:A]. B[x], le: A

B, all:

x:A. B[x], implies: P

Q, apply: f a, function: x:A

B[x], natural_number: $n, universe: Type, bag-size: bag-size(bs), bag: bag(T)
Definitions : so_lambda:

x y.t[x; y], so_lambda:

x.t[x], prop:

, member: t

T, simple-comb: simple-comb(F;Xs), implies: P

Q, es-sv-class: es-sv-class(es;X), all:

x:A. B[x], so_apply: x[s1;s2], so_apply: x[s], uall:

[x:A]. B[x], nat:

, subtype: S

T, eclass: EClass(A[eo; e]), guard: {T}
Lemmas : eclass_wf, event-ordering+_wf, es-sv-class_wf, le_wf, bag_wf, all_wf, nat_wf, bag-size_wf, event-ordering+_inc, es-E_wf, int_seg_wf

\mforall{}[Info,B:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[A:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[Xs:k:\mBbbN{}n {}\mrightarrow{} EClass(A k)]. \mforall{}[F:k:\mBbbN{}n {}\mrightarrow{} bag(A k) {}\mrightarrow{} bag(B)]. \mforall{}[es:EO+(Info)]. (es-sv-class(es;simple-comb(F;Xs))) supposing ((\mforall{}bs:k:\mBbbN{}n {}\mrightarrow{} bag(A k). ((\mforall{}k:\mBbbN{}n. (bag-size(bs k) \mleq{} 1)) {}\mRightarrow{} (bag-size(F bs) \mleq{} 1))) and (\mforall{}k:\mBbbN{}n. es-sv-class(es;Xs k))) Date html generated: 2012_02_20-PM-02_56_10 Last ObjectModification: 2012_02_07-PM-01_46_30 Home Index