Step
*
1
2
3
2
1
1
1
of Lemma
cu-box-in-box_wf
1. I : Cname List
2. J : nameset(I) List
3. x : nameset(I)
4. d : ℕ2
5. box : I-face(c𝕌;I) List
6. (∀f1,f2∈box. face-compatible(c𝕌;I;f1;f2))
7. ¬(x ∈ J)
8. l_subset(Cname;J;I)
9. ∀y:nameset(J). ∀c:ℕ2. (∃f∈box. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
10. (∃f∈box. face-name(f) = <x, d> ∈ (nameset(I) × ℕ2))
11. (∀f∈box.¬(face-name(f) = <x, 1 - d> ∈ (nameset(I) × ℕ2)))
12. (∀f∈box.(fst(f) ∈ [x / J]))
13. (∀f1,f2∈box. ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
14. u : i:ℕ||box|| ⟶ cu-cube-family(cube(box[i]);I-[dimension(box[i])];1)
15. i : ℕ||box||
16. j : ℕ||box||
17. ¬(dimension(box[i]) = dimension(box[j]) ∈ Cname)
18. cu-cube-restriction(cube(box[j]);I-[dimension(box[j])];I-[dimension(box[j]); dimension(box[i])];
(dimension(box[i]):=direction(box[i]));1;u j)
= cu-cube-restriction(cube(box[j]);I-[dimension(box[j])];I-[dimension(box[j]); dimension(box[i])];
(dimension(box[i]):=direction(box[i]));1;u j)
∈ cu-cube-family(cube(box[j]);I-[dimension(box[j]); dimension(box[i])];(1 o (dimension(box[i]):=direction(box[i]))))
19. (box[i] ∈ box)
20. (box[j] ∈ box)
21. (box[j] = box[i] ∈ I-face(c𝕌;I)) ∨ face-compatible(c𝕌;I;box[j];box[i]) ∨ face-compatible(c𝕌;I;box[i];box[j])
⊢ cu-cube-family(cube(box[j]);I-[dimension(box[j]); dimension(box[i])];(1 o (dimension(box[i]):=direction(box[i]))))
= cu-cube-family(cube(box[i]);I-[dimension(box[i]); dimension(box[j])];(1 o (dimension(box[j]):=direction(box[j]))))
∈ Type
BY
{ TACTIC:D -1 }
1
1. I : Cname List
2. J : nameset(I) List
3. x : nameset(I)
4. d : ℕ2
5. box : I-face(c𝕌;I) List
6. (∀f1,f2∈box. face-compatible(c𝕌;I;f1;f2))
7. ¬(x ∈ J)
8. l_subset(Cname;J;I)
9. ∀y:nameset(J). ∀c:ℕ2. (∃f∈box. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
10. (∃f∈box. face-name(f) = <x, d> ∈ (nameset(I) × ℕ2))
11. (∀f∈box.¬(face-name(f) = <x, 1 - d> ∈ (nameset(I) × ℕ2)))
12. (∀f∈box.(fst(f) ∈ [x / J]))
13. (∀f1,f2∈box. ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
14. u : i:ℕ||box|| ⟶ cu-cube-family(cube(box[i]);I-[dimension(box[i])];1)
15. i : ℕ||box||
16. j : ℕ||box||
17. ¬(dimension(box[i]) = dimension(box[j]) ∈ Cname)
18. cu-cube-restriction(cube(box[j]);I-[dimension(box[j])];I-[dimension(box[j]); dimension(box[i])];
(dimension(box[i]):=direction(box[i]));1;u j)
= cu-cube-restriction(cube(box[j]);I-[dimension(box[j])];I-[dimension(box[j]); dimension(box[i])];
(dimension(box[i]):=direction(box[i]));1;u j)
∈ cu-cube-family(cube(box[j]);I-[dimension(box[j]); dimension(box[i])];(1 o (dimension(box[i]):=direction(box[i]))))
19. (box[i] ∈ box)
20. (box[j] ∈ box)
21. box[j] = box[i] ∈ I-face(c𝕌;I)
⊢ cu-cube-family(cube(box[j]);I-[dimension(box[j]); dimension(box[i])];(1 o (dimension(box[i]):=direction(box[i]))))
= cu-cube-family(cube(box[i]);I-[dimension(box[i]); dimension(box[j])];(1 o (dimension(box[j]):=direction(box[j]))))
∈ Type
2
1. I : Cname List
2. J : nameset(I) List
3. x : nameset(I)
4. d : ℕ2
5. box : I-face(c𝕌;I) List
6. (∀f1,f2∈box. face-compatible(c𝕌;I;f1;f2))
7. ¬(x ∈ J)
8. l_subset(Cname;J;I)
9. ∀y:nameset(J). ∀c:ℕ2. (∃f∈box. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
10. (∃f∈box. face-name(f) = <x, d> ∈ (nameset(I) × ℕ2))
11. (∀f∈box.¬(face-name(f) = <x, 1 - d> ∈ (nameset(I) × ℕ2)))
12. (∀f∈box.(fst(f) ∈ [x / J]))
13. (∀f1,f2∈box. ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
14. u : i:ℕ||box|| ⟶ cu-cube-family(cube(box[i]);I-[dimension(box[i])];1)
15. i : ℕ||box||
16. j : ℕ||box||
17. ¬(dimension(box[i]) = dimension(box[j]) ∈ Cname)
18. cu-cube-restriction(cube(box[j]);I-[dimension(box[j])];I-[dimension(box[j]); dimension(box[i])];
(dimension(box[i]):=direction(box[i]));1;u j)
= cu-cube-restriction(cube(box[j]);I-[dimension(box[j])];I-[dimension(box[j]); dimension(box[i])];
(dimension(box[i]):=direction(box[i]));1;u j)
∈ cu-cube-family(cube(box[j]);I-[dimension(box[j]); dimension(box[i])];(1 o (dimension(box[i]):=direction(box[i]))))
19. (box[i] ∈ box)
20. (box[j] ∈ box)
21. face-compatible(c𝕌;I;box[j];box[i]) ∨ face-compatible(c𝕌;I;box[i];box[j])
⊢ cu-cube-family(cube(box[j]);I-[dimension(box[j]); dimension(box[i])];(1 o (dimension(box[i]):=direction(box[i]))))
= cu-cube-family(cube(box[i]);I-[dimension(box[i]); dimension(box[j])];(1 o (dimension(box[j]):=direction(box[j]))))
∈ Type
Latex:
Latex:
1. I : Cname List
2. J : nameset(I) List
3. x : nameset(I)
4. d : \mBbbN{}2
5. box : I-face(c\mBbbU{};I) List
6. (\mforall{}f1,f2\mmember{}box. face-compatible(c\mBbbU{};I;f1;f2))
7. \mneg{}(x \mmember{} J)
8. l\_subset(Cname;J;I)
9. \mforall{}y:nameset(J). \mforall{}c:\mBbbN{}2. (\mexists{}f\mmember{}box. face-name(f) = <y, c>)
10. (\mexists{}f\mmember{}box. face-name(f) = <x, d>)
11. (\mforall{}f\mmember{}box.\mneg{}(face-name(f) = <x, 1 - d>))
12. (\mforall{}f\mmember{}box.(fst(f) \mmember{} [x / J]))
13. (\mforall{}f1,f2\mmember{}box. \mneg{}(face-name(f1) = face-name(f2)))
14. u : i:\mBbbN{}||box|| {}\mrightarrow{} cu-cube-family(cube(box[i]);I-[dimension(box[i])];1)
15. i : \mBbbN{}||box||
16. j : \mBbbN{}||box||
17. \mneg{}(dimension(box[i]) = dimension(box[j]))
18. cu-cube-restriction(cube(box[j]);I-[dimension(box[j])];I-[dimension(box[j]); dimension(box[i])];
(dimension(box[i]):=direction(box[i]));1;u j)
= cu-cube-restriction(cube(box[j]);I-[dimension(box[j])];I-[dimension(box[j]); dimension(box[i])];
(dimension(box[i]):=direction(box[i]));1;u j)
19. (box[i] \mmember{} box)
20. (box[j] \mmember{} box)
21. (box[j] = box[i]) \mvee{} face-compatible(c\mBbbU{};I;box[j];box[i]) \mvee{} face-compatible(c\mBbbU{};I;box[i];box[j])
\mvdash{} cu-cube-family(cube(box[j]);I-[dimension(box[j]);
dimension(box[i])];(1 o (dimension(box[i]):=direction(box[i]))))
= cu-cube-family(cube(box[i]);I-[dimension(box[i]);
dimension(box[j])];(1 o (dimension(box[j]):=direction(box[j]))))
By
Latex:
TACTIC:D -1
Home
Index