Step
*
1
2
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. (∃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)
18. v = v ∈ ({x@0:{f:I-face(X;I)| (f ∈ box)} | ↑((fst(x@0) =z x) ∧b (fst(snd(x@0)) =z i))} List)
19. x1 : I-face(X;I)
20. (x1 ∈ box)
21. ↑((fst(x1) =z x) ∧b (fst(snd(x1)) =z i))
22. (x1 ∈ box)
⊢ face-name(x1) = <x, i> ∈ (nameset(I) × ℕ2)
BY
{ (RepeatFor 2 (D -4) THEN RepUR ``face-name`` 0 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. (∃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)
18. v = v ∈ ({x@0:{f:I-face(X;I)| (f ∈ box)} | ↑((fst(x@0) =z x) ∧b (fst(snd(x@0)) =z i))} List)
19. x2 : nameset(I)
20. x4 : ℕ2
21. x5 : X(I-[x2])
22. (<x2, x4, x5> ∈ box)
23. ↑((x2 =z x) ∧b (x4 =z i))
24. (<x2, x4, x5> ∈ box)
⊢ <x2, x4> = <x, i> ∈ (nameset(I) × ℕ2)
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. (\mexists{}f\mmember{}box. face-name(f) = <x, i>)
12. (\mforall{}f\mmember{}box.\mneg{}(face-name(f) = <x, 1 - i>))
13. (\mforall{}f\mmember{}box.(fst(f) \mmember{} [x / J]))
14. (\mforall{}f1,f2\mmember{}box. \mneg{}(face-name(f1) = face-name(f2)))
15. 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
16. v : \{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) = v
18. v = v
19. x1 : I-face(X;I)
20. (x1 \mmember{} box)
21. \muparrow{}((fst(x1) =\msubz{} x) \mwedge{}\msubb{} (fst(snd(x1)) =\msubz{} i))
22. (x1 \mmember{} box)
\mvdash{} face-name(x1) = <x, i>
By
Latex:
(RepeatFor 2 (D -4) THEN RepUR ``face-name`` 0 THEN All Reduce)
Home
Index