Nuprl Lemma : SM-gen-class-classrel
[es:EO']. [e:E]. [S:
']. [n:
]. [m:{1..n + 1
}]. [A:{m..n + 1} 
']. [init:Id bag(S)].
[trXs:k:{m..n + 1} (Id A k S S 
EClass'(A k))]. [s:S].
uiff(s 
SM-gen-class(init;n;m;trXs)(e);
L:(n:{m..n + 1} A n E) List
(classrel-multi-list(es;A;
n.(snd((trXs n)));L;e;m;n + 1)
(
null(L))
(e = (snd(snd(last(L)))))
(x:S
(x init loc(e)
(s
= list_accum(a,b.(fst((trXs (fst(b))))) loc(snd(snd(b)))
(fst(snd(b)))
a;
x;
L))))))
Proof not projected
Definitions occuring in Statement :
classrel-multi-list: classrel-multi-list(es;A;Xs;L;e;n1;n2),
SM-gen-class: SM-gen-class(init;n;m;trXs),
Message: Message,
classrel: v X(e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-loc: loc(e),
es-E: E,
Id: Id,
null: null(as),
assert: b,
int_seg: {i..j},
nat_plus: ,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
pi1: fst(t),
pi2: snd(t),
exists: x:A. B[x],
not: A,
squash: T,
and: P Q,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
product: x:A B[x],
list: type List,
add: n + m,
natural_number: $n,
universe: Type,
equal: s = t,
list_accum: list_accum(x,a.f[x; a];y;l),
last: last(L),
bag-member: x bs,
bag: bag(T)
Definitions :
eclass: EClass(A[eo; e]),
uiff: uiff(P;Q),
classrel: v X(e),
squash: T,
exists: x:A. B[x],
and: P Q,
pi2: snd(t),
not: A,
bag-member: x bs,
pi1: fst(t),
all: x:A. B[x],
member: t T,
subtype: S 
T,
nat: ,
implies: P 
Q,
ge: i 
j ,
le: A 
B,
false: False,
prop: 
,
true: True,
uimplies: b supposing a,
so_lambda: 
x.t[x],
cand: A c B,
label: ...$L... t,
top: Top,
so_lambda: x y.t[x; y],
assert: b,
null: null(as),
last: last(L),
band: p 
q,
btrue: tt,
bfalse: ff,
ifthenelse: if b then t else f fi ,
select: l[i],
length: ||as||,
ycomb: Y,
le_int: i z j,
bnot: b,
lt_int: i <z j,
classrel-multi-list: classrel-multi-list(es;A;Xs;L;e;n1;n2),
l_all: (xL.P[x]),
iff: P 
Q,
rev_implies: P Q,
so_apply: x[s],
int_seg: {i..j},
sorted-by: sorted-by(R;L),
lelt: i j < k,
or: P 
Q,
guard: {T},
l_disjoint: l_disjoint(T;l1;l2),
Id: Id,
es-le: e loc e' ,
list_accum: list_accum(x,a.f[x; a];y;l),
map: map(f;as),
es-p-local-pred: es-p-local-pred(es;P),
listp: A List,
nat_plus: ,
strongwellfounded: SWellFounded(R[x; y]),
uall: [x:A]. B[x],
so_apply: x[s1;s2],
es-locl: (e <loc e'),
sq_type: SQType(T),
l_member: (x l),
rev_uimplies: rev_uimplies(P;Q),
decidable: Dec(P),
sq_stable: SqStable(P),
append: as @ bs,
gt: i > j,
no_repeats: no_repeats(T;l),
bool: 
,
unit: Unit,
it: 
Lemmas :
es-causl-swellfnd,
event-ordering+_inc,
Message_wf,
nat_properties,
ge_wf,
less_than_wf,
nat_wf,
le_wf,
es-causl_wf,
classrel_wf,
SM-gen-class_wf,
squash_wf,
exists_wf,
int_seg_wf,
es-E_wf,
classrel-multi-list_wf,
pi2_wf,
eclass_wf2,
not_wf,
assert_wf,
null_wf3,
top_wf,
pi1_wf_top,
last_wf,
bag-member_wf,
es-loc_wf,
list_accum_wf,
Id_wf,
subtype_rel_simple_product,
event-ordering+_wf,
bag_wf,
subtype_rel_self,
equal_wf,
nat_plus_wf,
SM-gen-classrel-step,
primed-class-opt-classrel,
append_wf,
null_append,
last_append,
false_wf,
not_assert_elim,
subtype_base_sq,
bool_wf,
bool_subtype_base,
and_wf,
band_wf,
l_member_wf,
member_append,
member_singleton,
true_wf,
eclass_wf,
sorted-by-append,
es-locl_wf,
length_wf,
int_subtype_base,
lelt_wf,
select_wf,
es-locl_transitivity2,
es-le_weakening,
map_append,
no_repeats_wf,
no_repeats-append,
map_wf,
no_repeats-single,
es-locl_irreflexivity,
decidable__es-le,
decidable__es-locl,
es-le-not-locl,
es-le_wf,
all_wf,
cons_member,
primed-class-opt-exists,
atom2_subtype_base,
primed-class-opt_wf,
es-locl_transitivity1,
or_functionality_wrt_iff,
list_accum_append,
nil_member,
sq_stable__classrel,
firstn_wf,
pair-eta,
firstn_last,
length_wf_nat,
member_wf,
non_neg_length,
length_zero,
iff_wf,
es-p-local-pred_wf,
es-le_weakening_eq,
or_wf,
iff_functionality_wrt_iff,
pos_length2,
member_map,
last_member,
length-map,
length-append,
uall_wf,
isect_wf,
length_nil,
length_wf_nil,
length_cons,
iff_imp_equal_bool,
lt_int_wf,
btrue_wf,
iff_weakening_uiff,
assert_of_lt_int,
le_int_wf,
bnot_wf,
select-map,
select_append,
uiff_transitivity,
eqtt_to_assert,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_of_lt_int,
assert_of_le_int,
bfalse_wf,
event_ordering_wf,
select-append,
classrel-multi-list-prefix
\mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[S:\mBbbU{}']. \mforall{}[n:\mBbbN{}\msupplus{}]. \mforall{}[m:\{1..n + 1\msupminus{}\}]. \mforall{}[A:\{m..n + 1\msupminus{}\} {}\mrightarrow{} \mBbbU{}']. \mforall{}[init:Id {}\mrightarrow{} bag(S)].
\mforall{}[trXs:k:\{m..n + 1\msupminus{}\} {}\mrightarrow{} (Id {}\mrightarrow{} A k {}\mrightarrow{} S {}\mrightarrow{} S \mtimes{} EClass'(A k))]. \mforall{}[s:S].
uiff(s \mmember{} SM-gen-class(init;n;m;trXs)(e);\mdownarrow{}\mexists{}L:(n:\{m..n + 1\msupminus{}\} \mtimes{} A n \mtimes{} E) List
(classrel-multi-list(es;A;\mlambda{}n.(snd((trXs n)));L;e;m;n
+ 1)
\mwedge{} (\mneg{}\muparrow{}null(L))
\mwedge{} (e = (snd(snd(last(L)))))
\mwedge{} (\mexists{}x:S
(x \mdownarrow{}\mmember{} init loc(e)
\mwedge{} (s
= list\_accum(a,b.(fst((trXs (fst(b)))))
loc(snd(snd(b)))
(fst(snd(b)))
a;
x;
L))))))
Date html generated:
2012_01_23-PM-01_22_14
Last ObjectModification:
2012_01_06-PM-05_37_38
Home
Index