---

{ [A,B:Type]. [L2:(tg:Id  (A  B  (Top List))) List].
  [L:(Top  Id  Top) List]. [tg:Id]. [a:A]. [b:B].
    {(filter(ms.fst(snd(ms)) = tg;L) = []) 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,  Id: Id,  map: map(f;as),  uimplies: b supposing a,  uall: [x:A]. B[x],  top: Top,  guard: {T},  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],  nil: [],  list: type List,  universe: Type,  equal: s = t,  filter: filter(P;l),  l_member: (x  l),  concat: concat(ll)
Definitions :  uall: [x:A]. B[x],  top: Top,  guard: {T},  uimplies: b supposing a,  not: A,  member: t  T,  prop: ,  implies: P  Q,  so_lambda: x.t[x],  false: False,  all: x:A. B[x],  subtype: S  T,  exists: x:A. B[x],  and: P  Q,  pi1: fst(t),  rev_implies: P  Q,  iff: P  Q,  so_apply: x[s],  pi2: snd(t)
Lemmas :  iff_weakening_uiff,  filter_wf,  eq_id_wf,  pi1_wf_top,  pi2_wf,  uall_wf,  not_wf,  l_member_wf,  nil-iff-no-member,  Id_wf,  map_wf,  top_wf,  concat_wf,  member_filter,  assert_wf,  assert-eq-id,  member_map,  member-concat

---

\mforall{}[A,B:Type].  \mforall{}[L2:(tg:Id  \mtimes{}  (A  {}\mrightarrow{}  B  {}\mrightarrow{}  (Top  List)))  List].  \mforall{}[L:(Top  \mtimes{}  Id  \mtimes{}  Top)  List].  \mforall{}[tg:Id].
\mforall{}[a:A].  \mforall{}[b:B].
    \{(filter(\mlambda{}ms.fst(snd(ms))  =  tg;L)  =  [])  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_55
Last ObjectModification: 2011_06_18-AM-08_13_47

Home Index