---

Step * 2 1 2 1 1 1 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))))
6. x : A
7. f : A ⟶ (B + Top)
8. (∀f,g∈[u / v].  p-disjoint(A;f;g))
9. i : ℕ
10. i < ||[u / v]||
11. f = [u / v][i] ∈ (A ⟶ (B + Top))
12. ↑can-apply(f;x)
13. ↑can-apply(u;x)
14. ¬(i = 0 ∈ ℤ)
⊢ u = f ∈ (A ⟶ (B + Top))
BY
{ (Unfold `pairwise` (-7) THEN (InstHyp [⌜i⌝;⌜0⌝] (-7)⋅ THENA 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. ∀i:ℕ||[u / v]||. ∀j:ℕi.  p-disjoint(A;[u / v][j];[u / v][i])
9. i : ℕ
10. i < ||[u / v]||
11. f = [u / v][i] ∈ (A ⟶ (B + Top))
12. ↑can-apply(f;x)
13. ↑can-apply(u;x)
14. ¬(i = 0 ∈ ℤ)
15. p-disjoint(A;[u / v][0];[u / v][i])
⊢ u = 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.  i  :  \mBbbN{}
10.  i  <  ||[u  /  v]||
11.  f  =  [u  /  v][i]
12.  \muparrow{}can-apply(f;x)
13.  \muparrow{}can-apply(u;x)
14.  \mneg{}(i  =  0)
\mvdash{}  u  =  f


By

---

Latex:
(Unfold  `pairwise`  (-7)  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]  (-7)\mcdot{}  THENA  Auto))\mcdot{}

---

Home Index