Nuprl Lemma : SM-gen-tr_wf
[S:Type]. [n:
]. [m:{1..n + 1
}]. [A:k:{m..n + 1} 
Type]. [btrs:k:{m..n + 1} (bag(A k) 
(Id
A k
S
S))].
[bp:bag(S)]. [l:Id].
(SM-gen-tr(l;btrs;bp;n;m) 
bag(S))
Proof not projected
Definitions occuring in Statement :
SM-gen-tr: SM-gen-tr(l;btrs;bp;n;m),
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 :
member: t T,
lelt: i 
j < k,
exists: 
x:A. B[x],
and: P 
Q,
prop: 
,
all: x:A. B[x],
implies: P 
Q,
le: A B,
not: 
A,
false: False,
ge: i 
j ,
int_seg: {i..j},
SM-gen-tr: SM-gen-tr(l;btrs;bp;n;m),
guard: {T},
ycomb: Y,
ifthenelse: if b then t else f fi ,
btrue: tt,
iff: P 
Q,
assert: 
b,
top: Top,
subtype: S 
T,
rev_implies: P Q,
or: P 
Q,
true: True,
so_lambda: 
x.t[x],
squash: 
T,
suptype: suptype(S; T),
bfalse: ff,
nat_plus: ,
uall: [x:A]. B[x],
nat: ,
sq_type: SQType(T),
uimplies: b supposing a,
so_apply: x[s],
bool: 
,
unit: Unit,
uiff: uiff(P;Q),
label: ...$L... t,
it: 
Lemmas :
int_seg_properties,
subtype_base_sq,
int_subtype_base,
int_seg_wf,
bag_wf,
Id_wf,
le_wf,
nat_plus_wf,
nat_properties,
ge_wf,
bool_wf,
bool_subtype_base,
iff_imp_equal_bool,
bor_wf,
bnot_wf,
bag-null_wf,
pi1_wf_top,
btrue_wf,
iff_functionality_wrt_iff,
assert_wf,
not_wf,
empty-bag_wf,
true_wf,
iff_weakening_uiff,
uiff_transitivity,
assert_of_bor,
or_functionality_wrt_uiff2,
decidable__assert,
assert_of_bnot,
not_functionality_wrt_uiff,
assert-bag-null,
lifting-loc-2_wf,
pi2_wf,
eq_int_eq_true,
nat_plus_properties,
member_wf,
squash_wf,
bor-btrue,
eq_int_wf,
bfalse_wf,
false_wf,
assert_of_eq_int,
bor-bfalse,
eqtt_to_assert,
eqff_to_assert
\mforall{}[S:Type]. \mforall{}[n:\mBbbN{}\msupplus{}]. \mforall{}[m:\{1..n + 1\msupminus{}\}]. \mforall{}[A:k:\{m..n + 1\msupminus{}\} {}\mrightarrow{} Type].
\mforall{}[btrs:k:\{m..n + 1\msupminus{}\} {}\mrightarrow{} (bag(A k) \mtimes{} (Id {}\mrightarrow{} A k {}\mrightarrow{} S {}\mrightarrow{} S))]. \mforall{}[bp:bag(S)]. \mforall{}[l:Id].
(SM-gen-tr(l;btrs;bp;n;m) \mmember{} bag(S))
Date html generated:
2011_10_20-PM-03_34_38
Last ObjectModification:
2011_08_17-AM-00_37_40
Home
Index