{ 
[t:
]. (mlt_inning_test(t) 
List 
+ ( ) 
) }
{ Proof }
Definitions occuring in Statement :
mlt_inning_test: mlt_inning_test(t),
bool: ,
nat: ,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
union: left + right,
list: type List,
int:
Definitions :
uall: [x:A]. B[x],
member: t T,
mlt_inning_test: mlt_inning_test(t),
spreadn: spread3,
nat:
Lemmas :
eq_int_wf,
bor_wf,
lt_int_wf,
band_wf,
le_int_wf,
length_wf1,
nat_wf
\mforall{}[t:\mBbbZ{}]. (mlt\_inning\_test(t) \mmember{} \mBbbN{} \mtimes{} \mBbbZ{} List \mtimes{} \mBbbN{} {}\mrightarrow{} \mBbbZ{} + (\mBbbN{} \mtimes{} \mBbbN{} \mtimes{} \mBbbZ{}) {}\mrightarrow{} \mBbbB{})
Date html generated:
2011_08_17-PM-06_31_28
Last ObjectModification:
2011_06_18-AM-11_54_14
Home
Index