Nuprl Lemma : rec-comb-es-sv

[Info,B:Type].

[n:

].

[A:

n

Type].

[Xs:k:

n

EClass(A k)].

[F:Id

k:

n

bag(A k)

bag(B)

bag(B)].

[init:Id

bag(B)].

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

bs:k:

n

bag(A k).

l:Id.

b:bag(B).
((

k:

n. (bag-size(bs k)

1))

(bag-size(b)

1)

(bag-size(F l bs b)

1))) and
(

k:

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

l:Id. (bag-size(init l)

1)))

Proof not projected

Definitions occuring in Statement : rec-comb: rec-comb(X;f;init), es-sv-class: es-sv-class(es;X), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), Id: Id, 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], ycomb: Y, true: True, squash:

T, prop:

, false: False, not:

A, ge: i

j , member: t

T, rec-comb: rec-comb(X;f;init), implies: P

Q, es-sv-class: es-sv-class(es;X), le: A

B, all:

x:A. B[x], nat:

, and: P

Q, es-locl: (e <loc e'), so_apply: x[s1;s2], so_apply: x[s], exists:

x:A. B[x], uall:

[x:A]. B[x], strongwellfounded: SWellFounded(R[x; y]), subtype: S

T, eclass: EClass(A[eo; e]), guard: {T}
Lemmas : eclass_wf, event-ordering+_wf, es-sv-class_wf, Id_wf, bag_wf, all_wf, bag-size_wf, equal_wf, es-E_wf, es-locl_wf, primed-class-opt-es-sv0, rec-comb_wf2, primed-class-opt_wf, es-loc_wf, int_seg_wf, es-causl_wf, le_wf, nat_wf, less_than_wf, ge_wf, nat_properties, event-ordering+_inc, es-causl-swellfnd

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