---

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
{ ((((((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)) ) }

---

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:
((((((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))  )

---

Home Index