---

{ [C:Id  Type]. [A,B:Type]. [L2:(tg:Id  (A  B  (C[tg] List))) List].
  [L:(l:IdLnk  t:Id  C[t]) List]. [tg:Id]. [a:A]. [b:B].
    {(||filter(ms.fst(snd(ms)) = tg;L)|| = 0) supposing 
        (((tg  map(p.(fst(p));L2))) and 
        (map(x.(snd(x));L)
        = concat(map(tgf.map(x.<fst(tgf), x>;(snd(tgf)) a b);L2))))} }

{ Proof }

---

Definitions occuring in Statement :  eq_id: a = b,  IdLnk: IdLnk,  Id: Id,  map: map(f;as),  length: ||as||,  uimplies: b supposing a,  uall: [x:A]. B[x],  guard: {T},  so_apply: x[s],  pi1: fst(t),  pi2: snd(t),  not: A,  apply: f a,  lambda: x.A[x],  function: x:A  B[x],  pair: <a, b>,  product: x:A  B[x],  list: type List,  natural_number: $n,  int: ,  universe: Type,  equal: s = t,  filter: filter(P;l),  l_member: (x  l),  concat: concat(ll)
Definitions :  uall: [x:A]. B[x],  so_apply: x[s],  guard: {T},  uimplies: b supposing a,  member: t  T,  top: Top,  all: x:A. B[x],  subtype: S  T,  suptype: suptype(S; T),  prop: ,  so_lambda: x.t[x],  implies: P  Q,  iff: P  Q,  and: P  Q
Lemmas :  map-concat-filter-lemma1,  top_wf,  not_wf,  l_member_wf,  Id_wf,  map_wf,  pi1_wf_top,  IdLnk_wf,  pi2_wf,  concat_wf,  length_wf1,  filter_wf,  eq_id_wf,  iff_weakening_uiff,  uiff_inversion,  length_zero

---

\mforall{}[C:Id  {}\mrightarrow{}  Type].  \mforall{}[A,B:Type].  \mforall{}[L2:(tg:Id  \mtimes{}  (A  {}\mrightarrow{}  B  {}\mrightarrow{}  (C[tg]  List)))  List].  \mforall{}[L:(l:IdLnk
                                                                                                                                                                  \mtimes{}  t:Id
                                                                                                                                                                  \mtimes{}  C[t])  List].
\mforall{}[tg:Id].  \mforall{}[a:A].  \mforall{}[b:B].
    \{(||filter(\mlambda{}ms.fst(snd(ms))  =  tg;L)||  =  0)  supposing 
            ((\mneg{}(tg  \mmember{}  map(\mlambda{}p.(fst(p));L2)))  and 
            (map(\mlambda{}x.(snd(x));L)  =  concat(map(\mlambda{}tgf.map(\mlambda{}x.<fst(tgf),  x>(snd(tgf))  a  b);L2))))\}


Date html generated: 2011_08_10-AM-07_50_59
Last ObjectModification: 2011_06_18-AM-08_13_49

Home Index