---

Step * of Lemma l-first_wf

∀[T:Type]. ∀[f:T ⟶ 𝔹]. ∀[L:T List].  (l-first(x.f[x];L) ∈ (∃x:{T| ((x ∈ L) ∧ (↑f[x]))}) ∨ (∀x∈L.¬↑f[x]))
BY
{ (Unfold `l-first` 0
   THEN InductionOnList
   THEN Reduce 0
   THEN ((BoolCase ⌜f[u]⌝⋅ THENA Auto) ORELSE Auto')
   THEN ((DoSubsume THENL [Hypothesis; Auto]) ORELSE Auto)) }

1
.....wf..... 
1. T : Type
2. f : T ⟶ 𝔹
3. u : T
4. ¬↑f[u]
5. v : T List
6. rec-case(v) of
   [] => inr (λx.Ax) 
   x::xs =>
    r.if f[x] then inl x else r fi  ∈ (∃x:{T| ((x ∈ v) ∧ (↑f[x]))}) ∨ (∀x∈v.¬↑f[x])
7. rec-case(v) of
   [] => inr (λx.Ax) 
   h::t =>
    r.if f[h] then inl h else r fi 
= rec-case(v) of
  [] => inr (λx.Ax) 
  h::t =>
   r.if f[h] then inl h else r fi 
∈ ((∃x:{T| ((x ∈ v) ∧ (↑f[x]))}) ∨ (∀x∈v.¬↑f[x]))
8. x : ∃x:{T| ((x ∈ v) ∧ (↑f[x]))} + (∀x∈v.¬↑f[x])
⊢ x ∈ ∃x:{T| ((x ∈ [u / v]) ∧ (↑f[x]))} + (∀x∈[u / v].¬↑f[x])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].
    (l-first(x.f[x];L)  \mmember{}  (\mexists{}x:\{T|  ((x  \mmember{}  L)  \mwedge{}  (\muparrow{}f[x]))\})  \mvee{}  (\mforall{}x\mmember{}L.\mneg{}\muparrow{}f[x]))


By

---

Latex:
(Unfold  `l-first`  0
  THEN  InductionOnList
  THEN  Reduce  0
  THEN  ((BoolCase  \mkleeneopen{}f[u]\mkleeneclose{}\mcdot{}  THENA  Auto)  ORELSE  Auto')
  THEN  ((DoSubsume  THENL  [Hypothesis;  Auto])  ORELSE  Auto))

---

Home Index