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