---

Step * of Lemma extend-A-open-box_wf

No Annotations
∀X:CubicalSet. ∀A:{X ⊢ _}. ∀I:Cname List. ∀alpha:X(I).
  ∀[J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[bx:A-open-box(X;A;I;alpha;J;x;i)]. ∀[f1,f2:A-face(X;A;I;alpha)].
  ∀[z:nameset(I)].
    extend-A-open-box(bx;f1;f2) ∈ A-open-box(X;A;I;alpha;[z / J];x;i) 
    supposing ((¬(z ∈ J))
              ∧ (A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2))
              ∧ (A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)))
    ∧ (¬(x = z ∈ Cname))
    ∧ (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
BY
{ (Auto
   THEN (DVar `bx' THEN DVar `z')
   THEN Unfolds ``extend-A-open-box A-open-box`` 0
   THEN MemTypeCD
   THEN Try (CompleteAuto)
   THEN ParallelOp -10
   THEN RepeatFor 2 (ParallelOp -10)
   THEN Try (((RW ListC (-1) THENM D -1) THEN Auto))
   THEN Try ((BLemma `l_subset_cons` THEN Auto))) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. alpha : X(I)
5. J : Cname List
6. x : nameset(I)
7. i : ℕ2
8. bx : A-face(X;A;I;alpha) List
9. (¬(x ∈ J))
∧ l_subset(Cname;J;I)
∧ ((∀y:nameset(J). ∀c:ℕ2.  (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
  ∧ (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
  ∧ (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈bx.(fst(f) ∈ [x / J]))
∧ (∀f1,f2∈bx.  ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
10. ∀i:ℕ||bx||. ∀j:ℕi.  A-face-compatible(X;A;I;alpha;bx[j];bx[i])
11. f1 : A-face(X;A;I;alpha)
12. f2 : A-face(X;A;I;alpha)
13. z : Cname
14. (z ∈ I)
15. ¬(z ∈ J)
16. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
17. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
18. ¬(x = z ∈ Cname)
19. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
⊢ ∀i:ℕ||[f1; [f2 / bx]]||. ∀j:ℕi.  A-face-compatible(X;A;I;alpha;[f1; [f2 / bx]][j];[f1; [f2 / bx]][i])

2
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. alpha : X(I)
5. J : Cname List
6. x : nameset(I)
7. i : ℕ2
8. bx : A-face(X;A;I;alpha) List
9. A-adjacent-compatible(X;A;I;alpha;bx)
10. ¬(x ∈ J)
11. l_subset(Cname;J;I)
12. ((∀y:nameset(J). ∀c:ℕ2.  (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
    ∧ (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
    ∧ (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈bx.(fst(f) ∈ [x / J]))
∧ (∀f1,f2∈bx.  ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
13. f1 : A-face(X;A;I;alpha)
14. f2 : A-face(X;A;I;alpha)
15. z : Cname
16. (z ∈ I)
17. ¬(z ∈ J)
18. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
19. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
20. ¬(x = z ∈ Cname)
21. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
⊢ ((∀y:nameset([z / J]). ∀c:ℕ2.  (∃f∈[f1; [f2 / bx]]. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
  ∧ (∃f∈[f1; [f2 / bx]]. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
  ∧ (∀f∈[f1; [f2 / bx]].¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈[f1; [f2 / bx]].(fst(f) ∈ [x; [z / J]]))
∧ (∀f1,f2∈[f1; [f2 / bx]].  ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}I:Cname  List.  \mforall{}alpha:X(I).
    \mforall{}[J:Cname  List].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].  \mforall{}[bx:A-open-box(X;A;I;alpha;J;x;i)].
    \mforall{}[f1,f2:A-face(X;A;I;alpha)].  \mforall{}[z:nameset(I)].
        extend-A-open-box(bx;f1;f2)  \mmember{}  A-open-box(X;A;I;alpha;[z  /  J];x;i) 
        supposing  ((\mneg{}(z  \mmember{}  J))  \mwedge{}  (A-face-name(f1)  =  <z,  0>)  \mwedge{}  (A-face-name(f2)  =  <z,  1>))
        \mwedge{}  (\mneg{}(x  =  z))
        \mwedge{}  (\mforall{}f\mmember{}bx.A-face-compatible(X;A;I;alpha;f1;f)  \mwedge{}  A-face-compatible(X;A;I;alpha;f2;f))


By

---

Latex:
(Auto
  THEN  (DVar  `bx'  THEN  DVar  `z')
  THEN  Unfolds  ``extend-A-open-box  A-open-box``  0
  THEN  MemTypeCD
  THEN  Try  (CompleteAuto)
  THEN  ParallelOp  -10
  THEN  RepeatFor  2  (ParallelOp  -10)
  THEN  Try  (((RW  ListC  (-1)  THENM  D  -1)  THEN  Auto))
  THEN  Try  ((BLemma  `l\_subset\_cons`  THEN  Auto)))

---

Home Index