---

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


1. Info : Type
2. es : EO+(Info)
3. L : E List
4. no_repeats(E;L)
5. ∀e1,e2:E.  (e1 ↓∈ L ⇒ e2 ↓∈ L ⇒ (¬(e1 <loc e2)))
6. concat(map(λe.≤loc(e);L)) = concat(map(λe.≤loc(e);L)) ∈ bag(E)
⊢ no_repeats(E;concat(map(λe.≤loc(e);L)))
BY
{ (RWO "no_repeats_concat" 0
   THEN Auto
   THEN (All (RWW "length-map-sq"))
   THEN Auto
   THEN (RWO "select-map" 0 THENA Auto)
   THEN Reduce 0
   THEN Try (Complete ((GenConclAtAddr [2;1] THEN Auto)))) }

1
1. Info : Type
2. es : EO+(Info)
3. L : E List
4. no_repeats(E;L)
5. ∀e1,e2:E.  (e1 ↓∈ L ⇒ e2 ↓∈ L ⇒ (¬(e1 <loc e2)))
6. concat(map(λe.≤loc(e);L)) = concat(map(λe.≤loc(e);L)) ∈ bag(E)
7. i : ℕ||L||@i
8. no_repeats(E;map(λe.≤loc(e);L)[i])
9. j : {j:ℕ||L||| ¬(i = j ∈ ℤ)} @i
10. k : ℕ||map(λe.≤loc(e);L)[i]||@i
⊢ ¬(≤loc(L[i])[k] ∈ ≤loc(L[j]))

---

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.  concat(map(\mlambda{}e.\mleq{}loc(e);L))  =  concat(map(\mlambda{}e.\mleq{}loc(e);L))
\mvdash{}  no\_repeats(E;concat(map(\mlambda{}e.\mleq{}loc(e);L)))


By

(RWO  "no\_repeats\_concat"  0
  THEN  Auto
  THEN  (All  (RWW  "length-map-sq"))
  THEN  Auto
  THEN  (RWO  "select-map"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Try  (Complete  ((GenConclAtAddr  [2;1]  THEN  Auto))))

---

Home Index