Nuprl Lemma : SM-gen-class-locally-programmable

[Info:{Info:Type|

Info} ]

S:{S:Type| valueall-type(S)} .

n:

.

[A:k:

n + 1

Type]

trXs:k:

n + 1

(Id

A k

S

EClass(A k)).

init:Id

bag(S).
((

k:

n + 1. NormalLProgrammable(A k;snd((trXs k))))

NormalLProgrammable(S;SM-gen-class(init;n;1;trXs)))

Proof not projected

Definitions occuring in Statement : SM-gen-class: SM-gen-class(init;n;m;trXs), normal-locally-programmable: NormalLProgrammable(A;X), eclass: EClass(A[eo; e]), Id: Id, int_seg: {i..j

}, nat_plus:

, uall:

[x:A]. B[x], pi2: snd(t), all:

x:A. B[x], squash:

T, implies: P

Q, set: {x:A| B[x]} , apply: f a, function: x:A

B[x], product: x:A

B[x], add: n + m, natural_number: $n, universe: Type, bag: bag(T), valueall-type: valueall-type(T)
Definitions : uall:

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

x:A. B[x], int_seg: {i..j

}, implies: P

Q, SM-gen-class: SM-gen-class(init;n;m;trXs), nat:

, member: t

T, le: A

B, not:

A, false: False, prop:

, so_lambda:

x.t[x], so_lambda:

x y.t[x; y], subtype: S

T, lelt: i

j < k, and: P

Q, suptype: suptype(S; T), top: Top, squash:

T, or: P

Q, true: True, lifting-loc-2: lifting-loc-2(f), rev_implies: P

Q, iff: P

Q, lifting2-loc: lifting2-loc(f;loc;abag;bbag), lifting-loc-gen-rev: lifting-loc-gen-rev(n;bags;loc;f), select: l[i], lifting-gen-rev: lifting-gen-rev(n;f;bags), lifting-gen-list-rev: lifting-gen-list-rev(n;bags), ycomb: Y, ifthenelse: if b then t else f fi , eq_int: (i =

j), btrue: tt, bfalse: ff, le_int: i

z j, bnot:

b, lt_int: i <z j, nat_plus:

, so_apply: x[s], so_apply: x[s1;s2], pi2: snd(t), exists:

x:A. B[x], pi1: fst(t), guard: {T}
Lemmas : rec-comb-locally-programmable1, le_wf, pi2_wf, eclass_wf, es-E_wf, event-ordering+_inc, event-ordering+_wf, SM-gen-tr_wf, lelt_wf, int_seg_wf, pi1_wf_top, bag_wf, all_wf, normal-locally-programmable_wf, Id_wf, nat_plus_wf, valueall-type_wf, squash_wf, SM-gen-tr-exists2, empty-bag_wf, exists_wf, equal_wf

\mforall{}[Info:\{Info:Type| \mdownarrow{}Info\} ] \mforall{}S:\{S:Type| valueall-type(S)\} . \mforall{}n:\mBbbN{}\msupplus{}. \mforall{}[A:k:\mBbbN{}n + 1 {}\mrightarrow{} Type] \mforall{}trXs:k:\mBbbN{}n + 1 {}\mrightarrow{} (Id {}\mrightarrow{} A k {}\mrightarrow{} S {}\mrightarrow{} S \mtimes{} EClass(A k)). \mforall{}init:Id {}\mrightarrow{} bag(S). ((\mforall{}k:\mBbbN{}n + 1. NormalLProgrammable(A k;snd((trXs k)))) {}\mRightarrow{} NormalLProgrammable(S;SM-gen-class(init;n;1;trXs))) Date html generated: 2012_01_23-PM-01_23_23 Last ObjectModification: 2011_12_30-PM-09_21_02 Home Index