Nuprl Lemma : SM4-class_wf
[A,B,C,D,E:
']. [init:Id 
bag(E)]. [trX1:Id A E E 
EClass'(A)]. [trX2:Id B E E EClass'(B)].
[trX3:Id C E E EClass'(C)]. [trX4:Id D E E EClass'(D)].
(SM4-class(init;trX1;trX2;trX3;trX4) 
EClass'(E))
Proof not projected
Definitions occuring in Statement :
SM4-class: SM4-class(init;trX1;trX2;trX3;trX4),
Message: Message,
eclass: EClass(A[eo; e]),
Id: Id,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
universe: Type,
bag: bag(T)
Definitions :
SM4-class: SM4-class(init;trX1;trX2;trX3;trX4),
uall: [x:A]. B[x],
exists: 
x:A. B[x],
label: ...$L... t,
suptype: suptype(S; T),
subtype: S 
T,
bfalse: ff,
btrue: tt,
guard: {T},
all: x:A. B[x],
prop: 
,
false: False,
implies: P 
Q,
not: 
A,
le: A 
B,
and: P 
Q,
lelt: i j < k,
int_seg: {i..j
},
nat_plus: 
,
eq_int: (i =
j),
ifthenelse: if b then t else f fi ,
member: t T,
uiff: uiff(P;Q),
unit: Unit,
uimplies: b supposing a,
sq_type: SQType(T),
or: P 
Q,
decidable: Dec(P),
bool: 
,
it: 
Lemmas :
bag_wf,
btrue_wf,
int_seg_properties,
not_functionality_wrt_uiff,
assert_of_bnot,
eqff_to_assert,
not_wf,
bnot_wf,
eclass_wf2,
Id_wf,
assert_of_eq_int,
eqtt_to_assert,
assert_wf,
uiff_transitivity,
bool_wf,
bfalse_wf,
int_subtype_base,
subtype_base_sq,
decidable__equal_int,
int_seg_wf,
eq_int_wf,
ifthenelse_wf,
le_wf,
Message_wf,
SM-gen-class_wf
\mforall{}[A,B,C,D,E:\mBbbU{}']. \mforall{}[init:Id {}\mrightarrow{} bag(E)]. \mforall{}[trX1:Id {}\mrightarrow{} A {}\mrightarrow{} E {}\mrightarrow{} E \mtimes{} EClass'(A)]. \mforall{}[trX2:Id
{}\mrightarrow{} B
{}\mrightarrow{} E
{}\mrightarrow{} E
\mtimes{} EClass'(B)].
\mforall{}[trX3:Id {}\mrightarrow{} C {}\mrightarrow{} E {}\mrightarrow{} E \mtimes{} EClass'(C)]. \mforall{}[trX4:Id {}\mrightarrow{} D {}\mrightarrow{} E {}\mrightarrow{} E \mtimes{} EClass'(D)].
(SM4-class(init;trX1;trX2;trX3;trX4) \mmember{} EClass'(E))
Date html generated:
2011_10_20-PM-03_37_37
Last ObjectModification:
2011_09_12-AM-10_35_25
Home
Index