---

Step * of Lemma fpf-join-compatible-left

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B,C,D,E,F,G:A ─→ Type]. ∀[f:a:A fp-> B[a]]. ∀[g:a:A fp-> C[a]]. ∀[h:a:A fp-> D[a]].
  ({(f ⊕ g || h) supposing (g || h and f || h)}) supposing 
     ((∀a:A. (E[a] ⊆r G[a])) and 
     (∀a:A. (F[a] ⊆r G[a])) and 
     (∀a:A. (D[a] ⊆r F[a])) and 
     (∀a:A. (D[a] ⊆r E[a])) and 
     (∀a:A. (C[a] ⊆r F[a])) and 
     (∀a:A. (B[a] ⊆r E[a])))
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN (All (Unfold `fpf-compatible`))
   THEN Auto
   THEN (RWO "fpf-join-dom2" (-2))
   THEN Auto
   THEN ((D (-2))
         THEN Repeat ((Unfolds ``fpf-cap fpf-join fpf-ap`` 0 THEN Reduce 0))
         THEN SplitOnConclITE
         THEN Auto
         THEN AllHyps h.((InstHyp [⌈x⌉] h)⋅ THENA Complete (Auto)) 
         THEN (All (Unfold `fpf-ap`)⋅ THEN Auto)⋅)⋅) }

---

Latex:


\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B,C,D,E,F,G:A  {}\mrightarrow{}  Type].  \mforall{}[f:a:A  fp->  B[a]].  \mforall{}[g:a:A  fp->  C[a]].
\mforall{}[h:a:A  fp->  D[a]].
    (\{(f  \moplus{}  g  ||  h)  supposing  (g  ||  h  and  f  ||  h)\})  supposing 
          ((\mforall{}a:A.  (E[a]  \msubseteq{}r  G[a]))  and 
          (\mforall{}a:A.  (F[a]  \msubseteq{}r  G[a]))  and 
          (\mforall{}a:A.  (D[a]  \msubseteq{}r  F[a]))  and 
          (\mforall{}a:A.  (D[a]  \msubseteq{}r  E[a]))  and 
          (\mforall{}a:A.  (C[a]  \msubseteq{}r  F[a]))  and 
          (\mforall{}a:A.  (B[a]  \msubseteq{}r  E[a])))


By

(Unfold  `guard`  0
  THEN  Auto
  THEN  (All  (Unfold  `fpf-compatible`))
  THEN  Auto
  THEN  (RWO  "fpf-join-dom2"  (-2))
  THEN  Auto
  THEN  ((D  (-2))
              THEN  Repeat  ((Unfolds  ``fpf-cap  fpf-join  fpf-ap``  0  THEN  Reduce  0))
              THEN  SplitOnConclITE
              THEN  Auto
              THEN  AllHyps  h.((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  h)\mcdot{}  THENA  Complete  (Auto)) 
              THEN  (All  (Unfold  `fpf-ap`)\mcdot{}  THEN  Auto)\mcdot{})\mcdot{})

---

Home Index