{ mlt_nxt_inning() 
List ( + ( )) 
( List ) }
{ Proof }
Definitions occuring in Statement :
nat: ,
member: t T,
function: x:A B[x],
product: x:A B[x],
union: left + right,
list: type List,
int:
Definitions :
int: ,
member: t T,
equal: s = t,
nat: ,
product: x:A B[x],
union: left + right,
list: type List,
natural_number: $n,
pair: <a, b>,
inr: inr x ,
le: A 
B,
universe: Type,
prop: 
,
function: x:A B[x],
all: 
x:A. B[x],
less_than: a < b,
void: Void,
implies: P 
Q,
false: False,
not: 
A,
set: {x:A| B[x]} ,
p-outcome: Outcome,
subtype_rel: A 
r B,
strong-subtype: strong-subtype(A;B),
rationals: 
,
subtype: S T,
real: 
,
nil: [],
add: n + m,
ge: i 
j ,
l_member: (x l),
eq_int: (i =
j),
bool: 
,
bnot: 
b,
lambda: 
x.A[x],
so_lambda: 
x.t[x],
bl-exists: (
xL.P[x])_b,
ifthenelse: if b then t else f fi ,
cons: [car / cdr],
le_int: i z j,
spread: spread def,
inl: inl x ,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
spreadn: spread3,
fpf: a:A fp-> B[a],
guard: {T},
sq_type: SQType(T),
sqequal: s ~ t,
true: True,
squash: 
T,
assert: 
b,
and: P 
Q,
iff: P 
Q,
rev_implies: P Q,
apply: f a,
so_apply: x[s],
or: P 
Q,
pi2: snd(t),
limited-type: LimitedType,
pi1: fst(t),
bfalse: ff,
btrue: tt,
length: ||as||,
isect: 
x:A. B[x],
top: Top,
mlt_nxt_inning: mlt_nxt_inning()
Lemmas :
length_wf1,
top_wf,
false_wf,
length_wf_nat,
non_neg_length,
btrue_wf,
bfalse_wf,
bool_wf,
decide_wf,
pi1_wf,
pi2_wf,
cons_one_one,
assert_wf,
guard_wf,
nat_sq,
int_sq,
member_wf,
le_int_wf,
ifthenelse_wf,
bl-exists_wf,
bnot_wf,
eq_int_wf,
l_member_wf,
nat_properties,
le_wf,
nat_wf
mlt\_nxt\_inning() \mmember{} \mBbbN{} \mtimes{} \mBbbZ{} List \mtimes{} \mBbbN{} \mtimes{} (\mBbbZ{} + (\mBbbN{} \mtimes{} \mBbbN{} \mtimes{} \mBbbZ{})) {}\mrightarrow{} (\mBbbN{} \mtimes{} \mBbbZ{} List \mtimes{} \mBbbN{})
Date html generated:
2010_08_27-PM-08_30_23
Last ObjectModification:
2010_06_23-PM-11_54_11
Home
Index