Nuprl Lemma : SM2-class-gen-classrel
[es:EO']. [e:E]. [S,A,B:
']. [init:Id 
bag(S)]. [tr1:Id A S S]. [X1:EClass'(A)]. [tr2:Id
B
S
S].
[X2:EClass'(B)]. [s:S].
uiff(s 
SM2-class(init;<tr1, X1>;<tr2, X2>)(
e);
L:(n:{1..3
} 
if (n =
1) then A else B fi E) List
(classrel-multi-list(es;
n.if (n = 1) then A else B fi ;n.if (n = 1) then X1 else X2 fi ;L;e;1;3)
(
null(L))
(e = (snd(snd(last(L)))))
(x:S
(x init loc(e)
(s
= list_accum(a,b.if (fst(b) = 1) then tr1 else tr2 fi loc(snd(snd(b))) (fst(snd(b))) a;x;L))))))
Proof not projected
Definitions occuring in Statement :
SM2-class: SM2-class(init;trX1;trX2),
classrel-multi-list: classrel-multi-list(es;A;Xs;L;e;n1;n2),
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),
eq_int: (i = j),
assert: b,
ifthenelse: if b then t else f fi ,
int_seg: {i..j},
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],
pair: <a, b>,
product: x:A B[x],
list: type List,
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 :
so_lambda: 
x y.t[x; y],
top: Top,
bfalse: ff,
btrue: tt,
guard: {T},
false: False,
implies: P 
Q,
le: A 
B,
ge: i 
j ,
cand: A c B,
so_lambda: x.t[x],
subtype: S 
T,
all: x:A. B[x],
prop: 
,
member: t T,
pi1: fst(t),
pi2: snd(t),
not: A,
and: P Q,
eq_int: (i = j),
ifthenelse: if b then t else f fi ,
exists: x:A. B[x],
eclass: EClass(A[eo; e]),
suptype: suptype(S; T),
lelt: i j < k,
nat_plus: 
,
int_seg: {i..j},
true: True,
label: ...$L... t,
squash: T,
iff: P 
Q,
rev_implies: P Q,
uimplies: b supposing a,
bag-member: x bs,
classrel: v X(e),
uiff: uiff(P;Q),
unit: Unit,
so_apply: x[s1;s2],
sq_type: SQType(T),
or: P 
Q,
decidable: Dec(P),
bool: 
,
so_apply: x[s],
uall: [x:A]. B[x],
it: 
,
SM2-class: SM2-class(init;trX1;trX2)
Lemmas :
Id_wf,
bag_wf,
event-ordering+_wf,
not_functionality_wrt_uiff,
assert_of_bnot,
eqff_to_assert,
bnot_wf,
subtype_rel_self,
subtype_rel_simple_product,
assert_of_eq_int,
eqtt_to_assert,
equal_wf,
uiff_transitivity,
bool_wf,
list_accum_wf,
es-loc_wf,
bag-member_wf,
last_wf,
pi1_wf_top,
pi2_wf,
top_wf,
null_wf3,
assert_wf,
not_wf,
eclass_wf2,
int_subtype_base,
subtype_base_sq,
decidable__equal_int,
ge_wf,
classrel-multi-list_wf,
event-ordering+_inc,
es-E_wf,
eq_int_wf,
ifthenelse_wf,
int_seg_wf,
exists_wf,
squash_wf,
SM2-class_wf2,
Message_wf,
classrel_wf,
btrue_wf,
int_seg_properties,
bfalse_wf,
lelt_wf,
SM-gen-class-classrel,
uiff_wf,
true_wf,
and_wf,
apply-ifthenelse-pi2-eq,
le_wf,
SM-gen-class_wf,
apply-ifthenelse-pi2,
Error :pi2_wf,
apply-ifthenelse-pi1,
set_subtype_base,
bool_subtype_base,
bool_cases
\mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[S,A,B:\mBbbU{}']. \mforall{}[init:Id {}\mrightarrow{} bag(S)]. \mforall{}[tr1:Id {}\mrightarrow{} A {}\mrightarrow{} S {}\mrightarrow{} S]. \mforall{}[X1:EClass'(A)].
\mforall{}[tr2:Id {}\mrightarrow{} B {}\mrightarrow{} S {}\mrightarrow{} S]. \mforall{}[X2:EClass'(B)]. \mforall{}[s:S].
uiff(s \mmember{} SM2-class(init;<tr1, X1><tr2, X2>)(
e);\mdownarrow{}\mexists{}L:(n:\{1..3\msupminus{}\} \mtimes{} if (n =\msubz{} 1) then A else B fi \mtimes{} E) List
(classrel-multi-list(es;\mlambda{}n.if (n =\msubz{} 1) then A else B fi ;\mlambda{}n.if (n =\msubz{} 1)
then X1
else X2
fi ;L;e;1;3)
\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.if (fst(b) =\msubz{} 1) then tr1 else tr2 fi loc(snd(snd(b)))
(fst(snd(b)))
a;
x;
L))))))
Date html generated:
2012_01_23-PM-01_22_42
Last ObjectModification:
2012_01_06-PM-02_50_08
Home
Index