Step
*
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)
⊢ v ∈ {f:I-face(X;I)| (f ∈ box) ∧ (face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))} List
BY
{ DoSubsume }
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 ∈ {x@0:{f:I-face(X;I)| (f ∈ box)} | ↑((fst(x@0) =z x) ∧b (fst(snd(x@0)) =z i))} 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)
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)
⊢ ({x@0:{f:I-face(X;I)| (f ∈ box)} | ↑((fst(x@0) =z x) ∧b (fst(snd(x@0)) =z i))} List) ⊆r ({f:I-face(X;I)|
(f ∈ box)
∧ (face-name(f)
= <x, i>
∈ (nameset(I) × ℕ2))} List)
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 \mmember{} \{f:I-face(X;I)| (f \mmember{} box) \mwedge{} (face-name(f) = <x, i>)\} List
By
Latex:
DoSubsume
Home
Index