---

Step * of Lemma lifting-3-strict

∀[f:Top]. ∀[b:bag(Top)].
  ∀b':bag(Top). ((lifting-3(f) {} b b' ~ {}) ∧ (lifting-3(f) b {} b' ~ {}) ∧ (lifting-3(f) b b' {} ~ {}))
BY
{ (Auto
   THEN (InstLemma `lifting-gen-strict` [⌜3⌝;⌜f⌝]⋅ THENA Auto)
   THEN RepUR ``lifting-3 lifting3`` 0
   THEN RepUR ``lifting-gen`` -1
   THEN BHyp -1 
   THEN Auto
   THEN Reduce 0
   THEN Auto) }

1
1. f : Top
2. b : bag(Top)
3. b' : bag(Top)@i
4. ∀[a:k:ℕ3 ⟶ bag(Top)]. lifting-gen-rev(3;f;a) ~ {} 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. lifting-3(f) {} b b' ~ {}
5. ∀[a:k:ℕ3 ⟶ bag(Top)]. lifting-gen-rev(3;f;a) ~ {} 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. lifting-3(f) {} b b' ~ {}
5. lifting-3(f) b {} b' ~ {}
6. ∀[a:k:ℕ3 ⟶ bag(Top)]. lifting-gen-rev(3;f;a) ~ {} 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)
        ((lifting-3(f)  \{\}  b  b'  \msim{}  \{\})  \mwedge{}  (lifting-3(f)  b  \{\}  b'  \msim{}  \{\})  \mwedge{}  (lifting-3(f)  b  b'  \{\}  \msim{}  \{\}))


By

---

Latex:
(Auto
  THEN  (InstLemma  `lifting-gen-strict`  [\mkleeneopen{}3\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``lifting-3  lifting3``  0
  THEN  RepUR  ``lifting-gen``  -1
  THEN  BHyp  -1 
  THEN  Auto
  THEN  Reduce  0
  THEN  Auto)

---

Home Index