---

Step * of Lemma concat-lifting-3-strict

∀[f:Top]. ∀[b:bag(Top)].
  ∀b':bag(Top)
    ((concat-lifting-3(f) {} b b' ~ {}) ∧ (concat-lifting-3(f) b {} b' ~ {}) ∧ (concat-lifting-3(f) b b' {} ~ {}))
BY
{ (Auto
   THEN (RepUR ``concat-lifting-3 concat-lifting concat-lifting-list`` 0
         THEN (InstLemma `lifting-gen-strict` [⌜3⌝;⌜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. b' : bag(Top)@i
4. ∀[a:k:ℕ3 ⟶ bag(Top)]. lifting-gen-list-rev(3;a) 0 f ~ {} supposing ∃k:ℕ3. (↑bag-null(a k))
⊢ ∃k:ℕ3. (↑bag-null([{}; b; b'][k]))

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

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

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[b:bag(Top)].
    \mforall{}b':bag(Top)
        ((concat-lifting-3(f)  \{\}  b  b'  \msim{}  \{\})
        \mwedge{}  (concat-lifting-3(f)  b  \{\}  b'  \msim{}  \{\})
        \mwedge{}  (concat-lifting-3(f)  b  b'  \{\}  \msim{}  \{\}))


By

---

Latex:
(Auto
  THEN  (RepUR  ``concat-lifting-3  concat-lifting  concat-lifting-list``  0
              THEN  (InstLemma  `lifting-gen-strict`  [\mkleeneopen{}3\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