---

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


1. [A] : Type
2. [V] : Type
3. [B] : A ─→ Type
4. ∀a:A. (B[a] ⊆r V)
5. eq : EqDecider(A)@i
6. f : a:A fp-> B[a] List@i
7. h : a:A fp-> B[a] List@i
8. g : a:A fp-> B[a] List@i
9. R : (V List) ─→ V ─→ 𝔹@i
10. fpf-single-valued(A;eq;x.B[x];V;g)
11. fpf-union-compatible(A;V;x.B[x];eq;R;f;g)@i
12. ∀x:A. ((↑x ∈ dom(h)) ⇒ ((↑x ∈ dom(g)) c∧ h(x) ⊆ g(x)))@i
13. x : A@i
14. ↑x ∈ dom(h)@i
15. (↑x ∈ dom(g)) c∧ h(x) ⊆ g(x)
16. ↑x ∈ dom(fpf-union-join(eq;R;f;g))
⊢ h(x) ⊆ fpf-union-join(eq;R;f;g)(x)
BY
{ (D -2
   THEN (InstLemma `fpf-union-contains2` [⌈A⌉;⌈V⌉;⌈B⌉;⌈eq⌉;⌈f⌉;⌈g⌉;⌈x⌉;⌈R⌉]⋅ THENA Auto)
   THEN RepeatFor 3 (ParallelOp (-3))
   THEN (RWO "fpf-union-join-ap" 0⋅ THENA Auto)
   THEN Unfold `l_contains` (-3)
   THEN RWO "l_all_iff" (-3)
   THEN Auto
   THEN Try ((BackThruSomeHyp THEN Unfold `fpf-cap` 0 THEN SplitOnConclITE THEN Auto))
   THEN (All (Unfold `so_apply`) THEN DoSubsume THEN Auto)⋅) }

---

Latex:



1.  [A]  :  Type
2.  [V]  :  Type
3.  [B]  :  A  {}\mrightarrow{}  Type
4.  \mforall{}a:A.  (B[a]  \msubseteq{}r  V)
5.  eq  :  EqDecider(A)@i
6.  f  :  a:A  fp->  B[a]  List@i
7.  h  :  a:A  fp->  B[a]  List@i
8.  g  :  a:A  fp->  B[a]  List@i
9.  R  :  (V  List)  {}\mrightarrow{}  V  {}\mrightarrow{}  \mBbbB{}@i
10.  fpf-single-valued(A;eq;x.B[x];V;g)
11.  fpf-union-compatible(A;V;x.B[x];eq;R;f;g)@i
12.  \mforall{}x:A.  ((\muparrow{}x  \mmember{}  dom(h))  {}\mRightarrow{}  ((\muparrow{}x  \mmember{}  dom(g))  c\mwedge{}  h(x)  \msubseteq{}  g(x)))@i
13.  x  :  A@i
14.  \muparrow{}x  \mmember{}  dom(h)@i
15.  (\muparrow{}x  \mmember{}  dom(g))  c\mwedge{}  h(x)  \msubseteq{}  g(x)
16.  \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  (InstLemma  `fpf-union-contains2`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  (ParallelOp  (-3))
  THEN  (RWO  "fpf-union-join-ap"  0\mcdot{}  THENA  Auto)
  THEN  Unfold  `l\_contains`  (-3)
  THEN  RWO  "l\_all\_iff"  (-3)
  THEN  Auto
  THEN  Try  ((BackThruSomeHyp  THEN  Unfold  `fpf-cap`  0  THEN  SplitOnConclITE  THEN  Auto))
  THEN  (All  (Unfold  `so\_apply`)  THEN  DoSubsume  THEN  Auto)\mcdot{})

---

Home Index