Nuprl Lemma : SM-gen-tr-exists2
[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].
p:{m..n + 1}
((SM-gen-tr(l;btrs;bp;n;m) = (lifting-loc-2(snd((btrs p))) l (fst((btrs p))) bp))
(i:{m..p}. (
bag-null(fst((btrs i))))))
Proof not projected
Definitions occuring in Statement :
SM-gen-tr: SM-gen-tr(l;btrs;bp;n;m),
lifting-loc-2: lifting-loc-2(f),
Id: Id,
assert: b,
int_seg: {i..j},
nat_plus: ,
uall: [x:A]. B[x],
pi1: fst(t),
pi2: snd(t),
all: x:A. B[x],
exists: x:A. B[x],
and: P Q,
apply: f a,
function: x:A B[x],
product: x:A B[x],
add: n + m,
natural_number: $n,
universe: Type,
equal: s = t,
bag-null: bag-null(bs),
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
exists: x:A. B[x],
member: t 
T,
prop: 
,
implies: P 
Q,
ge: i 
j ,
le: A 
B,
not: 
A,
false: False,
lelt: i j < k,
int_seg: {i..j},
and: P Q,
SM-gen-tr: SM-gen-tr(l;btrs;bp;n;m),
ycomb: Y,
ifthenelse: if b then t else f fi ,
btrue: tt,
top: Top,
subtype: S 
T,
so_lambda: 
x.t[x],
suptype: suptype(S; T),
or: P 
Q,
gt: i > j,
uiff: uiff(P;Q),
bfalse: ff,
nat_plus: ,
nat: ,
sq_type: SQType(T),
uimplies: b supposing a,
guard: {T},
so_apply: x[s],
bool: 
,
unit: Unit,
it: 
Lemmas :
nat_plus_properties,
int_seg_properties,
subtype_base_sq,
int_subtype_base,
int_seg_wf,
nat_plus_wf,
nat_properties,
ge_wf,
bool_wf,
bool_subtype_base,
bor-btrue,
bnot_wf,
bag-null_wf,
le_wf,
pi1_wf_top,
bag_wf,
lifting-loc-2_wf,
pi2_wf,
assert_witness,
assert_wf,
Id_wf,
eq_int_eq_true,
bor_wf,
eq_int_wf,
not_wf,
empty-bag_wf,
decidable__assert,
decidable_wf,
band_wf,
not_functionality_wrt_uiff,
assert-bag-null,
not-not-assert,
uiff_transitivity,
eqtt_to_assert,
assert_of_bor,
or_functionality_wrt_uiff,
assert_of_bnot,
assert_of_eq_int,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_thru_bor,
assert_of_band,
and_functionality_wrt_uiff
\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].
\mexists{}p:\{m..n + 1\msupminus{}\}
((SM-gen-tr(l;btrs;bp;n;m) = (lifting-loc-2(snd((btrs p))) l (fst((btrs p))) bp))
\mwedge{} (\mforall{}i:\{m..p\msupminus{}\}. (\muparrow{}bag-null(fst((btrs i))))))
Date html generated:
2011_10_20-PM-03_35_03
Last ObjectModification:
2011_08_17-PM-02_52_57
Home
Index