---

Step * 2 1 2 1 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))))
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))
BY
{ (Reduce 0 THEN (SplitOnConclITE THENA Auto)) }

1
.....truecase..... 
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)
11. ↑can-apply(u;x)
⊢ hd([u / filter(λf.can-apply(f;x);v)]) = f ∈ (A ⟶ (B + Top))

2
.....falsecase..... 
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)
11. ¬↑can-apply(u;x)
⊢ hd(filter(λf.can-apply(f;x);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))
6.  x  :  A
7.  f  :  A  {}\mrightarrow{}  (B  +  Top)
8.  (\mforall{}f,g\mmember{}[u  /  v].    p-disjoint(A;f;g))
9.  (f  \mmember{}  [u  /  v])
10.  \muparrow{}can-apply(f;x)
\mvdash{}  hd(filter(\mlambda{}f.can-apply(f;x);[u  /  v]))  =  f


By

---

Latex:
(Reduce  0  THEN  (SplitOnConclITE  THENA  Auto))

---

Home Index