---

Step * of Lemma b_all-map2

∀[A,B:Type].
  ∀b:bag(A). ∀f:{a:A| a ↓∈ b}  ⟶ B. ∀P:B ⟶ ℙ.
    ((∀b:B. SqStable(P[b])) ⇒ (b_all(B;bag-map(f;b);x.P[x]) ⇐⇒ b_all(A;b;x.P[f x])))
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN RepeatFor 2 (D 0)
          THEN Try (Complete ((MemCD'
                               THEN Try (Complete (Auto))
                               THEN Using [`A',⌜{a:A| a ↓∈ b} ⌝] MemCD⋅
                               THEN Auto
                               THEN BLemma `bag-subtype`
                               THEN Auto)))) }

1
1. [A] : Type
2. [B] : Type
3. b : bag(A)
4. f : {a:A| a ↓∈ b}  ⟶ B
5. P : B ⟶ ℙ
6. ∀b:B. SqStable(P[b])
7. b_all(B;bag-map(f;b);x.P[x])
⊢ b_all(A;b;x.P[f x])

2
1. [A] : Type
2. [B] : Type
3. b : bag(A)
4. f : {a:A| a ↓∈ b}  ⟶ B
5. P : B ⟶ ℙ
6. ∀b:B. SqStable(P[b])
7. b_all(A;b;x.P[f x])
⊢ b_all(B;bag-map(f;b);x.P[x])

3
.....wf..... 
1. A : Type
2. B : Type
3. b : bag(A)
4. f : {a:A| a ↓∈ b}  ⟶ B
5. P : B ⟶ ℙ
6. ∀b:B. SqStable(P[b])
⊢ istype(b_all(A;b;x.P[f x]))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}b:bag(A).  \mforall{}f:\{a:A|  a  \mdownarrow{}\mmember{}  b\}    {}\mrightarrow{}  B.  \mforall{}P:B  {}\mrightarrow{}  \mBbbP{}.
        ((\mforall{}b:B.  SqStable(P[b]))  {}\mRightarrow{}  (b\_all(B;bag-map(f;b);x.P[x])  \mLeftarrow{}{}\mRightarrow{}  b\_all(A;b;x.P[f  x])))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  RepeatFor  2  (D  0)
                THEN  Try  (Complete  ((MemCD'
                                                          THEN  Try  (Complete  (Auto))
                                                          THEN  Using  [`A',\mkleeneopen{}\{a:A|  a  \mdownarrow{}\mmember{}  b\}  \mkleeneclose{}]  MemCD\mcdot{}
                                                          THEN  Auto
                                                          THEN  BLemma  `bag-subtype`
                                                          THEN  Auto))))

---

Home Index