---

Step * of Lemma get_face-wf

∀[X:CubicalSet]. ∀[I,J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[box:open_box(X;I;J;x;i)].
  (get_face(x;i;box) ∈ {f:I-face(X;I)| (f ∈ box) ∧ (face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))} )
BY
{ (Intros
   THEN Unhide
   THEN (D -1 THEN SplitAndHyps)
   THEN Unfold `get_face` 0
   THEN ((InstLemma `filter_type` [⌜{f:I-face(X;I)| (f ∈ box)} ⌝;⌜λf.((fst(f) =z x) ∧b (fst(snd(f)) =z i))⌝;⌜box⌝]⋅
          THENA Auto
          )
         THEN Reduce (-1)
         )
   THEN GenConclTerm ⌜filter(λf.((fst(f) =z x) ∧b (fst(snd(f)) =z i));box)⌝⋅
   THEN Auto) }

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. (∃f∈box. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
12. (∀f∈box.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
13. (∀f∈box.(fst(f) ∈ [x / J]))
14. (∀f1,f2∈box.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
15. 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
16. v : {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)
= v
∈ ({x@0:{f:I-face(X;I)| (f ∈ box)} | ↑((fst(x@0) =z x) ∧b (fst(snd(x@0)) =z i))}  List)
⊢ v ∈ {f:I-face(X;I)| (f ∈ box) ∧ (face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))}  List

2
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. (∃f∈box. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
12. (∀f∈box.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
13. (∀f∈box.(fst(f) ∈ [x / J]))
14. (∀f1,f2∈box.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
15. 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
16. v : {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)
= v
∈ ({x@0:{f:I-face(X;I)| (f ∈ box)} | ↑((fst(x@0) =z x) ∧b (fst(snd(x@0)) =z i))}  List)
⊢ ||v|| ≥ 1 

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I,J:Cname  List].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].  \mforall{}[box:open\_box(X;I;J;x;i)].
    (get\_face(x;i;box)  \mmember{}  \{f:I-face(X;I)|  (f  \mmember{}  box)  \mwedge{}  (face-name(f)  =  <x,  i>)\}  )


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  (D  -1  THEN  SplitAndHyps)
  THEN  Unfold  `get\_face`  0
  THEN  ((InstLemma  `filter\_type`  [\mkleeneopen{}\{f:I-face(X;I)|  (f  \mmember{}  box)\}  \mkleeneclose{};\mkleeneopen{}\mlambda{}f.((fst(f)  =\msubz{}  x)
                                                                                                                                    \mwedge{}\msubb{}  (fst(snd(f))  =\msubz{}  i))\mkleeneclose{};\mkleeneopen{}box\mkleeneclose{}]\mcdot{}
                THENA  Auto
                )
              THEN  Reduce  (-1)
              )
  THEN  GenConclTerm  \mkleeneopen{}filter(\mlambda{}f.((fst(f)  =\msubz{}  x)  \mwedge{}\msubb{}  (fst(snd(f))  =\msubz{}  i));box)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index