Nuprl Lemma : SM-gen-class

Nuprl Lemma : SM-gen-class_wf

[Info,S:Type].

[n:

].

[m:{1..n + 1

}].

[A:k:{m..n + 1

}

Type].

[trXs:k:{m..n + 1

}

(Id

A k

S

EClass(A k))].

[init:Id

bag(S)].
(SM-gen-class(init;n;m;trXs)

EClass(S))

Proof not projected

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

}, nat_plus:

, uall:

[x:A]. B[x], member: t

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

B[x], product: x:A

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

[x:A]. B[x], member: t

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

, le: A

B, not:

A, implies: P

Q, false: False, so_lambda:

x.t[x], so_lambda:

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

x:A. B[x], subtype: S

T, top: Top, nat_plus:

, int_seg: {i..j

}, lelt: i

j < k, and: P

Q, prop:

, so_apply: x[s], so_apply: x[s1;s2]
Lemmas : rec-comb_wf2, le_wf, pi2_wf, Id_wf, eclass_wf, es-E_wf, event-ordering+_inc, event-ordering+_wf, int_seg_wf, SM-gen-tr_wf, pi1_wf_top, bag_wf, nat_plus_wf

\mforall{}[Info,S:Type]. \mforall{}[n:\mBbbN{}\msupplus{}]. \mforall{}[m:\{1..n + 1\msupminus{}\}]. \mforall{}[A:k:\{m..n + 1\msupminus{}\} {}\mrightarrow{} Type]. \mforall{}[trXs:k:\{m..n + 1\msupminus{}\} {}\mrightarrow{} (Id {}\mrightarrow{} A k {}\mrightarrow{} S {}\mrightarrow{} S \mtimes{} EClass(A k))]. \mforall{}[init:Id {}\mrightarrow{} bag(S)]. (SM-gen-class(init;n;m;trXs) \mmember{} EClass(S)) Date html generated: 2012_01_23-PM-01_06_46 Last ObjectModification: 2011_12_30-PM-08_24_24 Home Index