---

Step * 1 of Lemma map-concat-filter-lemma2


1. C : Id ─→ Type
2. A : Type
3. B : Type
4. L2 : (tg:Id × (A ─→ B ─→ (C[tg] List))) List
5. L : (l:IdLnk × t:Id × C[t]) List
6. tg : Id
7. a : A
8. b : B
9. (filter(λms.fst(snd(ms)) = tg;L) = [] ∈ ((Top × Id × Top) List)) 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)) ∈ ((tg:Id × Top) List)))
⊢ (||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)) ∈ ((tg:Id × C[tg]) List)))
BY
{ ParallelOp (-1) }

1
.....antecedent..... 
1. C : Id ─→ Type
2. A : Type
3. B : Type
4. L2 : (tg:Id × (A ─→ B ─→ (C[tg] List))) List
5. L : (l:IdLnk × t:Id × C[t]) List
6. tg : Id
7. a : A
8. b : B
9. map(λx.(snd(x));L) = concat(map(λtgf.map(λx.<fst(tgf), x>;(snd(tgf)) a b);L2)) ∈ ((tg:Id × C[tg]) List)
⊢ map(λx.(snd(x));L) = concat(map(λtgf.map(λx.<fst(tgf), x>;(snd(tgf)) a b);L2)) ∈ ((tg:Id × Top) List)

2
1. C : Id ─→ Type
2. A : Type
3. B : Type
4. L2 : (tg:Id × (A ─→ B ─→ (C[tg] List))) List
5. L : (l:IdLnk × t:Id × C[t]) List
6. tg : Id
7. a : A
8. b : B
9. map(λx.(snd(x));L) = concat(map(λtgf.map(λx.<fst(tgf), x>;(snd(tgf)) a b);L2)) ∈ ((tg:Id × C[tg]) List)
10. filter(λms.fst(snd(ms)) = tg;L) = [] ∈ ((Top × Id × Top) List) supposing ¬(tg ∈ map(λp.(fst(p));L2))
⊢ ||filter(λms.fst(snd(ms)) = tg;L)|| = 0 ∈ ℤ supposing ¬(tg ∈ map(λp.(fst(p));L2))

---

Latex:



1.  C  :  Id  {}\mrightarrow{}  Type
2.  A  :  Type
3.  B  :  Type
4.  L2  :  (tg:Id  \mtimes{}  (A  {}\mrightarrow{}  B  {}\mrightarrow{}  (C[tg]  List)))  List
5.  L  :  (l:IdLnk  \mtimes{}  t:Id  \mtimes{}  C[t])  List
6.  tg  :  Id
7.  a  :  A
8.  b  :  B
9.  (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))))
\mvdash{}  (||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))))


By

ParallelOp  (-1)

---

Home Index