Step * 1 of Lemma length-open_box-ge-3


1. [X] CubicalSet
2. [I] Cname List
3. nameset(I) List
4. [x] nameset(I)
5. [i] : ℕ2
6. [box] open_box(X;I;J;x;i)
7. 3 < (||remove-repeats(CnameDeq;J)|| 2)
⊢ (∃j1∈J. (∃j2∈J. ¬(j1 j2 ∈ Cname)))
BY
((Assert CnameDeq ∈ EqDecider(nameset(I)) BY
          (Unfold `nameset` THEN Auto))
   THEN (Assert 1 < ||remove-repeats(CnameDeq;J)|| BY
               Auto')
   THEN SupposeNot
   THEN Assert ⌜False⌝⋅
   THEN Auto) }

1
1. CubicalSet
2. Cname List
3. nameset(I) List
4. nameset(I)
5. : ℕ2
6. box open_box(X;I;J;x;i)
7. 3 < (||remove-repeats(CnameDeq;J)|| 2)
8. CnameDeq ∈ EqDecider(nameset(I))
9. 1 < ||remove-repeats(CnameDeq;J)||
10. ¬(∃j1∈J. (∃j2∈J. ¬(j1 j2 ∈ Cname)))
⊢ False


Latex:


Latex:

1.  [X]  :  CubicalSet
2.  [I]  :  Cname  List
3.  J  :  nameset(I)  List
4.  [x]  :  nameset(I)
5.  [i]  :  \mBbbN{}2
6.  [box]  :  open\_box(X;I;J;x;i)
7.  3  <  1  +  (||remove-repeats(CnameDeq;J)||  *  2)
\mvdash{}  (\mexists{}j1\mmember{}J.  (\mexists{}j2\mmember{}J.  \mneg{}(j1  =  j2)))


By


Latex:
((Assert  CnameDeq  \mmember{}  EqDecider(nameset(I))  BY
                (Unfold  `nameset`  0  THEN  Auto))
  THEN  (Assert  1  <  ||remove-repeats(CnameDeq;J)||  BY
                          Auto')
  THEN  SupposeNot
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto)




Home Index