---

Step * of Lemma can-apply-compose

∀[A,B,C:Type]. ∀[g:A ⟶ (B + Top)]. ∀[f:B ⟶ (C + Top)]. ∀[x:A].
  {(↑can-apply(g;x)) ∧ (↑can-apply(f;do-apply(g;x)))} supposing ↑can-apply(f o g;x)
BY
{ (Auto
   THEN (MoveToConcl (-1))
   THEN ((RWO "can-apply-compose-sq" (0)) THENA Auto)
   THEN Unfold `guard` 0
   THEN AutoBoolCase ⌜can-apply(g;x)⌝⋅) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[g:A  {}\mrightarrow{}  (B  +  Top)].  \mforall{}[f:B  {}\mrightarrow{}  (C  +  Top)].  \mforall{}[x:A].
    \{(\muparrow{}can-apply(g;x))  \mwedge{}  (\muparrow{}can-apply(f;do-apply(g;x)))\}  supposing  \muparrow{}can-apply(f  o  g;x)


By

---

Latex:
(Auto
  THEN  (MoveToConcl  (-1))
  THEN  ((RWO  "can-apply-compose-sq"  (0))  THENA  Auto)
  THEN  Unfold  `guard`  0
  THEN  AutoBoolCase  \mkleeneopen{}can-apply(g;x)\mkleeneclose{}\mcdot{})

---

Home Index