---

Step * of Lemma lifting-gen-strict

∀[n:ℕ]. ∀[f:Top]. ∀[a:k:ℕn ⟶ bag(Top)].  lifting-gen(n;f) a ~ {} supposing ∃k:ℕn. (↑bag-null(a k))
BY
{ (RepUR ``lifting-gen lifting-gen-rev`` 0
   THEN Assert ⌜∀k,m:ℕ.
                  ∀[n:ℕ]
                    (((n - m) ≤ k)
                    ⇒ (∀[f:Top]. ∀[a:k:ℕn ⟶ bag(Top)].
                          lifting-gen-list-rev(n;a) m f ~ {} supposing ∃i:{m..n-}. (↑bag-null(a i))))⌝⋅
   THEN Try ((Auto THEN InstHyp [⌜n⌝;⌜0⌝;⌜n⌝] 1⋅ THEN Auto))
   THEN InductionOnNat
   THEN Auto
   THEN D -1
   THEN Auto'
   THEN RecUnfold `lifting-gen-list-rev` 0
   THEN Reduce 0
   THEN OldAutoSplit
   THEN (InstHyp [⌜m + 1⌝;⌜n⌝] 3⋅ THENA Auto')
   THEN (Decide ⌜i = m ∈ ℤ⌝⋅ THENA Auto)
   THEN Try (Complete ((RWW "-2 bag-combine-empty-right" 0 THEN Auto THEN With ⌜i⌝ (D 0)⋅ THEN Auto)))
   THEN Subst ⌜a m ~ {}⌝ 0⋅
   THEN RWW "bag-combine-empty-left" 0
   THEN Auto) }

1
.....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 ~ {}

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:Top].  \mforall{}[a:k:\mBbbN{}n  {}\mrightarrow{}  bag(Top)].    lifting-gen(n;f)  a  \msim{}  \{\}  supposing  \mexists{}k:\mBbbN{}n.  (\muparrow{}bag-null(a  k))


By

---

Latex:
(RepUR  ``lifting-gen  lifting-gen-rev``  0
  THEN  Assert  \mkleeneopen{}\mforall{}k,m:\mBbbN{}.
                                \mforall{}[n:\mBbbN{}]
                                    (((n  -  m)  \mleq{}  k)
                                    {}\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))))\mkleeneclose{}
  \mcdot{}
  THEN  Try  ((Auto  THEN  InstHyp  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  1\mcdot{}  THEN  Auto))
  THEN  InductionOnNat
  THEN  Auto
  THEN  D  -1
  THEN  Auto'
  THEN  RecUnfold  `lifting-gen-list-rev`  0
  THEN  Reduce  0
  THEN  OldAutoSplit
  THEN  (InstHyp  [\mkleeneopen{}m  +  1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  3\mcdot{}  THENA  Auto')
  THEN  (Decide  \mkleeneopen{}i  =  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (Complete  ((RWW  "-2  bag-combine-empty-right"  0  THEN  Auto  THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)))
  THEN  Subst  \mkleeneopen{}a  m  \msim{}  \{\}\mkleeneclose{}  0\mcdot{}
  THEN  RWW  "bag-combine-empty-left"  0
  THEN  Auto)

---

Home Index