Step * 1 1 1 1 1 1 of Lemma class-output-support-no-repeats


1. Info Type
2. es EO+(Info)
3. List
4. no_repeats(E;L)
5. ∀e1,e2:E.  (e1 ↓∈  e2 ↓∈  (e1 <loc e2)))
6. : ℕ||L||@i
7. {j:ℕ||L||| ¬(i j ∈ ℤ)} @i
8. : ℕ||≤loc(L[i])||@i
9. ≤loc(L[i])[k] ≤loc L[j] @i
10. ≤loc(L[i])[k] ≤loc L[i] 
11. loc(L[i]) loc(L[j]) ∈ Id ⇐⇒ (L[i] <loc L[j]) ∨ (L[i] L[j] ∈ E) ∨ (L[j] <loc L[i])
⊢ False
BY
(DVar `j'
   THEN (D (-1)
         THEN Thin (-1)
         THEN (D (-1) THENA Auto)
         THEN SplitOrHyps
         THEN MoveToConcl (-1)
         THEN Fold `not` 0
         THEN BackThruSomeHyp'
         THEN RWW "bag-member-list" 0
         THEN Auto)⋅
   }


Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
3.  L  :  E  List
4.  no\_repeats(E;L)
5.  \mforall{}e1,e2:E.    (e1  \mdownarrow{}\mmember{}  L  {}\mRightarrow{}  e2  \mdownarrow{}\mmember{}  L  {}\mRightarrow{}  (\mneg{}(e1  <loc  e2)))
6.  i  :  \mBbbN{}||L||@i
7.  j  :  \{j:\mBbbN{}||L|||  \mneg{}(i  =  j)\}  @i
8.  k  :  \mBbbN{}||\mleq{}loc(L[i])||@i
9.  \mleq{}loc(L[i])[k]  \mleq{}loc  L[j]  @i
10.  \mleq{}loc(L[i])[k]  \mleq{}loc  L[i] 
11.  loc(L[i])  =  loc(L[j])  \mLeftarrow{}{}\mRightarrow{}  (L[i]  <loc  L[j])  \mvee{}  (L[i]  =  L[j])  \mvee{}  (L[j]  <loc  L[i])
\mvdash{}  False


By

(DVar  `j'
  THEN  (D  (-1)
              THEN  Thin  (-1)
              THEN  (D  (-1)  THENA  Auto)
              THEN  SplitOrHyps
              THEN  MoveToConcl  (-1)
              THEN  Fold  `not`  0
              THEN  BackThruSomeHyp'
              THEN  RWW  "bag-member-list"  0
              THEN  Auto)\mcdot{}
  )




Home Index