---

Step * 1 1 of Lemma no_repeats-rat-cube-faces


1. k : ℕ
2. c : ℚCube(k)
⊢ ∀l1,l2:ℕk.
    ((l1 ∈ filter(λj.(dim(c j) =z 1);upto(k)))
    ⇒ (l2 ∈ filter(λj.(dim(c j) =z 1);upto(k)))
    ⇒ (¬(l1 = l2 ∈ ℕk))
    ⇒ l_disjoint(ℚCube(k);(λj.[lower-rc-face(c;j); upper-rc-face(c;j)]) 
                           l1;(λj.[lower-rc-face(c;j); upper-rc-face(c;j)]) l2))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN RepeatFor 2 (((D 0 THENA Auto) THEN GenListD (-1) THEN D -1 THEN (RW  assert_pushdownC (-1) THENA Auto)))
   THEN (Auto THEN Reduce 0)
   THEN (RWW "l_disjoint_cons" 0 THENA Auto)
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN GenListD (-1)
   THEN D -1) }

1
1. k : ℕ
2. c : ℚCube(k)
3. l1 : ℕk
4. l2 : ℕk
5. (l1 ∈ upto(k))
6. dim(c l1) = 1 ∈ ℤ
7. (l2 ∈ upto(k))
8. dim(c l2) = 1 ∈ ℤ
9. ¬(l1 = l2 ∈ ℕk)
10. lower-rc-face(c;l2) = lower-rc-face(c;l1) ∈ ℚCube(k)
⊢ False

2
1. k : ℕ
2. c : ℚCube(k)
3. l1 : ℕk
4. l2 : ℕk
5. (l1 ∈ upto(k))
6. dim(c l1) = 1 ∈ ℤ
7. (l2 ∈ upto(k))
8. dim(c l2) = 1 ∈ ℤ
9. ¬(l1 = l2 ∈ ℕk)
10. (lower-rc-face(c;l2) ∈ [upper-rc-face(c;l1)])
⊢ False

3
1. k : ℕ
2. c : ℚCube(k)
3. l1 : ℕk
4. l2 : ℕk
5. (l1 ∈ upto(k))
6. dim(c l1) = 1 ∈ ℤ
7. (l2 ∈ upto(k))
8. dim(c l2) = 1 ∈ ℤ
9. ¬(l1 = l2 ∈ ℕk)
10. ¬(lower-rc-face(c;l2) ∈ [lower-rc-face(c;l1); upper-rc-face(c;l1)])
11. upper-rc-face(c;l2) = lower-rc-face(c;l1) ∈ ℚCube(k)
⊢ False

4
1. k : ℕ
2. c : ℚCube(k)
3. l1 : ℕk
4. l2 : ℕk
5. (l1 ∈ upto(k))
6. dim(c l1) = 1 ∈ ℤ
7. (l2 ∈ upto(k))
8. dim(c l2) = 1 ∈ ℤ
9. ¬(l1 = l2 ∈ ℕk)
10. ¬(lower-rc-face(c;l2) ∈ [lower-rc-face(c;l1); upper-rc-face(c;l1)])
11. (upper-rc-face(c;l2) ∈ [upper-rc-face(c;l1)])
⊢ False

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  c  :  \mBbbQ{}Cube(k)
\mvdash{}  \mforall{}l1,l2:\mBbbN{}k.
        ((l1  \mmember{}  filter(\mlambda{}j.(dim(c  j)  =\msubz{}  1);upto(k)))
        {}\mRightarrow{}  (l2  \mmember{}  filter(\mlambda{}j.(dim(c  j)  =\msubz{}  1);upto(k)))
        {}\mRightarrow{}  (\mneg{}(l1  =  l2))
        {}\mRightarrow{}  l\_disjoint(\mBbbQ{}Cube(k);(\mlambda{}j.[lower-rc-face(c;j);  upper-rc-face(c;j)]) 
                                                      l1;(\mlambda{}j.[lower-rc-face(c;j);  upper-rc-face(c;j)])  l2))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RepeatFor  2  (((D  0  THENA  Auto)
                                        THEN  GenListD  (-1)
                                        THEN  D  -1
                                        THEN  (RW    assert\_pushdownC  (-1)  THENA  Auto)))
  THEN  (Auto  THEN  Reduce  0)
  THEN  (RWW  "l\_disjoint\_cons"  0  THENA  Auto)
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  GenListD  (-1)
  THEN  D  -1)

---

Home Index