Nuprl Lemma : SM-gen-class-du_wf
[Info,S:Type]. [n:
]. [m:n + 1]. [A:k:{m..n + 1
} 
Type].
[trXs:k:{m..n + 1} (Id A k S S 
EClass(A k))]. [init:Id bag(S)].
(SM-gen-class-du(init;n;m;trXs) 
Id disjoint-union-type(listify(A;m;n + 1)) S S
EClass(disjoint-union-type(listify(A;m;n + 1))))
Proof not projected
Definitions occuring in Statement :
SM-gen-class-du: SM-gen-class-du(init;n;m;trXs),
disjoint-union-type: disjoint-union-type(L),
eclass: EClass(A[eo; e]),
Id: Id,
listify: listify(f;m;n),
int_seg: {i..j},
nat: ,
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 :
member: t T,
exists: 
x:A. B[x],
prop: 
,
so_lambda: 
x y.t[x; y],
all: x:A. B[x],
implies: P 
Q,
le: A 
B,
not: 
A,
false: False,
ge: i 
j ,
int_seg: {i..j},
disjoint-union-type: disjoint-union-type(L),
listify: listify(f;m;n),
SM-gen-class-du: SM-gen-class-du(init;n;m;trXs),
ycomb: Y,
ifthenelse: if b then t else f fi ,
btrue: tt,
bfalse: ff,
iff: P 
Q,
assert: 
b,
rev_implies: P Q,
true: True,
and: P 
Q,
null: null(as),
lelt: i j < k,
subtype: S 
T,
suptype: suptype(S; T),
top: Top,
uiff: uiff(P;Q),
bnot: 
b,
so_lambda: x.t[x],
nat: ,
uall: [x:A]. B[x],
so_apply: x[s1;s2],
sq_type: SQType(T),
uimplies: b supposing a,
guard: {T},
bool: 
,
unit: Unit,
length: ||as||,
so_apply: x[s],
it: 
Lemmas :
int_seg_properties,
Id_wf,
bag_wf,
int_seg_wf,
eclass_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
nat_wf,
subtype_base_sq,
int_subtype_base,
le_wf,
nat_properties,
ge_wf,
bool_wf,
bool_subtype_base,
iff_imp_equal_bool,
le_int_wf,
bfalse_wf,
iff_functionality_wrt_iff,
assert_wf,
false_wf,
iff_weakening_uiff,
assert_of_le_int,
btrue_wf,
true_wf,
eq_int_eq_true,
eq_int_wf,
assert_of_eq_int,
pair-eta,
disjoint-union-type_wf,
listify_wf,
assert_of_null,
length_zero,
non_neg_length,
listify_length,
length_wf_nat,
null_wf3,
top_wf,
isl_wf,
eqtt_to_assert,
outl_wf,
uiff_transitivity,
bnot_wf,
not_wf,
eqff_to_assert,
assert_of_bnot,
pi1_wf_top,
outr_wf,
disjoint-union-class_wf,
pi2_wf,
not_assert_elim
\mforall{}[Info,S:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[m:\mBbbN{}n + 1]. \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-du(init;n;m;trXs) \mmember{} Id {}\mrightarrow{} disjoint-union-type(listify(A;m;n + 1)) {}\mrightarrow{} S {}\mrightarrow{} S
\mtimes{} EClass(disjoint-union-type(listify(A;m;n + 1))))
Date html generated:
2011_10_20-PM-03_40_29
Last ObjectModification:
2011_09_23-PM-06_57_32
Home
Index