---

Step * 2 of Lemma fpf-contains-union-join-left2


1. [A] : Type
2. [B] : A ─→ Type
3. eq : EqDecider(A)@i
4. f : a:A fp-> B[a] List@i
5. h : a:A fp-> B[a] List@i
6. g : a:A fp-> B[a] List@i
7. R : ∩a:A. ((B[a] List) ─→ B[a] ─→ 𝔹)@i
8. ∀x:A. ((↑x ∈ dom(h)) ⇒ ((↑x ∈ dom(f)) c∧ h(x) ⊆ f(x)))@i
9. x : A@i
10. ↑x ∈ dom(h)@i
11. (↑x ∈ dom(f)) c∧ h(x) ⊆ f(x)
12. ↑x ∈ dom(fpf-union-join(eq;R;f;g))
⊢ h(x) ⊆ fpf-union-join(eq;R;f;g)(x)
BY
{ (D -2
   THEN Thin (-1)
   THEN RepeatFor 3 (ParallelLast)
   THEN RWO "fpf-union-join-ap" 0
   THEN Auto
   THEN (InstLemma `fpf-union-contains` [⌈A⌉;⌈B⌉;⌈eq⌉;⌈f⌉;⌈g⌉;⌈x⌉;⌈R⌉]⋅ THENA Auto)
   THEN Unfold `l_contains` (-1)
   THEN (RWO "l_all_iff" (-1) THENA Auto)
   THEN BHyp (-1)
   THEN Auto) }

1
1. [A] : Type
2. [B] : A ─→ Type
3. eq : EqDecider(A)@i
4. f : a:A fp-> B[a] List@i
5. h : a:A fp-> B[a] List@i
6. g : a:A fp-> B[a] List@i
7. R : ∩a:A. ((B[a] List) ─→ B[a] ─→ 𝔹)@i
8. ∀x:A. ((↑x ∈ dom(h)) ⇒ ((↑x ∈ dom(f)) c∧ h(x) ⊆ f(x)))@i
9. x : A@i
10. ↑x ∈ dom(h)@i
11. ↑x ∈ dom(f)
12. ∀i:ℕ||h(x)||. (h(x)[i] ∈ f(x))
13. i : ℕ||h(x)||@i
14. (h(x)[i] ∈ f(x))
15. ∀a:B[x]. ((a ∈ f(x)?[]) ⇒ (a ∈ fpf-union(f;g;eq;R;x)))
⊢ (h(x)[i] ∈ f(x)?[])

---

Latex:



1.  [A]  :  Type
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  eq  :  EqDecider(A)@i
4.  f  :  a:A  fp->  B[a]  List@i
5.  h  :  a:A  fp->  B[a]  List@i
6.  g  :  a:A  fp->  B[a]  List@i
7.  R  :  \mcap{}a:A.  ((B[a]  List)  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbB{})@i
8.  \mforall{}x:A.  ((\muparrow{}x  \mmember{}  dom(h))  {}\mRightarrow{}  ((\muparrow{}x  \mmember{}  dom(f))  c\mwedge{}  h(x)  \msubseteq{}  f(x)))@i
9.  x  :  A@i
10.  \muparrow{}x  \mmember{}  dom(h)@i
11.  (\muparrow{}x  \mmember{}  dom(f))  c\mwedge{}  h(x)  \msubseteq{}  f(x)
12.  \muparrow{}x  \mmember{}  dom(fpf-union-join(eq;R;f;g))
\mvdash{}  h(x)  \msubseteq{}  fpf-union-join(eq;R;f;g)(x)


By

(D  -2
  THEN  Thin  (-1)
  THEN  RepeatFor  3  (ParallelLast)
  THEN  RWO  "fpf-union-join-ap"  0
  THEN  Auto
  THEN  (InstLemma  `fpf-union-contains`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `l\_contains`  (-1)
  THEN  (RWO  "l\_all\_iff"  (-1)  THENA  Auto)
  THEN  BHyp  (-1)
  THEN  Auto)

---

Home Index