---

Step * of Lemma concat-lifting-2-strict

∀[f:Top]. ∀[b:bag(Top)].  ((f@ {} b ~ {}) ∧ (f@ b {} ~ {}))
BY
{ (Auto
   THEN (RepUR ``concat-lifting-2 concat-lifting concat-lifting2 concat-lifting-list`` 0
         THEN (InstLemma `lifting-gen-strict` [⌜2⌝;⌜f⌝]⋅ THENA Auto)
         THEN RepUR ``lifting-gen lifting-gen-rev`` -1
         THEN RWO "-1" 0
         THEN Auto
         THEN Reduce 0
         THEN Auto
         THEN Try ((RepUR ``bag-union empty-bag`` 0 THEN Trivial)))⋅
   ) }

1
1. f : Top
2. b : bag(Top)
3. ∀[a:k:ℕ2 ⟶ bag(Top)]. lifting-gen-list-rev(2;a) 0 f ~ {} supposing ∃k:ℕ2. (↑bag-null(a k))
⊢ ∃k:ℕ2. (↑bag-null([{}; b][k]))

2
1. f : Top
2. b : bag(Top)
3. f@ {} b ~ {}
4. ∀[a:k:ℕ2 ⟶ bag(Top)]. lifting-gen-list-rev(2;a) 0 f ~ {} supposing ∃k:ℕ2. (↑bag-null(a k))
⊢ ∃k:ℕ2. (↑bag-null([b; {}][k]))

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[b:bag(Top)].    ((f@  \{\}  b  \msim{}  \{\})  \mwedge{}  (f@  b  \{\}  \msim{}  \{\}))


By

---

Latex:
(Auto
  THEN  (RepUR  ``concat-lifting-2  concat-lifting  concat-lifting2  concat-lifting-list``  0
              THEN  (InstLemma  `lifting-gen-strict`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  RepUR  ``lifting-gen  lifting-gen-rev``  -1
              THEN  RWO  "-1"  0
              THEN  Auto
              THEN  Reduce  0
              THEN  Auto
              THEN  Try  ((RepUR  ``bag-union  empty-bag``  0  THEN  Trivial)))\mcdot{}
  )

---

Home Index