Nuprl Lemma : SM-gen-tr-if
[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}].
((i:{m..p}. (
bag-null(fst((btrs i)))))
(((
bag-null(fst((btrs p)))) 
(n =
p)))
(SM-gen-tr(l;btrs;bp;n;m) = (lifting-loc-2(snd((btrs p))) l (fst((btrs p))) bp)))
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,
eq_int: (i = j),
bor: p q,
bnot: b,
assert: b,
int_seg: {i..j},
nat_plus: ,
uall: [x:A]. B[x],
pi1: fst(t),
pi2: snd(t),
all: x:A. B[x],
implies: 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 :
int_seg: {i..j},
all: x:A. B[x],
lelt: i 
j < k,
member: t 
T,
exists: 
x:A. B[x],
and: P 
Q,
prop: 
,
top: Top,
subtype: S 
T,
implies: P Q,
ge: i 
j ,
le: A B,
not: A,
false: False,
bnot: b,
SM-gen-tr: SM-gen-tr(l;btrs;bp;n;m),
ycomb: Y,
ifthenelse: if b then t else f fi ,
btrue: tt,
or: P Q,
so_lambda: 
x.t[x],
uiff: uiff(P;Q),
bfalse: ff,
assert: b,
bag-null: bag-null(bs),
bor: p q,
suptype: suptype(S; T),
rev_implies: P 
Q,
iff: P Q,
empty-bag: {},
true: True,
null: null(as),
gt: i > j,
squash: 
T,
nat_plus: ,
uall: [x:A]. B[x],
nat: ,
sq_type: SQType(T),
uimplies: b supposing a,
guard: {T},
so_apply: x[s],
bool: 
,
unit: Unit,
it: 
Lemmas :
int_seg_properties,
subtype_base_sq,
int_subtype_base,
assert_wf,
bor_wf,
bnot_wf,
bag-null_wf,
pi1_wf_top,
bag_wf,
Id_wf,
eq_int_wf,
int_seg_wf,
le_wf,
nat_plus_wf,
nat_properties,
ge_wf,
bool_wf,
not_wf,
empty-bag_wf,
decidable__assert,
decidable_wf,
lifting-loc-2_wf,
pi2_wf,
band_wf,
assert_of_bor,
not_functionality_wrt_uiff,
assert-bag-null,
not-not-assert,
btrue_neq_bfalse,
assert_elim,
nat_plus_properties,
bfalse_wf,
uiff_transitivity,
eqtt_to_assert,
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,
SM-gen-tr_wf,
bool_subtype_base,
iff_imp_equal_bool,
iff_functionality_wrt_iff,
false_wf,
iff_weakening_uiff,
ifthenelse_wf,
squash_wf,
true_wf
\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].
\mforall{}[p:\{m..n + 1\msupminus{}\}].
((\mforall{}i:\{m..p\msupminus{}\}. (\muparrow{}bag-null(fst((btrs i)))))
{}\mRightarrow{} (\muparrow{}((\mneg{}\msubb{}bag-null(fst((btrs p)))) \mvee{}\msubb{}(n =\msubz{} p)))
{}\mRightarrow{} (SM-gen-tr(l;btrs;bp;n;m) = (lifting-loc-2(snd((btrs p))) l (fst((btrs p))) bp)))
Date html generated:
2011_10_20-PM-03_35_17
Last ObjectModification:
2011_08_17-PM-03_12_56
Home
Index