---

Step * 1 of Lemma concat-lifting-strict


1. n : ℕ
2. bags : k:ℕn ⟶ bag(Top)
3. f : Top
4. k : ℕn
5. (bags k) = {} ∈ bag(Top)
6. m : ℤ
7. 0 < m
8. ∀i:ℕ. ((i ≤ k) ⇒ i < n ⇒ ((k - i) ≤ (m - 1)) ⇒ (∀f:Top. (lifting-gen-list-rev(n;bags) i f ~ {})))
9. i : ℕ
10. n ≠ i
11. i ≤ k
12. i < n
13. (k - i) ≤ m
14. f1 : Top
15. ¬(i = k ∈ ℤ)
⊢ bag-union(bag-map(λx.{};bags i)) ~ {}
BY
{ ((GenConclAtAddrType ⌜Top List⌝ [1;1;2]⋅ THENA Auto)
   THEN All Thin
   THEN RepUR ``bag-map bag-union empty-bag concat`` 0
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  bags  :  k:\mBbbN{}n  {}\mrightarrow{}  bag(Top)
3.  f  :  Top
4.  k  :  \mBbbN{}n
5.  (bags  k)  =  \{\}
6.  m  :  \mBbbZ{}
7.  0  <  m
8.  \mforall{}i:\mBbbN{}
          ((i  \mleq{}  k)  {}\mRightarrow{}  i  <  n  {}\mRightarrow{}  ((k  -  i)  \mleq{}  (m  -  1))  {}\mRightarrow{}  (\mforall{}f:Top.  (lifting-gen-list-rev(n;bags)  i  f  \msim{}  \{\})))
9.  i  :  \mBbbN{}
10.  n  \mneq{}  i
11.  i  \mleq{}  k
12.  i  <  n
13.  (k  -  i)  \mleq{}  m
14.  f1  :  Top
15.  \mneg{}(i  =  k)
\mvdash{}  bag-union(bag-map(\mlambda{}x.\{\};bags  i))  \msim{}  \{\}


By

---

Latex:
((GenConclAtAddrType  \mkleeneopen{}Top  List\mkleeneclose{}  [1;1;2]\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  RepUR  ``bag-map  bag-union  empty-bag  concat``  0
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index