---

Step * of Lemma fpf-compatible-triple

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[f,g,h:x:T fp-> Type].
  ({(g ⊆ h ⊕ f ⊕ g ∧ f ⊆ h ⊕ f ⊕ g) ∧ h ⊕ g ⊆ h ⊕ f ⊕ g ∧ h ⊕ f ⊆ h ⊕ f ⊕ g}) supposing (h || g and h || f and f || g)
BY
{ (Auto
   THEN Unfolds ``guard fpf-sub`` 0
   THEN Auto
   THEN (AllHyps h.((RWO "fpf-join-dom" h THENM D h) THEN Complete (Auto)) 
         THEN ((RWW "fpf-join-ap-sq" 0⋅ THENA Auto)
               THEN Repeat (AutoSplit)
               THEN Symmetry
               THEN Auto
               THEN AllHyps h.((RWO "fpf-join-dom" h THENM D h) THEN Auto) ⋅)⋅
         )⋅) }

---

Latex:


\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[f,g,h:x:T  fp->  Type].
    (\{(g  \msubseteq{}  h  \moplus{}  f  \moplus{}  g  \mwedge{}  f  \msubseteq{}  h  \moplus{}  f  \moplus{}  g)  \mwedge{}  h  \moplus{}  g  \msubseteq{}  h  \moplus{}  f  \moplus{}  g  \mwedge{}  h  \moplus{}  f  \msubseteq{}  h  \moplus{}  f  \moplus{}  g\})  supposing 
          (h  ||  g  and 
          h  ||  f  and 
          f  ||  g)


By

(Auto
  THEN  Unfolds  ``guard  fpf-sub``  0
  THEN  Auto
  THEN  (AllHyps  h.((RWO  "fpf-join-dom"  h  THENM  D  h)  THEN  Complete  (Auto)) 
              THEN  ((RWW  "fpf-join-ap-sq"  0\mcdot{}  THENA  Auto)
                          THEN  Repeat  (AutoSplit)
                          THEN  Symmetry
                          THEN  Auto
                          THEN  AllHyps  h.((RWO  "fpf-join-dom"  h  THENM  D  h)  THEN  Auto)  \mcdot{})\mcdot{}
              )\mcdot{})

---

Home Index