---

Step * of Lemma fpf-join-cap-sq

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> Top]. ∀[x:A]. ∀[z:Top].
  (f ⊕ g(x)?z ~ if x ∈ dom(f) then f(x)?z else g(x)?z fi )
BY
{ xxx((((((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 ∀h:hyp. (D h THEN OrLeft THEN Complete (Auto)) 
      THEN ∀h:hyp. (D h THEN OrRight THEN Complete (Auto)) )xxx }

---

Latex:

---

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{}  if  x  \mmember{}  dom(f)  then  f(x)?z  else  g(x)?z  fi  )


By

---

Latex:
xxx((((((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  \mforall{}h:hyp.  (D  h  THEN  OrLeft  THEN  Complete  (Auto)) 
        THEN  \mforall{}h:hyp.  (D  h  THEN  OrRight  THEN  Complete  (Auto))  )xxx

---

Home Index