---

Step * of Lemma fpf-join-cap

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> Top]. ∀[x:A]. ∀[z:Top].  (f ⊕ g(x)?z ~ f(x)?g(x)?z)
BY
{ ((((((UnivCD THENA Auto) THEN Unfold `fpf-cap` 0 THEN RWO "fpf-join-ap-sq" 0) THENA Auto)
     THEN Repeat ((SplitOnConclITE THENA Auto))
     THEN Try (Trivial)
     THEN (All (RWO "fpf-join-dom")))
    THENA Auto
    )
   THEN SplitOrHyps
   THEN Try (Trivial)
   THEN AllHyps h.(D h THEN OrLeft THEN Complete (Auto)) 
   THEN AllHyps h.(D h THEN OrRight THEN Complete (Auto)) ) }

---

Latex:


\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f,g:a:A  fp->  Top].  \mforall{}[x:A].  \mforall{}[z:Top].    (f  \moplus{}  g(x)?z  \msim{}  f(x)?g(x)?z)


By

((((((UnivCD  THENA  Auto)  THEN  Unfold  `fpf-cap`  0  THEN  RWO  "fpf-join-ap-sq"  0)  THENA  Auto)
      THEN  Repeat  ((SplitOnConclITE  THENA  Auto))
      THEN  Try  (Trivial)
      THEN  (All  (RWO  "fpf-join-dom")))
    THENA  Auto
    )
  THEN  SplitOrHyps
  THEN  Try  (Trivial)
  THEN  AllHyps  h.(D  h  THEN  OrLeft  THEN  Complete  (Auto)) 
  THEN  AllHyps  h.(D  h  THEN  OrRight  THEN  Complete  (Auto))  )

---

Home Index