---

Step * of Lemma concat-lifting-strict

∀[n:ℕ]. ∀[bags:k:ℕn ⟶ bag(Top)]. ∀[f:Top].  concat-lifting(n;f;bags) ~ {} supposing ∃k:ℕn. ((bags k) = {} ∈ bag(Top))
BY
{ (Auto
   THEN ExRepD
   THEN RepUR ``concat-lifting concat-lifting-list`` 0⋅
   THEN Assert ⌜∀m,i:ℕ.  ((i ≤ k) ⇒ i < n ⇒ ((k - i) ≤ m) ⇒ (∀f:Top. (lifting-gen-list-rev(n;bags) i f ~ {})))⌝⋅
   THEN Try ((InstHyp [⌜k⌝;⌜0⌝;⌜f⌝] (-1)⋅ THEN Auto THEN ExRepD THEN HypSubst' (-1) 0 THEN Reduce 0 THEN Auto)⋅)
   THEN (InductionOnNat
         THEN Auto
         THEN RecUnfold `lifting-gen-list-rev` 0
         THEN Reduce 0
         THEN AutoSplit
         THEN (Decide i = k ∈ ℤ THENA Auto)
         THEN Try (Complete ((Subst' bags i ~ {} 0
                              THEN Reduce 0
                              THEN Auto
                              THEN Try ((BLemma `equal-empty-bag` THEN Auto)))⋅))
         THEN Auto'
         THEN RepUR ``bag-combine`` 0
         THEN Subst ⌜λx.(lifting-gen-list-rev(n;bags) (i + 1) (f1 x)) ~ λx.{}⌝ 0⋅
         THEN Try ((EqCD THEN BackThruSomeHyp THEN Auto')))⋅) }

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

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[bags:k:\mBbbN{}n  {}\mrightarrow{}  bag(Top)].  \mforall{}[f:Top].
    concat-lifting(n;f;bags)  \msim{}  \{\}  supposing  \mexists{}k:\mBbbN{}n.  ((bags  k)  =  \{\})


By

---

Latex:
(Auto
  THEN  ExRepD
  THEN  RepUR  ``concat-lifting  concat-lifting-list``  0\mcdot{}
  THEN  Assert  \mkleeneopen{}\mforall{}m,i:\mBbbN{}.
                                ((i  \mleq{}  k)
                                {}\mRightarrow{}  i  <  n
                                {}\mRightarrow{}  ((k  -  i)  \mleq{}  m)
                                {}\mRightarrow{}  (\mforall{}f:Top.  (lifting-gen-list-rev(n;bags)  i  f  \msim{}  \{\})))\mkleeneclose{}\mcdot{}
  THEN  Try  ((InstHyp  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  (-1)\mcdot{}
                        THEN  Auto
                        THEN  ExRepD
                        THEN  HypSubst'  (-1)  0
                        THEN  Reduce  0
                        THEN  Auto)\mcdot{})
  THEN  (InductionOnNat
              THEN  Auto
              THEN  RecUnfold  `lifting-gen-list-rev`  0
              THEN  Reduce  0
              THEN  AutoSplit
              THEN  (Decide  i  =  k  THENA  Auto)
              THEN  Try  (Complete  ((Subst'  bags  i  \msim{}  \{\}  0
                                                        THEN  Reduce  0
                                                        THEN  Auto
                                                        THEN  Try  ((BLemma  `equal-empty-bag`  THEN  Auto)))\mcdot{}))
              THEN  Auto'
              THEN  RepUR  ``bag-combine``  0
              THEN  Subst  \mkleeneopen{}\mlambda{}x.(lifting-gen-list-rev(n;bags)  (i  +  1)  (f1  x))  \msim{}  \mlambda{}x.\{\}\mkleeneclose{}  0\mcdot{}
              THEN  Try  ((EqCD  THEN  BackThruSomeHyp  THEN  Auto')))\mcdot{})

---

Home Index