---

Step * of Lemma fpf-sub-join

∀[A:Type]. ∀[B:A ─→ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a]].  {f ⊆ f ⊕ g ∧ g ⊆ f ⊕ g} supposing f || g
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN Try ((Using [`B2',⌈B⌉] (BLemma `fpf-sub-join-left`)⋅ THEN Auto))
   THEN Try ((BLemma `fpf-sub-join-right` THEN Auto))) }

---

Latex:


\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f,g:a:A  fp->  B[a]].
    \{f  \msubseteq{}  f  \moplus{}  g  \mwedge{}  g  \msubseteq{}  f  \moplus{}  g\}  supposing  f  ||  g


By

(Unfold  `guard`  0
  THEN  Auto
  THEN  Try  ((Using  [`B2',\mkleeneopen{}B\mkleeneclose{}]  (BLemma  `fpf-sub-join-left`)\mcdot{}  THEN  Auto))
  THEN  Try  ((BLemma  `fpf-sub-join-right`  THEN  Auto)))

---

Home Index