Step
*
1
2
1
1
2
2
1
of Lemma
name-morph-decomp
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. ∀[f@0:{x:nameset(I)| ↑¬bisname(f x)} ⟶ (Cname × ℕ2)]. (mapfilter(f@0;λx.(¬bisname(f x));I) ∈ (Cname × ℕ2) List)
5. mapfilter(λx.<x, f x>;λx.(¬bisname(f x));I) ∈ (Cname × ℕ2) List
6. nameset(I) ≡ nameset(filter(λx.(¬bisname(f x));I) @ filter(λx.isname(f x);I))
7. K : Cname List
8. nameset(I) ≡ nameset(filter(λx.(¬bisname(f x));I) @ K)
9. g : nameset(K) ⟶ nameset(J)
10. Inj(nameset(K);nameset(J);g)
11. face-maps-comp(mapfilter(λx.<x, f x>;λx.(¬bisname(f x));I)) ∈ name-morph(map(λp.(fst(p));mapfilter(λx.<x, f x>;
λx.(¬bisname(f
x));
I))
@ K;K)
⊢ face-maps-comp(mapfilter(λx.<x, f x>;λx.(¬bisname(f x));I)) ∈ name-morph(I;K)
BY
{ Subst' map(λp.(fst(p));mapfilter(λx.<x, f x>;λx.(¬bisname(f x));I)) ~ filter(λx.(¬bisname(f x));I) -1 }
1
.....equality.....
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. ∀[f@0:{x:nameset(I)| ↑¬bisname(f x)} ⟶ (Cname × ℕ2)]. (mapfilter(f@0;λx.(¬bisname(f x));I) ∈ (Cname × ℕ2) List)
5. mapfilter(λx.<x, f x>;λx.(¬bisname(f x));I) ∈ (Cname × ℕ2) List
6. nameset(I) ≡ nameset(filter(λx.(¬bisname(f x));I) @ filter(λx.isname(f x);I))
7. K : Cname List
8. nameset(I) ≡ nameset(filter(λx.(¬bisname(f x));I) @ K)
9. g : nameset(K) ⟶ nameset(J)
10. Inj(nameset(K);nameset(J);g)
11. face-maps-comp(mapfilter(λx.<x, f x>;λx.(¬bisname(f x));I)) ∈ name-morph(map(λp.(fst(p));mapfilter(λx.<x, f x>;
λx.(¬bisname(f
x));
I))
@ K;K)
⊢ map(λp.(fst(p));mapfilter(λx.<x, f x>;λx.(¬bisname(f x));I)) ~ filter(λx.(¬bisname(f x));I)
2
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. ∀[f@0:{x:nameset(I)| ↑¬bisname(f x)} ⟶ (Cname × ℕ2)]. (mapfilter(f@0;λx.(¬bisname(f x));I) ∈ (Cname × ℕ2) List)
5. mapfilter(λx.<x, f x>;λx.(¬bisname(f x));I) ∈ (Cname × ℕ2) List
6. nameset(I) ≡ nameset(filter(λx.(¬bisname(f x));I) @ filter(λx.isname(f x);I))
7. K : Cname List
8. nameset(I) ≡ nameset(filter(λx.(¬bisname(f x));I) @ K)
9. g : nameset(K) ⟶ nameset(J)
10. Inj(nameset(K);nameset(J);g)
11. face-maps-comp(mapfilter(λx.<x, f x>;λx.(¬bisname(f x));I)) ∈ name-morph(filter(λx.(¬bisname(f x));I) @ K;K)
⊢ face-maps-comp(mapfilter(λx.<x, f x>;λx.(¬bisname(f x));I)) ∈ name-morph(I;K)
Latex:
Latex:
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. \mforall{}[f@0:\{x:nameset(I)| \muparrow{}\mneg{}\msubb{}isname(f x)\} {}\mrightarrow{} (Cname \mtimes{} \mBbbN{}2)]
(mapfilter(f@0;\mlambda{}x.(\mneg{}\msubb{}isname(f x));I) \mmember{} (Cname \mtimes{} \mBbbN{}2) List)
5. mapfilter(\mlambda{}x.<x, f x>\mlambda{}x.(\mneg{}\msubb{}isname(f x));I) \mmember{} (Cname \mtimes{} \mBbbN{}2) List
6. nameset(I) \mequiv{} nameset(filter(\mlambda{}x.(\mneg{}\msubb{}isname(f x));I) @ filter(\mlambda{}x.isname(f x);I))
7. K : Cname List
8. nameset(I) \mequiv{} nameset(filter(\mlambda{}x.(\mneg{}\msubb{}isname(f x));I) @ K)
9. g : nameset(K) {}\mrightarrow{} nameset(J)
10. Inj(nameset(K);nameset(J);g)
11. face-maps-comp(mapfilter(\mlambda{}x.<x, f x>\mlambda{}x.(\mneg{}\msubb{}isname(f x));I))
\mmember{} name-morph(map(\mlambda{}p.(fst(p));mapfilter(\mlambda{}x.<x, f x>\mlambda{}x.(\mneg{}\msubb{}isname(f x));I)) @ K;K)
\mvdash{} face-maps-comp(mapfilter(\mlambda{}x.<x, f x>\mlambda{}x.(\mneg{}\msubb{}isname(f x));I)) \mmember{} name-morph(I;K)
By
Latex:
Subst' map(\mlambda{}p.(fst(p));mapfilter(\mlambda{}x.<x, f x>\mlambda{}x.(\mneg{}\msubb{}isname(f x));I))
\msim{} filter(\mlambda{}x.(\mneg{}\msubb{}isname(f x));I) -1
Home
Index