---

Step * of Lemma do-apply-p-first

∀[A,B:Type]. ∀[L:(A ⟶ (B + Top)) List]. ∀[x:A].
  do-apply(p-first(L);x) = do-apply(hd(filter(λf.can-apply(f;x);L));x) ∈ B supposing ↑can-apply(p-first(L);x)
BY
{ xxxInductionOnListxxx }

1
1. A : Type
2. B : Type
⊢ ∀[x:A]. do-apply(p-first([]);x) = do-apply(hd(filter(λf.can-apply(f;x);[]));x) ∈ B supposing ↑can-apply(p-first([]);x)

2
1. A : Type
2. B : Type
3. u : A ⟶ (B + Top)
4. v : (A ⟶ (B + Top)) List
5. ∀[x:A]. do-apply(p-first(v);x) = do-apply(hd(filter(λf.can-apply(f;x);v));x) ∈ B supposing ↑can-apply(p-first(v);x)
⊢ ∀[x:A]
    do-apply(p-first([u / v]);x) = do-apply(hd(filter(λf.can-apply(f;x);[u / v]));x) ∈ B 
    supposing ↑can-apply(p-first([u / v]);x)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[L:(A  {}\mrightarrow{}  (B  +  Top))  List].  \mforall{}[x:A].
    do-apply(p-first(L);x)  =  do-apply(hd(filter(\mlambda{}f.can-apply(f;x);L));x) 
    supposing  \muparrow{}can-apply(p-first(L);x)


By

---

Latex:
xxxInductionOnListxxx

---

Home Index