---

Step * 2 1 2 of Lemma do-apply-p-first-disjoint


1. A : Type
2. B : Type
3. u : A ⟶ (B + Top)
4. v : (A ⟶ (B + Top)) List
5. ∀x:A. ∀f:A ⟶ (B + Top).
     ((∀f,g∈v.  p-disjoint(A;f;g))
     ⇒ (f ∈ v)
     ⇒ (↑can-apply(f;x))
     ⇒ (hd(filter(λf.can-apply(f;x);v)) = f ∈ (A ⟶ (B + Top))))
⊢ ∀x:A. ∀f:A ⟶ (B + Top).
    ((∀f,g∈[u / v].  p-disjoint(A;f;g))
    ⇒ (f ∈ [u / v])
    ⇒ (↑can-apply(f;x))
    ⇒ (hd(filter(λf.can-apply(f;x);[u / v])) = f ∈ (A ⟶ (B + Top))))
BY
{ Auto }

1
1. A : Type
2. B : Type
3. u : A ⟶ (B + Top)
4. v : (A ⟶ (B + Top)) List
5. ∀x:A. ∀f:A ⟶ (B + Top).
     ((∀f,g∈v.  p-disjoint(A;f;g))
     ⇒ (f ∈ v)
     ⇒ (↑can-apply(f;x))
     ⇒ (hd(filter(λf.can-apply(f;x);v)) = f ∈ (A ⟶ (B + Top))))
6. x : A
7. f : A ⟶ (B + Top)
8. (∀f,g∈[u / v].  p-disjoint(A;f;g))
9. (f ∈ [u / v])
10. ↑can-apply(f;x)
⊢ hd(filter(λf.can-apply(f;x);[u / v])) = f ∈ (A ⟶ (B + Top))

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  u  :  A  {}\mrightarrow{}  (B  +  Top)
4.  v  :  (A  {}\mrightarrow{}  (B  +  Top))  List
5.  \mforall{}x:A.  \mforall{}f:A  {}\mrightarrow{}  (B  +  Top).
          ((\mforall{}f,g\mmember{}v.    p-disjoint(A;f;g))
          {}\mRightarrow{}  (f  \mmember{}  v)
          {}\mRightarrow{}  (\muparrow{}can-apply(f;x))
          {}\mRightarrow{}  (hd(filter(\mlambda{}f.can-apply(f;x);v))  =  f))
\mvdash{}  \mforall{}x:A.  \mforall{}f:A  {}\mrightarrow{}  (B  +  Top).
        ((\mforall{}f,g\mmember{}[u  /  v].    p-disjoint(A;f;g))
        {}\mRightarrow{}  (f  \mmember{}  [u  /  v])
        {}\mRightarrow{}  (\muparrow{}can-apply(f;x))
        {}\mRightarrow{}  (hd(filter(\mlambda{}f.can-apply(f;x);[u  /  v]))  =  f))


By

---

Latex:
Auto

---

Home Index