Nuprl Lemma : SM2-class_wf
[A,B,C:
']. [init:Id 
bag(C)]. [trX1:Id A C C 
EClass'(A)]. [trX2:Id B C C EClass'(B)].
(SM2-class(init;trX1;trX2) 
EClass'(C))
Proof not projected
Definitions occuring in Statement :
SM2-class: SM2-class(init;trX1;trX2),
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],
SM2-class: SM2-class(init;trX1;trX2),
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:\mBbbU{}']. \mforall{}[init:Id {}\mrightarrow{} bag(C)]. \mforall{}[trX1:Id {}\mrightarrow{} A {}\mrightarrow{} C {}\mrightarrow{} C \mtimes{} EClass'(A)].
\mforall{}[trX2:Id {}\mrightarrow{} B {}\mrightarrow{} C {}\mrightarrow{} C \mtimes{} EClass'(B)].
(SM2-class(init;trX1;trX2) \mmember{} EClass'(C))
Date html generated:
2011_10_20-PM-03_36_41
Last ObjectModification:
2011_08_17-AM-00_55_49
Home
Index