---

Step * 2 1 2 1 1 1 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. ∀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))
BY
{ (Reduce (-1) THEN (RevHypSubst' -5 -1 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;f)
⊢ 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{}i:\mBbbN{}||[u  /  v]||.  \mforall{}j:\mBbbN{}i.    p-disjoint(A;[u  /  v][j];[u  /  v][i])
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)
15.  p-disjoint(A;[u  /  v][0];[u  /  v][i])
\mvdash{}  u  =  f


By

---

Latex:
(Reduce  (-1)  THEN  (RevHypSubst'  -5  -1  THENA  Auto))

---

Home Index