---

{ mlt_inning_step()     List     + (    )  (   List  ) }

{ Proof }

---

Definitions occuring in Statement :  mlt_inning_step: mlt_inning_step(),  nat: ,  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  union: left + right,  list: type List,  int:
Definitions :  equal: s = t,  member: t  T,  nat: ,  int: ,  list: type List,  product: x:A  B[x],  union: left + right,  pair: <a, b>,  inr: inr x ,  cons: [car / cdr],  universe: Type,  natural_number: $n,  le: A  B,  ge: i  j ,  set: {x:A| B[x]} ,  function: x:A  B[x],  all: x:A. B[x],  subtract: n - m,  eq_int: (i = j),  bool: ,  ifthenelse: if b then t else f fi ,  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],  l_member: (x  l),  apply: f a,  so_apply: x[s],  implies: P  Q,  or: P  Q,  guard: {T},  assert: b,  lambda: x.A[x],  mlt_inning_step: mlt_inning_step()
Lemmas :  member_wf,  ifthenelse_wf,  eq_int_wf,  nat_properties,  nat_wf

---

mlt\_inning\_step()  \mmember{}  \mBbbN{}  \mtimes{}  \mBbbZ{}  List  \mtimes{}  \mBbbN{}  {}\mrightarrow{}  \mBbbZ{}  +  (\mBbbN{}  \mtimes{}  \mBbbN{}  \mtimes{}  \mBbbZ{})  {}\mrightarrow{}  (\mBbbN{}  \mtimes{}  \mBbbZ{}  List  \mtimes{}  \mBbbN{})


Date html generated: 2010_08_27-PM-08_30_37
Last ObjectModification: 2010_06_23-PM-11_57_09

Home Index