Step
*
2
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)
⊢ ||v|| ≥ 1
BY
{ (DVar `v' THENA 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. 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)
⊢ ||[]|| ≥ 1
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. u : {x@0:{f:I-face(X;I)| (f ∈ box)} | ↑((fst(x@0) =z x) ∧b (fst(snd(x@0)) =z i))}
17. v : {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)
= [u / v]
∈ ({x@0:{f:I-face(X;I)| (f ∈ box)} | ↑((fst(x@0) =z x) ∧b (fst(snd(x@0)) =z i))} List)
⊢ ||[u / v]|| ≥ 1
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
\mvdash{} ||v|| \mgeq{} 1
By
Latex:
(DVar `v' THENA Auto)
Home
Index