---

Step * 2 1 1 1 1 1 of Lemma get_face-wf


1. X : CubicalSet
2. I : Cname List
3. J : Cname List
4. x : nameset(I)
5. i : ℕ2
6. box : I-face(X;I) List
7. adjacent-compatible(X;I;box)
8. ¬(x ∈ J)
9. l_subset(Cname;J;I)
10. ∀y:nameset(J). ∀c:ℕ2.  (∃f∈box. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
11. i@0 : ℕ||box||
12. face-name(box[i@0]) = <x, i> ∈ (nameset(I) × ℕ2)
13. (∀f∈box.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
14. (∀f∈box.(fst(f) ∈ [x / J]))
15. (∀f1,f2∈box.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
16. filter(λf.((fst(f) =z x) ∧b (fst(snd(f)) =z i));box) ∈ {x@0:{f:I-face(X;I)| (f ∈ box)} | 
                                                            ↑((fst(x@0) =z x) ∧b (fst(snd(x@0)) =z i))}  List
17. filter(λf.((fst(f) =z x) ∧b (fst(snd(f)) =z i));box)
= []
∈ ({x@0:{f:I-face(X;I)| (f ∈ box)} | ↑((fst(x@0) =z x) ∧b (fst(snd(x@0)) =z i))}  List)
18. filter(λf.((fst(f) =z x) ∧b (fst(snd(f)) =z i));box) = [] ∈ ({f:I-face(X;I)| (f ∈ box)}  List)
⊢ ↑((fst(box[i@0]) =z x) ∧b (fst(snd(box[i@0])) =z i))
BY
{ (RepUR ``face-name`` 12 THEN (EqHD 12 THENA Auto) THEN All Reduce) }

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

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  I  :  Cname  List
3.  J  :  Cname  List
4.  x  :  nameset(I)
5.  i  :  \mBbbN{}2
6.  box  :  I-face(X;I)  List
7.  adjacent-compatible(X;I;box)
8.  \mneg{}(x  \mmember{}  J)
9.  l\_subset(Cname;J;I)
10.  \mforall{}y:nameset(J).  \mforall{}c:\mBbbN{}2.    (\mexists{}f\mmember{}box.  face-name(f)  =  <y,  c>)
11.  i@0  :  \mBbbN{}||box||
12.  face-name(box[i@0])  =  <x,  i>
13.  (\mforall{}f\mmember{}box.\mneg{}(face-name(f)  =  <x,  1  -  i>))
14.  (\mforall{}f\mmember{}box.(fst(f)  \mmember{}  [x  /  J]))
15.  (\mforall{}f1,f2\mmember{}box.    \mneg{}(face-name(f1)  =  face-name(f2)))
16.  filter(\mlambda{}f.((fst(f)  =\msubz{}  x)  \mwedge{}\msubb{}  (fst(snd(f))  =\msubz{}  i));box)  \mmember{}  \{x@0:\{f:I-face(X;I)|  (f  \mmember{}  box)\}  | 
                                                                                                                        \muparrow{}((fst(x@0)  =\msubz{}  x)
                                                                                                                        \mwedge{}\msubb{}  (fst(snd(x@0))  =\msubz{}  i))\}    List
17.  filter(\mlambda{}f.((fst(f)  =\msubz{}  x)  \mwedge{}\msubb{}  (fst(snd(f))  =\msubz{}  i));box)  =  []
18.  filter(\mlambda{}f.((fst(f)  =\msubz{}  x)  \mwedge{}\msubb{}  (fst(snd(f))  =\msubz{}  i));box)  =  []
\mvdash{}  \muparrow{}((fst(box[i@0])  =\msubz{}  x)  \mwedge{}\msubb{}  (fst(snd(box[i@0]))  =\msubz{}  i))


By

---

Latex:
(RepUR  ``face-name``  12  THEN  (EqHD  12  THENA  Auto)  THEN  All  Reduce)

---

Home Index