---

Step * 2 of Lemma face-compatible-image


1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : nameset(I)
6. f2 : ℕ2
7. f3 : X(I-[x])
8. y : nameset(I)
9. f5 : ℕ2
10. f6 : X(I-[y])
11. ↑isname(f x)
12. ↑isname(f y)
13. (¬(x = y ∈ Cname)) ⇒ ((y:=f5)(f3) = (x:=f2)(f6) ∈ X(I-[x; y]))
14. f y ∈ nameset(K)
15. f x ∈ nameset(K)
16. ¬((f x) = (f y) ∈ Cname)
17. ¬(x = y ∈ Cname)
⊢ (f y:=f5)(f(f3)) = (f x:=f2)(f(f6)) ∈ X(K-[f x; f y])
BY
{ xxx(DVar `x'
      THEN DVar `y'
      THEN (Assert y ∈ nameset(I-[x]) BY
                  (DVar `y' THEN MemTypeCD THEN Try (RepeatFor 2 ((RW ListC 0 THENA Auto))) THEN Auto))
      THEN (Assert x ∈ nameset(I-[y]) BY
                  (DVar `x' THEN MemTypeCD THEN Try (RepeatFor 2 ((RW ListC 0 THENA Auto))) THEN Auto)))xxx }

1
1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : Cname
6. (x ∈ I)
7. f2 : ℕ2
8. f3 : X(I-[x])
9. y : Cname
10. (y ∈ I)
11. f5 : ℕ2
12. f6 : X(I-[y])
13. ↑isname(f x)
14. ↑isname(f y)
15. (¬(x = y ∈ Cname)) ⇒ ((y:=f5)(f3) = (x:=f2)(f6) ∈ X(I-[x; y]))
16. f y ∈ nameset(K)
17. f x ∈ nameset(K)
18. ¬((f x) = (f y) ∈ Cname)
19. ¬(x = y ∈ Cname)
20. y ∈ nameset(I-[x])
21. x ∈ nameset(I-[y])
⊢ (f y:=f5)(f(f3)) = (f x:=f2)(f(f6)) ∈ X(K-[f x; f y])

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  I  :  Cname  List
3.  K  :  Cname  List
4.  f  :  name-morph(I;K)
5.  x  :  nameset(I)
6.  f2  :  \mBbbN{}2
7.  f3  :  X(I-[x])
8.  y  :  nameset(I)
9.  f5  :  \mBbbN{}2
10.  f6  :  X(I-[y])
11.  \muparrow{}isname(f  x)
12.  \muparrow{}isname(f  y)
13.  (\mneg{}(x  =  y))  {}\mRightarrow{}  ((y:=f5)(f3)  =  (x:=f2)(f6))
14.  f  y  \mmember{}  nameset(K)
15.  f  x  \mmember{}  nameset(K)
16.  \mneg{}((f  x)  =  (f  y))
17.  \mneg{}(x  =  y)
\mvdash{}  (f  y:=f5)(f(f3))  =  (f  x:=f2)(f(f6))


By

---

Latex:
xxx(DVar  `x'
        THEN  DVar  `y'
        THEN  (Assert  y  \mmember{}  nameset(I-[x])  BY
                                (DVar  `y'
                                  THEN  MemTypeCD
                                  THEN  Try  (RepeatFor  2  ((RW  ListC  0  THENA  Auto)))
                                  THEN  Auto))
        THEN  (Assert  x  \mmember{}  nameset(I-[y])  BY
                                (DVar  `x'
                                  THEN  MemTypeCD
                                  THEN  Try  (RepeatFor  2  ((RW  ListC  0  THENA  Auto)))
                                  THEN  Auto)))xxx

---

Home Index