---

Step * 1 of Lemma lifting-gen-strict

.....equality..... 
1. k : ℤ
2. 0 < k
3. ∀m:ℕ
     ∀[n:ℕ]
       (((n - m) ≤ (k - 1))
       ⇒ (∀[f:Top]. ∀[a:k:ℕn ⟶ bag(Top)].  lifting-gen-list-rev(n;a) m f ~ {} supposing ∃i:{m..n-}. (↑bag-null(a i))))
4. m : ℕ
5. n : ℕ
6. (n - m) ≤ k
7. f : Top
8. a : k:ℕn ⟶ bag(Top)
9. i : {m..n-}
10. ↑bag-null(a i)
11. ¬(n = m ∈ ℤ)
12. ∀[f:Top]. ∀[a:k:ℕn ⟶ bag(Top)].
      lifting-gen-list-rev(n;a) (m + 1) f ~ {} supposing ∃i:{m + 1..n-}. (↑bag-null(a i))
13. i = m ∈ ℤ
⊢ a m ~ {}
BY
{ ((RWO  "assert-bag-null" (-4) THEN Auto) THEN BLemma `equal-empty-bag` THEN Auto)⋅ }

---

Latex:

---

Latex:
.....equality..... 
1.  k  :  \mBbbZ{}
2.  0  <  k
3.  \mforall{}m:\mBbbN{}
          \mforall{}[n:\mBbbN{}]
              (((n  -  m)  \mleq{}  (k  -  1))
              {}\mRightarrow{}  (\mforall{}[f:Top].  \mforall{}[a:k:\mBbbN{}n  {}\mrightarrow{}  bag(Top)].
                          lifting-gen-list-rev(n;a)  m  f  \msim{}  \{\}  supposing  \mexists{}i:\{m..n\msupminus{}\}.  (\muparrow{}bag-null(a  i))))
4.  m  :  \mBbbN{}
5.  n  :  \mBbbN{}
6.  (n  -  m)  \mleq{}  k
7.  f  :  Top
8.  a  :  k:\mBbbN{}n  {}\mrightarrow{}  bag(Top)
9.  i  :  \{m..n\msupminus{}\}
10.  \muparrow{}bag-null(a  i)
11.  \mneg{}(n  =  m)
12.  \mforall{}[f:Top].  \mforall{}[a:k:\mBbbN{}n  {}\mrightarrow{}  bag(Top)].
            lifting-gen-list-rev(n;a)  (m  +  1)  f  \msim{}  \{\}  supposing  \mexists{}i:\{m  +  1..n\msupminus{}\}.  (\muparrow{}bag-null(a  i))
13.  i  =  m
\mvdash{}  a  m  \msim{}  \{\}


By

---

Latex:
((RWO    "assert-bag-null"  (-4)  THEN  Auto)  THEN  BLemma  `equal-empty-bag`  THEN  Auto)\mcdot{}

---

Home Index